CSE 360: Lecture 8

Syntax of lambda-terms

Lambda Prolog has exactly one binding operator, called lambda. In mathematical notion, this binder is written using prefix notation, like lambda x. B. In the concrete syntax of lambda Prolog, this is written with a backslash in infix notation as x \ B. The following are some example lambda-terms.
```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.

Conversion and equality

The rules of alpha-conversion, beta-conversion and eta-conversion are then, respectively, the following operations on terms:
• 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.

These rules are collectively referred to as the lambda-conversion rules. Equality of terms in lambda Prolog is given by lambda-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.

Examples of lambda-Conversion

For example, the following terms are equal within lambda Prolog:
```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.

Natural numbers as lambda-terms

The computation of lambda-normal forms is a rich operation, largely because of the presence of beta-conversion. Lambda-normalization can be used as a computing device itself. In particular, consider the simple signature
```kind i  type.
```
The only closed, simply typed, lambda-normal terms of second-order type
`(i -> i) -> i -> i`
are 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.

Really big lambda-term computations

Consider the series of lambda-terms of which the following are the first four:
```(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.
Lecture Directory / Module Directory / CSE360 Syllabus