9/17/19
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). There are two ways of identifying which redex to reduce as the way toward NOR. If the written out formula is scanned from left to right, the first redex that is met is the redex to reduce (then, the resulting new expression is scanned from left to right and the first redex met is the one to reduce... and so on). A slightly different approach is to look for redexes that are not contained within other redexes (i.e. they are not strict subeexpressions of other redexes) then reduce the leftmost one of those, and repeat until there are no redexes left.
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. As a recipe:- look for redexes that do not contain other redexes (i.e. they do not have any strict subeexpressions which are redexes) then reduce the rightmost one of those, and repeat until there are no redexes left.
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).