Practical Higher-Order Functional and Logic Programming Based on Lambda-Calculus and Set-Abstraction

摘要

The authors propose new variation of relative set abstraction as an extension to a lambda-calculus-based functional language. This feature interacts orthogonally with the standard functional language capabilities, yet provides the full expressive power of first-order Horn-logic programming, as well as a very useful subset of higher-order Horn-logic programming. This resulting language lends itself to efficient interpretation, in that complete operational procedures are possible without computationally expensive primitives such as higher-order unification, unification relative to an equational theory, or general theorem-proving.