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: 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 ) )
 ⇒β