×

A logic programming language with lambda-abstraction, function variables, and simple unification. (English) Zbl 0738.68016

Summary: This paper presents a logic programming language, called \(L_ \lambda\), that 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.

MSC:

68N17 Logic programming

Software:

ETPS
PDFBibTeX XMLCite
Full Text: DOI Link