Higher
Order Logic Programming with Untyped Lambda Expressions.
by James H. Andrews
| |
Higher
Order Logic Programming with Untyped Lambda Expressions.
by James H. Andrews
|
| formalWARE
project
formalWARE
formalWARE
|
Abstract
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. Download Postscript
This paper was submitted to Computer Science Logic 1998 (CSL '98)
|
