Reduction Strategies (Cont.)


An example of the call by value reduction is given as follows:
   (λx.(λf.f(succ x)) (λz.(λg.(λy.(add (mul(g y) x)) z))))
       ((λz.(add z 3)) 5)
 ⇒β (λx.(λf.f(succ x))
       (λz.(λg.(λy.(add (mul (g y) x))) z))) (add 5 3)
 ⇒βx.(λf.f(succ x)) 
       (λz.(λg.(λy.(add (mul (g y) x))) z))) 8βf.f(succ 8)) (λz.(λg.(λy.(add (mul (g y) 8))) z))β (λz . (λg . (λy . (add (mul (g y) 8))) z)) (succ 8 )
 ⇒βz . (λg . (λy . (add (mul (g y) 8))) z)) 9β (λg . (λy . (add (mul (g y) 8))) 9) z
The reduction of the argument, ((λz.(add z 3)) 5), can be thought of as an optimization, since we pass in a value and not an unevaluated expression that would be evaluated twice in the body of the function.

Church-Rosser Theorem
The Church-Rosser theorem states Thus, normal-order evaluation is the most general evaluation rule of all. A functional programming language having the effect of normal-order evaluation is often called lazy. There is an efficient implementation of normal-order evaluation called call by need which can be used in functional languages. The idea is to pass an actual parameter to a function in unevaluated form. If the function needs to evaluate the parameter, it does so but it also overwrites the parameter so that it need not be reevaluated later.