Normal Forms and Termination


Our main weapon is going to be beta-reduction (i.e. simple function application). The sub-expression which gets reduced is known as a redex. When you keep beta-reducing an expression you may reach the stage where there are no further reductions to be done.


A lambda expression is in normal form if no subexpression of it has the form (λx.P Q). [An expression is considered to be a subexpression of itself.]

That is, it is in normal form if no further beta reductions can be done.

There are other concepts too, which will be important later.

When you set out doing beta-reductions on an expression, usually you will have a choice of which sub-expression to reduce first. Hence, there arises the notion of a reduction path. Various theorems have been proved here (and we may look at some of them later). Important to know is that all reduction paths which produce a normal form for an expression, produce the same normal form. Any reduction sequence for an expression that terminates, produces the same normal form. And it is never necessary to backtrack; that is to say, if there is a normal form it is always reachable by further reductions no matter what reductions you have performed to that point.

The Church-Rosser First Theorem: value of normal form does not depend on order, if reduction terminates it provides a unique normal form.

(We would expect this from our experience of arithmetic and algebra.) In arithmetic, for example, with an expression like (2+3).(4+5) we know we get the same value if we go (5).(4+5) to (5)(9) to 45, or (2+3).(9) to (5).9 to 45 ie the result does not depend on the order of evaluation. The same is true for lambda calculus (with the proviso of termination, which we will talk about shortly).

There are non-terminating reduction sequences; and there are expressions which have both terminating and non-terminating reduction sequences.

Some examples... Consider λx.(x x) (* a self-application function *) and apply it to itself

(λx.(x x) λx.(x x))

this beta reduces to (λx.(x x) λx.(x x)) which is just itself, so clearly there can be a non-terminating beta-reduction sequence here. This expression does not have a normal form.

We can now make this non-terminating expression an inessential part of something else. Consider λx.λy.y, when this is applied successive to two arguments it will consume both of them and return the second (ignoring the first). So, for example, ((λx.λy.y a) b) will reduce to b. So let us construct an expression like this which has our non terminating expression as the first argument and something innocent as the second

((λx.λy.y ((λx.(x x)) λx.(x x)) b)

if we beta reduce this from the entire of the first application, the reduction goes

((λx.λy.y ((λx.(x x)) λx.(x x)) b)

((λy.y) b)


so this expression has a normal form, namely b, and a terminating reduction sequence. If, on the other hand, we choose to reduce the first argument first, reduction goes on forever.

((λx.λy.y ((λx.(x x)) λx.(x x)) b) (* here the underlined piece reduces to itself. *)

((λx.λy.y ((λx.(x x)) λx.(x x)) b)

Convince yourself of the following:-

a) (λx.(x x) λx.(x x)) can be rewritten forever
b) ((λx.λy.y a) b) ⇒ b
c) ((λx.λy.y (λx.(x x) λx.(x x))) b) ⇒ b (*this is like (b) except that we have put self-application in for the argument 'a'.*)
d) ((λx.λy.y (λx.(x x) λx.(x x))) b) ⇒ b (*same as (c) but show it can be rewritten forever*)