A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
复制标题
DOI：
10.1007/bfb0038698
复制
发表时间：
1991-02
期刊：
影响因子：
--
通讯作者：
D. Miller
中科院分区：
文献类型：
--
作者：
D. Miller
在其他地方有人争论说，在术语中具有函数变量和 λ 抽象的逻辑编程语言是一种很好的元编程语言，特别是当对象语言包含绑定变量和范围的概念时。 λProlog 逻辑编程语言和相关的 Elf 和 Isabelle 系统通过包含高阶统一的实现来提供具有函数变量和 λ 抽象的元程序。本文提出了一种逻辑编程语言，称为 Lλ，它也包含函数变量和 λ 抽象，尽管对函数变量的出现有一定的限制。由于这些限制，Lλ 的实现不需要实现完全的高阶统一。相反，所需要的只是尊重绑定变量名称和范围的一阶统一的扩展。当统一符存在时，此类统一问题被证明是可判定的并且具有最一般的统一符。描述并证明了统一算法和逻辑编程解释器的正确性。给出了使用 Lλ 作为元编程语言的几个例子。
It has been argued elsewhere that a logic programming language with function variables and λ-abstractions within terms makes a good meta-programming language, especially when an object-language contains notions of bound variables and scope. The λProlog logic programming language and the related Elf and Isabelle systems provide meta-programs with both function variables and λ-abstractions by containing implementations of higher order unification. This paper presents a logic programming language, called Lλ, that also contains both function variables and λ-abstractions, although certain restrictions are placed on occurrences of function variables. As a result of these restrictions, an implementation of Lλdoes not need to implement full higher-order unification. Instead, an extension to first-order unification that respects bound variable names and scopes is all that is required. Such unification problems are shown to be decidable and to possess most general unifiers when unifiers exist. A unification algorithm and logic programming interpreter are described and proved correct. Several examples of using Lλas a meta-programming language are presented.