In the 'call by value' evaluation of lambda-calculus, I am bit confused with 'value'.
On page 57 of the book Types and Programming languages, it is said:
The definition of call by value, in which only outermost redexes are reduced and where 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.
So by that definition, a term
λx.x is a value, but a term
λx.((λy.y)x) is not a value since it can be reduced further.
But in an example of 'call by value' on the same page, reduction as the following. (
id is the identity function
id (id (λz.id z)) -------------- id (λz.id z) ------------ λz.id z
But in this example neither
(id (λz.id z))
is a value, nor
Isn't contradictions here? or I am misunderstanding something?
Can anyone clarify these to me?
Thanks in advance!