Reduction Orders

Topic

As we have seen, often a lambda expression can be reduced in different ways ie there will be more than one reduction that could be applied, at some stage in the reduction, and so, among the possible reductions, there is a choice as to which reduction to apply first.

There are a variety of reduction strategies (left to right, right to left, random, in to out, out to in, in to out left to right, etc.). Among these, two are prominent.

Normal order reduction

The strategy of always reducing the left-most outer-most redex is known as normal order reduction. Roughly this means, reduce the functions first and their arguments later. So, for example, if there is an application, with a lambda abstraction with a scope, reduce that abstraction, putting the arguments into the scope, before reducing the arguments. We saw an example of this where if-then-else was evaluated to a normal form when one of its arguments would not terminate (we never had to evaluate that argument).

Applicative order reduction

The strategy of always reducing the right-most inner-most redex is known as applicative order reduction. Roughly this means, reduce the arguments first and the functions later.

Two theorems to keep in mind.

Church-Rosser I : If a lambda expression has a normal form, that normal form is unique. (Actually Church-Rosser proved that the reduction relation is confluent, and this is a simple consequence of that.)

Church-Rosser II: If a lambda expression has a normal form, then normal order reduction will terminate and find that normal form.

Normal order reduction will not usually be the shortest or optimal reduction of an expression-- in fact for some systems you can even prove that normal order reduction will be the longest reduction. So, on the face of it, you have to balance the guaranteed finding of a normal form (if there is one) together with inefficiency, against possible non-termination (even if there is a normal form) together with efficiency.

Normal order reduction is called 'normal order reduction' because it will find the normal form (if there is one).