I'm currently reading Benjamin C. Pierce's “Types and Programming Languages”. Before really getting into type theory it explains lambda calculus and evaluation strategies.
I am a bit confused by the explanation of call by name vs call by value in this context.
The two strategies are explained in the following manner:
call by name
Like normal order in that it chooses the leftmost, outermost redex first, but more restrictive by not allowing reductions inside abstractions. An example:
id (id (λz. id z)) → id (λz. id z) → λz. id z
call by value
Only the outermost redexes are reduced and a redex is reduced only when its right-hand side has already been reduced to a value—a term that is finished computing and cannot be reduced any further. An example:
id (id (λz. id z)) → id (λz. id z) → λz. id z (identical to the call by name evaluation)
Ok, so far so good. But this is followed by the following paragraph:
The call-by-value strategy is strict, in the sense that the arguments to functions are always evaluated, whether or not they are used by the body of the function. In contrast, non-strict (or lazy) strategies such as call-by-name and call-by-need evaluate only the arguments that are actually used.
I know what call-by-value and call-by-name means practically, from having used (among others) C and Haskell, but I cannot see why the evaluation strategy explained above leads to this in the lambda calculus. Is this an additional rule that always accompany call-by-value, or does if follow from the reduction strategy outlined above?
Especially since the reduction steps in the examples are identical, I fail to see the difference between the two strategies and would love if someone could help me gain some intuition.