Systematic Construction of Declarative Programming Systems

研究目的：(A)设计和分析作为函数式逻辑程序设计语言的计算模型的窄化（narrow）； (B)探索在Lisp的基础上将函数式（Lisp）和逻辑式（Prolog）程序设计语言集成的方法。研究结果：我们将上述研究主题分为以下几个子主题；(1)设计Lisp抽象机并验证Lisp编译器的正确性；(2)在Lisp的基础上对Prolog的操作语义进行开发；(3)设计函数逻辑编程语言的计算模型。对于(1)和(2)，我们开发了一种将Prolog程序转换为Lisp程序的编程转换方法。该方法基于对Prolog底层计算模型的系统转换：从sld -驳斥模型到Prolog抽象机。这种转换的最终结果是一个Lisp （Scheme）程序。该方法具有以下实际意义：(i)能够在更接近计算机而不是证明理论的层次上理解Prolog的操作语义，（ii）能够在Lisp程序的层次上集成Lisp和Prolog程序，（iii）能够在同一层次上比较Lisp和Prolog的计算模型。对于(3)，我们设计了一个由外而内的条件缩窄，并给出了该缩窄的完备性证明。基于由外而内的狭窄，我们进一步开发了一个模拟由外而内条件狭窄的懒惰演算。这种微积分适于计算机实现。我们的结论是，就目的(A)而言，我们已经达到了最初的目标，而就目的(B)而言，还有许多工作要做。我们只研究一类条件项重写系统，我们称之为具有严格等式的正交系统。我们必须探索其他类型的条件项重写系统，看看在什么条件下可以实现完备性。

Purpose of Research: (A) To design and analyze of narrowing as a computation model of functional-logic programming languages, (B) to explore methods for integrating functional (Lisp) and logic (Prolog) programming languages on the basis of Lisp. Results of Research: We divide the above research themes into the following subthemes ; (1) to design a Lisp abstract machine and to verify the correctness of Lisp compilers,(2) to develop on operational semantics of Prolog on the basis of Lisp, (3) to design a computation model for functional-logic programming languages.As for (1) and (2) we developed a programming transformation method that transform Prolog programs into Lisp programs. The method is based on systematic transformation of underlying computation models of Prolog: starting from models of SLD-refutations into a Prolog abstract machine. The final outcome of this transformation is a Lisp (Scheme) program. This method has the following practical implications: (i) to be able to understand the operational semantics of Prolog at a level closer to a computer rather than proof theoretic level, (ii) to be able to integrate the Lisp and Prolog programs at the level of Lisp programs, and (iii) to be able to make a comparison of computation models of Lisp and Prolog at the same level.As for (3) we designed an outside-in conditional narrowing and gave a completeness proof of that narrowing. Based on the outside-in narrowing we further developed a lazy calculus that simulated the outside-in conditional narrowing. The calculus is suited for computer implementation.We conclude that as for the purpose (A) we have achieved its initial objectives and that as for (B) many works have to be done further. We only explore a class of conditional term rewriting systems which we call orthogonal systems with strict equality. We have to explore other classes of conditional term rewriting systems to see under what conditions completeness is achievable.