call by value: what is a value?

Question

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 λx.x)

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

  (λz.id z)

a value.

Isn't contradictions here? or I am misunderstanding something?

Can anyone clarify these to me?

Thanks in advance!

Answer 1

The set of values is defined for a particular reduction relation. Each reduction relation defines its own set of values.

Reduction for the lambda calculus isn't just beta reduction, there are also context rules. There are several common notions of reduction for the lambda calculus, with different sets of context rules.

In the full lambda calculus, any lambda term with a hole is a context: the context rules are $$ \frac{M \to M'}{M\,N \to M'\,N} \qquad \frac{N \to N'}{M\,N \to M\,N'} \qquad \frac{M \to M'}{\lambda x.M \to \lambda x.M'} $$ This doesn't mimic what most programming languages do. Most programming languages don't start evaluating a function's body before the function receives its arguments (this becomes especially important when evaluating the function body causes side effects). This translates into omitting the third rule above altogether: there is no reduction under a lambda. The reduction relation without that context rule is known as weak head reduction. For weak head reduction, $\lambda x. M$ is a value for any term $M$: even if $M$ could be reduced, $\lambda x. M$ can't.

Call-by-value and call-by-name are refinements of weak head reduction which also restrict the form of terms that rules can be applied to: the first two rules above, and the beta rule, have constraints on the form of $M$ or $N$.

As far as I recall, TAPL focuses on applications of the lambda calculus to programming and so focuses on weak head reduction. (λz.id z) is a value. (id (λz.id z)) isn't a value, which is why the first step reduces it (the first step is id M → id M' where M → M': it's the id in the argument that reduces, not the outer id).