Systematic Construction of Declarative Programming Systems
| Project/Area Number |
03680022
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
IDA Tetsuo Institute of Information Sciences and Electronic University of Tsukuba, Professor, 電子・情報工学系, 教授 (70100047)
|
|---|
| Project Period (FY) |
1991 – 1992
|
| Project Status |
Completed (Fiscal Year 1992)
|
| Budget Amount *help |
¥1,900,000 (Direct Cost: ¥1,900,000)
Fiscal Year 1992: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1991: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | Lisp / Prolog / Functional programming / Logic Programming / Narrowing / Integration of functional and logic programming / Program transformation from Prolog to Lisp / 論理型プログラミング / 関数、論理型プログラミングの融合 / プログラミング変換 / 項書換え系 / 遅延ナロ-イング |
|---|
| Research Abstract |
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.
|
Report
(3 results)
Research Products
(3 results)
