TY - GEN
T1 - A logic programming language with lambda-abstraction, function variables, and simple unification
AU - Miller, Dale
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1991.
PY - 1991/1/1
Y1 - 1991/1/1
N2 - It has been argued elsewhere that a logic programming language with function variables and λ-abstractions within terms makes a very good meta-programming language, especially when an object language contains notions of bound variables and scope. The λProlog logic programming language and the closely related Elf and Isabelle systems provide meta-programs with both function variables and λ-abstractions by containing implementations of higher-order unification. In this paper, we present a logic programming language, called Lλ, that also contains both function variables and λ-abstractions, but certain restriction are placed on occurrences of function variables. As a result, 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.
AB - It has been argued elsewhere that a logic programming language with function variables and λ-abstractions within terms makes a very good meta-programming language, especially when an object language contains notions of bound variables and scope. The λProlog logic programming language and the closely related Elf and Isabelle systems provide meta-programs with both function variables and λ-abstractions by containing implementations of higher-order unification. In this paper, we present a logic programming language, called Lλ, that also contains both function variables and λ-abstractions, but certain restriction are placed on occurrences of function variables. As a result, 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.
U2 - 10.1007/BFb0038698
DO - 10.1007/BFb0038698
M3 - Conference contribution
AN - SCOPUS:85032177635
SN - 9783540535904
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 253
EP - 281
BT - Extensions of Logic Programming - International Workshop, Proceedings
A2 - Schroeder-Heister, Peter
PB - Springer Verlag
T2 - International Workshop on Extensions of Logic Programming, 1989
Y2 - 8 December 1989 through 10 December 1989
ER -