Design of a functional logic programming language, and development of proof, vorification and synthosis system based on it.

函数式逻辑编程语言的设计，以及基于它的证明、验证和综合系统的开发。

• 批准号: 60580018
• 负责人: SATO Masahiko
• 金额: $ 0.96万
• 依托单位: TOHOKU UNIVERSITY (1986)The University of Tokyo (1985)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1985
• 资助国家: 日本
• 起止时间: 1985 至 1986
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-60580018/
• 关键词: constructive mathematics; formal semantics of programs; data type; verification of programs; Functional programming language; 論理型プログラム言語

The aim of the research was to provide an environment in which one can uniformly treat description of the specification of a program, proof of the specification, verification and synthesis of programs. To this end, we designed a constructive logical system QJ which is based on intuitionistic logic and a functional logic programming language Quty which is a subsystem of QJ.The programming language Quty has the following characteristics. 1. It has the logical symbols <not> , <and> , <or> and <exist> as its basic elements. The meanings of these logical symbols coincide with those of corresponding symbols in intuitionistic logic. It is therefore possible to write logically natural programs. 2. It has rich data types including function types. It is therefore possible to write functional programs which treat these higher type data. 3. Programs are executed in parallel. Parallel programming based on shared variables and streams are possible.QJ is a constructive logical system with types. QJ is designed so that the terms of QJ are exactly the programs of Quty. It is therefore possible to specify programs, prove the specification and verify programs in QJ. We also proved the consistency of the operational semantics of Quty within QJ. This means that a computation in Quty corresponds to a proof in QJ and that the logical symbols used in Quty programs have the natural logical meanings.Although we could only do a small experiments with regard to the implementation of the system, we certainly obtained good theoretical results which would form a basis for the implementation.

研究的目的是提供一个环境，在这个环境中，人们可以统一处理程序规范的描述、规范的证明、程序的验证和综合。为此，我们设计了一个基于直觉逻辑的构造性逻辑系统QJ和QJ的一个子系统函数逻辑程序设计语言Quty。1.它以逻辑符号&lt；NOT&gt；，&lt；和&gt；，或&gt；和&lt；Exist&gt；为其基本元素。这些逻辑符号的含义与直觉逻辑中相应符号的含义一致。因此，可以编写逻辑上自然的程序。2.数据类型丰富，包括函数类型。因此，编写处理这些较高类型数据的函数程序是可能的。3.程序并行执行。基于共享变量和流的并行编程是可能的。QJ是一个具有类型的构造性逻辑系统。QJ的设计使得QJ的条款完全是Quty的程序。因此，可以在QJ中指定程序、证明规范和验证程序。证明了QJ中Quty的操作语义的一致性。这意味着Quty中的一个计算对应于QJ中的一个证明，Quty程序中使用的逻辑符号具有自然的逻辑意义。虽然我们只能就系统的实现做一些小的实验，但我们肯定会得到良好的理论结果，这将为实现奠定基础。

项目成果

Masahiko Sato: "Typed Logical Calculus" Technical Report, Dept. of Into. Science, University of Tokyo. 85-13. 1-37 (1985)

Masahiko Sato：“类型化逻辑演算”技术报告，Into 部。

Masahiko Sato: "Theory of Symbolic Expressions <II> " Publ. RIMS, Kyoto University. 21. 455-540 (1985)

佐藤正彦：《符号表达理论<II>》出版。

Masahiko Sato and Takafumi Sakurai: "Qute : A Functional Langnage Bared on Unification" Logic Programming. 131-154 (1986)

Masahiko Sato 和 Takafumi Sakurai：“Qute：一种基于统一的函数式语言”逻辑编程。

佐藤雅彦: Technical Report,Dept.of Info Science,Univ.Tokyo. 85-13. 1-37 (1985)

佐藤正彦：东京大学信息科学系技术报告 85-13 (1985)。

佐藤雅彦: France,Japan Artificial Intelligence and Computer Science Symposium86. 159-174 (1986)

佐藤正彦：法国、日本人工智能和计算机科学研讨会86（1986）。