computation model for higher-order functional-logic languages

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

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