Systematic Construction of Declarative Programming Systems

点击翻译按钮获取中文摘要

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.