Call by value in the lambda calculus

问题:

I'm working my way through Types and Programming Languages, and Pierce, for the call by value reduction strategy, gives the example of the term id (id (λz. id z)). The inner redex id (λz. id z) is reduced to λz. id z first, giving id (λz. id z) as the result of the first reduction, before the outer redex is reduced to the normal form λz. id z.

But call by value order is defined as 'only outermost redexes are reduced', and 'a redex is reduced only when its right-hand side has already been reduced to a value'. In the example id (λz. id z) appears on the right-hand side of the outermost redex, and is reduced. How is this squared with the rule that only outermost redexes are reduced?

Is the answer that 'outermost' and 'innermost' only refers to lambda abstractions? So for a term t in λz. t, t can't be reduced, but in a redex s t, t is reduced to a value v if this is possible, and then s v is reduced?

回答1:

Short answer: yes. You can never reduce inside a lambda-term you can only reduce term outside, starting by right.

The set of evaluation contexts in lambda-calculus by value is defined as follow:

E = [ ] | (λ.t)E | Et

E is what you can value..

For example in lambda calculus by name the evaluation context is :

E = [ ] | Et | fE

as you can reduce an application even if a term is not a value. For example (λx.x)(z λx.x) is stuck in call by value but in call by name it reduce to (z λx.x), which is a normal form.
In the context grammar f is a normal form (in call by name) defined as:

f = λx.t | L  
L = x | L f

You can see another definition of contexts at chapter 19.5.3 of the Pierce.

回答2:

Is the answer that 'outermost' and 'innermost' only refers to lambda abstractions? So for a term t in λz. t, t can't be reduced, but in a redex s t, t is reduced to a value v if this is possible, and then s v is reduced?

Yes, that's exactly right.