Slide 12.11: Reduction strategies

Slide 12.10: β-reduction
Slide 12.12: Reduction strategies (cont.)
Home

Reduction Strategies

There may be a choice of two or more applications in an expression. For example, the following expression can be reduced by two different paths:

    ( λx . λy . ( add y ( ( λz . ( mul x z ) ) 3 ) ) ) 7 5
 ⇒_β ( λy . ( add y ( ( λz . ( mul 7 z ) ) 3 ) ) ) 5
 ⇒_β ( add 5 ( ( λz . ( mul 7 z ) ) 3 ) )
 ⇒_β ( add 5 ( mul 7 3 ) ) = ( add 5 21 ) = 26

    ( λx . λy . ( add y ( ( λz . ( mul x z ) ) 3 ) ) ) 7 5
 ⇒_β ( λx . λy . ( add y ( mul x 3 ) ) ) 7 5
 ⇒_β ( λy . ( add y ( mul 7 3 ) ) ) 5
 =  ( λy . ( add y 21 ) ) 5
 ⇒_β ( add 5 21 ) = 26

The strategy for determining which application to carry out next is called an evaluation rule. There are two rules commonly used:

Strict evaluation or call by value: It requires the evaluation of an actual parameter before it is passed to, or substituted in, a function. It corresponds to passing parameters by value in a language such as Pascal.

Normal-order evaluation or call by name: It specifies that the left-most, outer-most application of an expression be carried out at each step. An actual parameter is not evaluated before being passed to a function. It corresponds to passing parameters by name, as in Algol-60.

For example, the expression terminates by using normal-order evaluation:

    ( λx . 7 )  ( ( λx . x x ) ( λy . y y ) ) ⇒_β 7

The expression does not terminates by using strict evaluation:

    ( λx . 7 )  ( ( λx . x x ) ( λy . y y ) ) 
 ⇒_β ( λx . 7 )  ( ( λy . y y ) ( λy . y y ) )
 ⇒_β …