z\z x\(f (g y\(h x y)) x) x\y\x f\x\(f (f (f x)))The backslash used in forming universal and existential quantification in lambda Prolog is really just the lambda-binder.
y\(append (1::2::nil) y X) list int -> o. pi y\(append (1::2::nil) y X) o.Thus, the quantifiers have the following types:
type pi (A -> o) -> o. type sigma (A -> o) -> o.In this way, all formulas (even quantificational formulas) in lambda Prolog are seen as terms of type o.
A term t is in beta-normal form if it does not contain a beta-redex (that is, a subterm of the form ((lambda x. t) s)), and in lambda-normal form if, in addition, it does not contain an eta-redex (that is, a subterm of the form (lambda x.(t x)) with x not occurring free in t). Sometimes, lambda-normal is also called beta,eta-normal.
x\y\(f (g x) y) X\Y\(f (g X) Y) x\(f (g x)) x\y\(f ((u\v\v) (2 + 3) (g x)) y)The first two terms are related by alpha-conversions. The third term is the result of doing an eta-reduction on the first. Finally, doing a beta-reduction on the fourth term yields
x\y\(f ((v\v) (g x)) y)and doing a second beta-conversion yields the first term. It is impossible for lambda Prolog to tell these four terms apart. Similarly, it is impossible for lambda Prolog to determine the name of a bound variables, since such a determination would change under alpha-conversion.
kind i type.The only closed, simply typed, lambda-normal terms of second-order type
(i -> i) -> i -> iare terms lambda-convertible to one of the following terms
f\x\x f\x\(f x)) f\x\(f (f x)) f\x\(f (f (f x))) ...These terms are called the Church numerals and can be used to denote the non-negative integers: the series above represents the numbers 0, 1, 2, and 3.
It is an easy matter to compute the successor, addition, and multiplication functions for non-negative integers using this encoding of integers. Consider the following lambda terms.
n\f\x\(f (n f x)) n\m\f\x\(n f (m f x)) n\m\f\x\(n (m f) x)Since a lambda Prolog interpreter computes the lambda-normal form of expressions prior to printing them out, we can compute the multiplication of 2 with 2, using Church numerals, by simply using the query
?- N = ((n\m\f\x\(n (m f) x))(f\x\(f (f x))) (f\x\(f (f x)))). N == f\x\(f (f (f (f x)))). yes ?-The result is, of course, the Church numeral for 4.
(g\e\e) (e\f\(e (e f))) f\x\(f (f x)). (g\e\(g e)) (e\f\(e (e f))) f\x\(f (f x)). (g\e\(g (g e))) (e\f\(e (e f))) f\x\(f (f x)). (g\e\(g (g (g e)))) (e\f\(e (e f))) f\x\(f (f x)).Here the type of the bound variables are
x : i f : i -> i e : (i -> i) -> i -> i g : ((i -> i) -> i -> i) -> (i -> i) -> i -> i.The subterms that start with g\e\ are a version of Church numeral but with the type i replaced with the type (i -> i) -> i -> i: for example, the term g\e\(g (g e)) has the fourth-order type
(((i -> i) -> i -> i) -> (i -> i) -> i -> i) -> ((i -> i) -> i -> i) -> (i -> i) -> i -> i .The n-th term of this series has a size n+6. The normal form of the first term is f\x\(f (f x)), encoding the numeral 2, while the normal form for the second term is the encoding of the numeral 4. The third lambda-term normalizes to
f\x\(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))which encodes the numeral 16. The fourth lambda-term normalizes to the encoding of the numeral 256. It is easy to show that the n-th term of this series has a lambda-normal given by a stack of 2's as exponents. For small values of n, this increase in the size of terms is dramatic.