10 Software
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.
Definition.
A lambda expression is in normal form if no subexpression of it has the form (λx.P Q).
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.
Definition
A lambda expression E is in head normal form iff E is λx1.λx2...λxn.E' where E' itself is not a redex and (n>=0) ( note here that in the case where n=0 this covers both variables and applications where the function is not an abstraction).
Anything in normal form is in head normal form, but not vv. (For example, λx.(x (λy.y z)) is in head normal form but not in normal form.)
Definition
A lambda expression E is in weak head normal form iff either
either i) E itself is not a redex.
or ii) E is λx.E' for any E'.
Anything in head normal form is in weak head normal form, but not vv. (For example, λx.(λy.y z) is in weak head normal form but not in head normal form.)
Weak head normal form is the important notion-- this is to do with avoiding the capture of free variables, we will see the details later.
Rough characterization.... i) if no more reductions can be done the expression is in normal form. Suppose some reductions can be done, this can either be at the 'top' level if the expression is an application or 'internal' if the expression is an application or an abstraction. For all these definitions the top level reductions simply have to be made. It is the internal reductions that are of interest ii) if the expression is an application, say (P Q), or an abstraction whose inner scope is (P Q), and where P or Q or both are individually reducible, the expression is in head normal form. Finally, iii) even abstractions λx.(P Q) with P Q reducible are in weak head normal form.
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.
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)
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*)
Definition
Two lambda expressions are equal or equivalent iff they reduce to each other or to some common form.