Higher Order Logic Programming with Untyped Lambda Expressions

. A higher order logic programming system is presented. The declarative semantics of the system is based on the type-free higher order logic NaDSyL, which takes a nominalist approach to solving the set-theoretic paradoxes. The operational semantics is based on the deterministic and useful subset of higher order unification known as pattern unification. It is shown that the system allows all expressions of the untyped lambda calculus, including the Y combinator and expressions capturing recursive functions, without losing consistency due to Curry's paradox. The system automatically performs lazy function application and thus unifies higher order logic and functional programming in a simple and elegant manner. 1 Introduction The three notions of logic programming, functional programming, and higher order have been combined in various ways in recent years. We have higher-order functional languages like ML, higher order logic languages like Lambda Prolog, and proposals for combined functi..