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
-
Firstly that if any evaluation rule terminates when applied to a particular expression then normal-order evaluation also terminates.
-
Secondly, if any two evaluation rules terminate then they give the same result, up to α-conversion.
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.
