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

研究的目的是提供一个环境，在这个环境中，人们可以统一处理程序规范的描述、规范的证明、程序的验证和综合。为此，我们设计了一个基于直觉逻辑的构造性逻辑系统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程序中使用的逻辑符号具有自然的逻辑意义。虽然我们只能就系统的实现做一些小的实验，但我们肯定会得到良好的理论结果，这将为实现奠定基础。

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.