5
$\begingroup$

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!

$\endgroup$
6
$\begingroup$

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

$\endgroup$
  • $\begingroup$ "this becomes especially important when evaluating the function body causes side effects" Indeed! And fixed point combinators could also diverge, in practice, if we insist on reducing under lambdas. $\endgroup$ – chi Jun 28 '16 at 17:22
  • $\begingroup$ I think now I understood the value and call by value stuff. I read all these things before, but haven't read their connections as you explained. Thanks! $\endgroup$ – alim Jun 29 '16 at 5:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.