Predicate abstractions in higher-order logic programming

Lambda calculus offers a natural representation of syntactic structures involving higher-order constructs and local variables, and supports flexible manipulation of such concepts. Thus an integration of logic programming with lambda-terms would provide more direct support for meta-programming. While it is conceptually straightforward to replace first-order terms with lambda-terms, the extra search space in unification with respect to lambda-conversions cannot be ignored from a practical point of view. Our objective is to explore useful alternatives with weaker conversions that are computationally more tractable. In this paper, we study predicate abstractions, in which lambda-abstractions are used to provide anonymous predicates and functions that return predicates. The framework is based upon a simple logic of (untyped) lambda-calculus, called L(alpha). L(alpha) has a general model-theoretic semantics and an equality theory that corresponds to alpha-equivalence. Intended meanings of predicate abstractions are formalized by equivalence axioms over atomic formulas. We show that under certain conditions, computing with predicate abstractions does not incur any extra search space. Furthermore, programs in this language can be compiled statically into efficient Prolog programs and all most general answers are still preserved.