## A Logic Programming Language with Lambda-Abstraction, Function
Variables, and Simple Unification

**Dale Miller**
*Abstract:* 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.

*LFCS report ECS-LFCS-91-159*

A revised version appeared in the *Journal of Logic and
Computation*, Vol. 1, No. 4 (1991), 497 -- 536.

Previous |

Index |

Next