Lambda-equational logic programming
Mantis H. M. Cheng · 1987
Recent attempts at amalgamating functional and logic programming have neglected one of the most appealing features of functional programming--higher-order functions (3). One reason for not introducing such a feature in logic programming is the undecidability of higher order unification. It is known that the unification problem in second-order logic is semi-decidable and above that is undecidable (11). The semantical basis of most functional programming languages is founded on the type-free $\lambda$-calculus (6). Functions in $\lambda$-calculus are first class objects, i.e., they can be used as arguments and returned as results. In this sense, all functions in $\lambda$-calculus are higher order. On the other hand, logic programming is founded on a subset of first-order predicate logic. The efficient implementation technology of PROLOG has demonstrated the viability of using logic as a programming language. In this dissertation we show that it is possible to embed $\lambda$-calculus in logic programming in such a way that higher-order functions are preserved. We translate $\lambda$-terms into a set of first-order equations. The reductions on $\lambda$-terms are mimicked by term rewriting using the translated set of equations. We show that the complexity of our computation method on $\lambda$-terms is acceptable and prove its soundness and completeness with respect to the reduction rules of $\lambda$-calculus.