A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
Dale MillerAbstract: It has been argued elsewhere that a logic programming language with function variables and lambda-abstractions within terms makes a good meta-programming language, especially when an object-language contains notions of bound variables and scope. The lambdaProlog logic programming language and the related Elf and Isabelle systems provide meta-programs with both function variables and lambda-abstractions by containing implementations of higher-order unification. This paper presents a logic programming language called L_lambda, that also contains both function variables and lambda-abstractions, although certain restrictions are placed on occurrences of function variables. As a result of these restrictions, an implementation of L_lambda 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_lambda as a meta-programming language are presented.
A revised version appeared in the Journal of Logic and Computation, Vol. 1, No. 4 (1991), 497 -- 536.
Previous | Index | Next