Next: Properties of the
Up: Evaluation
Previous: The Reduction Rules
As noted in the introduction to this chapter
the evaluation process consists of the repeated selection of a redex
and the application of the appropriate reduction rule to it
until the term is in canonical form.
To make this process definite we need to specify which redex is chosen
if there is more than one possibility.
The goal of this choice should be that as few reductions as necessary are done
to bring the term into canonical form.
Now, whether or not a term is in canonical form depends only on the outer
structure of the term.
For example, the term inl(spread(<1,2>;u,v.u)) is considered to be
in canonical form even though it contains a redex.
Thus, to minimize the number of reductions needed
the choice is made to reduce the outermost redex.
Because of the position of the argument places in noncanonical forms,
this amounts to choosing the leftmost redex when
the term is written out in linear fashion.
Under this strategy the term (
x.<(
y.0)(x),3>)(4)
reduces to <(
y.0)(4),3> after a single application of the
application reduction rule,
whereas under an innermost or
rightmost strategy it would reduce to <0,3>.
This illustrates the lazy nature of this strategy.
Richard Eaton
Thu Sep 14 08:45:18 EDT 1995