computation model for higher-order functional-logic languages

函数式编程的经验表明，高阶概念会带来强大而简洁的编程。函数逻辑编程是一种集成函数编程和逻辑编程的方法，自然应该包含更高阶数的概念。很少有人研究如何在函数逻辑编程中融入高阶性。本课题的研究目的是为高阶函数逻辑程序设计提供理论基础。1.通过对一阶窄化演算LNC(Lazy Stringing Calculus)计算的深入研究，消除了适用推理规则选择上的不确定性，设计了一种新的演算LNCd(Definistic Lazy Holding Calculus)。由于确定性推理规则的选择，使得LNCd在速度上比LNC高效得多。2.提出了标准化定理的一种新的证明方法。Thi…S定理更是函数式程序设计语言中懒惰求值机制的理论基础。利用这个定理，我们得到了更有效的一阶缩窄机制。3.我们给出了以下三类函数逻辑程序设计语言的语义：多排序一阶语言、交互一阶语言和简单类型应用语言。我们使用等式逻辑来描述这些函数逻辑语言的语法。作为方程式的解释给出的语义学。为了证明这些语义的正确性，我们给出了公理语义、代数语义、运算语义和范畴语义之间的严格关系。4.提出了一种高阶缩窄演算HLNC(Higher-Order Lazy Holding Calculus)，实现了高阶重写系统的高阶缩窄。HLNC是利用上述用于实现有效缩窄机制的技术从一阶缩窄演算推导而来的。由于这个演算允许在TRSS中存在lambda项，因此它为具有lambda项的高阶函数逻辑语言提供了计算模型。较少

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