computation model for higher-order functional-logic languages

高阶函数逻辑语言的计算模型

基本信息

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

项目摘要

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

函数式编程的经验表明，高阶概念可以带来强大而简洁的函数式编程，这是一种集成函数式和逻辑编程的方法，人们自然会期望将高阶性的概念纳入其中。如何将高阶性融入函数式逻辑编程中。我们的研究项目的目的是为高阶函数式逻辑编程提供理论基础。我们在这个项目中的结果列举如下：1.通过仔细的检查。关于一阶计算缩小演算 LNC（惰性缩小演算），我们消除了适用推理规则选择上的非确定性，这导致了一种称为 LNCd（确定性惰性缩小演算）的新演算的设计，由于其确定性，与 LNC 相比，速度效率更高。适用的推理规则的选择。2.我们提出了一种新的标准化定理证明方法。该定理被称为懒惰评估机制的理论基础。使用这个定理，我们提供了更高效的一阶缩小机制。3.我们给出了以下三个函数逻辑编程语言家族的语义：多排序一阶语言、交互式一阶语言我们使用等式逻辑作为方程的解释来制定这些功能逻辑语言的语法，我们已经展示了公理语义、代数语义、运算语义和分类语义之间的严格关系。 4.我们提出了一种高阶窄化演算 HLNC (Higher-order Lazy Narrowing Calculus)，为高阶术语重写系统实现高阶窄化 HLNC 是从一阶窄化演算导出的。由于该演算允许 TRS 中存在 lambda 项，因此它为具有 Less 的高阶函数逻辑语言提供了计算模型。