| Project/Area Number |
08458059
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
IDA Tetsuo University of Tsukuba Instiute of information science and electronics professor, 電子・情報工学系, 教授 (70100047)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
SUZUKI Taro research associate, 電子・情報工学系, 助手 (90272179)
CHAKRAVARY Manuel lecturer, 電子・情報工学系, 講師 (30292535)
MIDDELDORP Aart associate professor, 電子・情報工学系, 助教授 (30251044)
|
|---|
| Project Period (FY) |
1996 – 1997
|
| Project Status |
Completed (Fiscal Year 1997)
|
| Budget Amount *help |
¥3,800,000 (Direct Cost: ¥3,800,000)
Fiscal Year 1997: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 1996: ¥2,800,000 (Direct Cost: ¥2,800,000)
|
|---|
| Keywords | narrowing / higher-order functional-logic language / computation model / conditional rewriting / completeness / 高階関数論理型言語 / 求解完全性 / 安全性 |
|---|
| Research Abstract |
Experiences with functional programming show that higher-order concept leads to powerful and succinct programming. Functional-logic programming, an approach to integrate functional and logic programming, would naturally be expected to incorporate the notion of higher-order-ness. Little has been investigated how to incorporate higher-order-ness in functional-logic programming. The aim of our research project is to provide theoretical foundation for higher-order functional-logic programming. Our result in this project are enumerated as follows.
1.By a close examination on computation in a first-order narrowing calculus LNC (Lazy Narrowing Calculus), we eliminated non-determinism on the selection of applicable inference rules, which lead a design of new calculus called LNCd (deterministic Lazy Narrowing Calculus). LNCd is much efficient in speed compared to LNC dueto determinism on the selection of applicable inference rules.
2.We proposed a new proof method for standardization theorem. Thi
… More
s theorem is known as a theoretical foundation for lazy evaluation mechanism in functional programming languages. Using this theorem we obtained more effcient first-order narrowing mechanism.
3.We gave semantics for the following three families of functional-logic programming languages : many-sorted first-order languages, interactive first-order languages and simply typed applicative languages. We formulated syntax of these functional-logic languages using equational logic. Semantics given as interpretation of equations. We have shown the rigorous relationship between axiomatic, algebraic, operational and categorical semantics in order to show correctness of these semantics.
4.We proposed a higher-order narrowing calculus HLNC (Higher-order Lazy Narrowing Calculus) implementing higher-order narrowing for higher-order term rewriting systems. HLNC is derived from a first order narrowing calculus with the employment of the techniques for the implementation of efficient narrowing mechanism described above. Since this calculus allows the presence of lambda terms in TRSs, it provides computation model for higher-order functional-logic languages with lambda terms. Less
|
