PREDICATE ABSTRACTIONS IN HIGHER-ORDER LOGIC PROGRAMMING

Lambda calculus offers a natural representation of syntactic structure s involving higher-order constructs and local variables, and supports flexible manipulation of such concepts. Thus an integration of logic p rogramming with lambda-terms would provide more direct support for met a-programming. While it is conceptually straightforward to replace fir st-order terms with lambda-terms, the extra search space in unificatio n with respect to lambda-conversions cannot be ignored from a practica l point of view. Our objective is to explore useful alternatives with weaker conversions that are computationally more tractable. In this pa per, we study predicate abstractions, in which lambda-abstractions are used to provide anonymous predicates and functions that return predic ates. The framework is based upon a simple logic of (untyped) lambda-c alculus, called L(alpha). L(alpha) has a general model-theoretic seman tics and an equality theory that corresponds to alpha-equivalence. Int ended meanings of predicate abstractions are formalized by equivalence axioms over atomic formulas. We show that under certain conditions, c omputing with predicate abstractions does not incur any extra search s pace. Furthermore, programs in this language can be compiled staticall y into efficient Prolog programs and all most general answers are stil l preserved.