Next: Properties of the Up: Evaluation Previous: The Reduction Rules

## The Reduction Strategy

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