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（懒惰的狭窄微积分）进行仔细检查，我们消除了针对适用推理规则的非确定性，该规则的设计导致了新的计算规则的设计，该设计称为LNCD（确定性的懒惰narrownownount Colculus）。与LNC Dueto确定适用的推理规则相比，LNCD的速度非常有效。2。我们为标准化定理提出了一种新的证明方法。 Thi…更多的定理被称为功能编程语言中懒惰评估机制的理论基础。使用该定理，我们获得了更有效的一阶狭窄机制。3。我们为以下三个功能性编程语言家族提供了语义：多级的一阶语言，交互式的一阶语言和简单地键入适用语言。我们使用等价逻辑对这些功能性语言进行了语法。语义作为方程式解释。我们已经展示了公理，代数，操作和分类语义之间的严格关系，以显示这些语义的正确性。4。我们提出了一个高阶狭窄的缩放计算HLNC（高阶懒惰狭窄的缩放计算计算），以实现高阶狭窄范围，以实现高阶范围狭窄范围。 HLNC源自一阶狭窄的微积分，并使用了上述有效狭窄机制的技术来实施该技术。由于此计算允许在TRS中存在Lambda项，因此它为具有Lambda项的高阶功能性语言提供了计算模型。较少的

项目成果

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: "Minimised Geomtric Buchberger Al-gorithm:An Optimal Algebraic Algorithm for Integer Programming" Proc.of ISSAC'97. 331-338 (1997)

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

I.Durand et al: "Decidable Call by Need Computations in Term Rewriting" Proc.of 14th International Conference on Automated Deduction. LNAI 1249. (1997)

I.Durand 等人：“术语重写中需要计算的可判定调用”第 14 届国际自动演绎会议论文集。

M.M.T.Chakravarty et al.: "A Computational Model for Constraint Functional-Logic Programming" 第14回日本ソフトウエア科学会大会論文集. 301-304 (1997)

M.M.T.Chakravarty 等人：“约束功能逻辑编程的计算模型”第 14 届日本软件科学学会会议记录 301-304 (1997)。

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。