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
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08458059/
• 关键词: narrowing; higher-order functional-logic language; computation model; conditional rewriting; completeness; 高階関数論理型言語; 求解完全性; 安全性

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（Lazy Narrowing Calculus）的计算分析，消除了推理规则选择的不确定性，设计了一种新的演算LNCd（deterministic Lazy Narrowing Calculus）。由于LNCd在推理规则的选择上具有确定性，因此与LNC相比，LNCd在速度上有很大的提高。2.提出了一种新的标准化定理的证明方法。Thi ...更多信息 S定理是函数式程序设计语言中惰性求值机制的理论基础。3.给出了三类函数逻辑程序设计语言的语义：多类一阶语言、交互式一阶语言和简单类型应用语言。我们使用等式逻辑制定了这些函数逻辑语言的语法。作为方程的解释给出的语义。为了证明这些语义的正确性，我们给出了公理语义、代数语义、操作语义和范畴语义之间的严格关系。4.提出了一种高阶窄化演算HLNC（Higher-order Lazy Narrowing Calculus），实现了高阶项重写系统的高阶窄化。HLNC是从一阶缩窄演算中导出的，采用了用于实现上述高效缩窄机制的技术。由于这种演算允许在TRS中存在lambda项，因此它为具有lambda项的高阶函数逻辑语言提供了计算模型。少

项目成果

Q.Li: "Minimised Geomtric Buchberger Al-gorithm:An Optimal Algebraic Algorithm for Integer Programming" Proc.of ISSAC'97. 331-338 (1997)

Q.Li：“最小化几何布赫伯格算法：整数规划的最优代数算法”Proc.of ISSAC97。

T.Yamada et al.: "Logicality of Conditional Rewrite Systems" Proceedings of the 22nd International Colloquium on Trees in Algebra and Programming(CAAP'97). LNCS1214. 141-152 (1997)

T.Yamada 等人：“条件重写系统的逻辑性”第 22 届国际代数和编程树研讨会论文集 (CAAP97)。

Q., Li: "A Parallel Algebrac Approach Towards Integer Programing" Proc.of the 9th International Conference on PDCS. 59-64 (1997)

Q.，Li：“整数规划的并行代数方法”Proc. of the 9th International Conference on PDCS。

M.Hamada et al.: "Deterministic and Non-deterministic Lazy Conditional Narrowing and their implementations" J.of IPSJ. 79 (3), to appear. (1998)

M.Hamada 等人：“确定性和非确定性惰性条件缩小及其实现”J.of IPSJ。

A.Middeldorp et al: "Transforming Termination by Self-Labelling" Proc.of the 13th Int.Conf.on Automated Deduction. LNAI 1104. 373-387 (1996)

A.Middeldorp 等人：“通过自我标签转变终止”Proc.of the 13th Int.Conf.on Automated Deduction。