- Syntax of lambda-terms
- Conversion and equality
- Examples of lambda-Conversion
- Natural numbers as lambda-terms
- Really big lambda-term computations

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

- Replacing a subterm (lambda x. s) by (lambda y. [y/x]s),
provided y is free for x in s and y is not free in s, is called
*alpha-conversion*. - Replacing a subterm ((lambda x. s) t) by ([t/x]s), provided t is
free for x in s, is called
*beta-reduction*. The converse operation is call*beta-expansion*. These two operations are both called*beta-conversion*. - Replacing a subterm (lambda x. (s x)) by s, provided x is not free
in s, is called
*eta-reduction*. The converse operation is call*eta-expansion*. These two operations are both called*eta-conversion*.

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

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

(((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 (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.

Lecture Directory / Module Directory / CSE360 Syllabus