Systematic Construction of Declarative Programming Systems

声明式编程系统的系统构建

基本信息

批准号：
03680022
负责人：
IDA Tetsuo
金额：
$ 1.22万
依托单位：
University of Tsukuba
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1991
资助国家：
日本
起止时间：
1991 至 1992
项目状态：
已结题

项目摘要

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.

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