More about evaluation

Reading: TAPL 5.3.

Operational semantics

Page 72 gives evaluation rules for the call-by-value λ-calculus. If we want to use evaluation contexts, they are defined as:

E ::= [⋅]
      E1 t2
      v1 E2

Then we can replace the congruence rules (E-App1 and E-App2) with the single rule:

   t ⟶ t'
――――――――――――――  (E-Context)
E[t] ⟶ E[t']

Evaluation strategies

Earlier (p. 56), you read about several evaluation strategies. It may seem rather arbitrary to pick one evaluation order out of many, so here are some additional remarks on why it’s actually not so bad.

Full β-reduction

The original definition of λ-calculus allows β-reduction to occur anywhere (full β-reduction, p. 56). This means that the evaluation relation is nondeterministic, because there are terms that have more than one place where β-reduction can be done. So, what should we do if two different evaluation paths end in two different normal forms? (Cf. nondeterministic Turing machines, where we said that the machine accepts iff at least one path accepts).

The good news is that this cannot happen, because β-reduction is confluent: if a ⟶* b and a ⟶* c, then there exists some d such that b ⟶* d and c ⟶* d (also known as the Church-Rosser theorem). In other words, whenever a path forks into two paths, there’s always a way to rejoin them. In particular, this means that every term has at most one normal form.

Normal-order evaluation

But it can happen that a term has some paths that lead to a normal form and some paths that do not. Such terms are called weakly normalizing but not strongly normalizing. For example, the term (λx. λy. y) Ω is weakly normalizing but not strongly normalizing.

Fortunately, normal-order evaluation (“the leftmost, outermost redex is reduced first”) is deterministic and is guaranteed to find a normal form if there is one.

Call-by-name evaluation

Call-by-name evaluation is similar to normal-order evaluation, except that we do not perform reductions inside lambdas. Because normal-order evaluation reduces outermost redexes first, it must be that a normal-order evaluation that results in a value always starts with a call-by-name evaluation [2]:

t ⟶* v  iff  t ⟶* v' ⟶* v
  nrm            cbn     nrm

(The fact that v' is an intermediate step in the normal-order evaluation from t to v isn’t stated by Plotkin, but the proof is exactly the same as his Corollary 4.1.)

So call-by-name evaluation is just normal-order evaluation that stops as soon as it reaches a value.

Call-by-value evaluation

To get to call-by-value, we back up to full β-reduction, then restrict to βᵥ-reduction [2], which, as mentioned briefly earlier, can only happen when the argument is a value. Another way of thinking about this restriction is in terms of what variables can be bound to: in the strategies above, variables can be bound to any terms, but under βᵥ-reduction and the strategies below, variables can only be bound to values.

βᵥ-reduction has some key properties in common with β-reduction:

• Full βᵥ-reduction is confluent, and it is weakly but not strongly normalizing.

• There is an evaluation strategy that always finds a βᵥ-normal form: “Find the leftmost, outermost subterm that contains a call-by-value redex; that redex is reduced first.” I don’t know if this strategy has a name; let’s call it βᵥ-normal-order evaluation.

• If a βᵥ-normal-order evaluation results in a value, it must begin with a call-by-value evaluation [1:55,2]:

  t ⟶* v iff t ⟶* v' ⟶* v
    nrmv         cbv     nrmv

  where nrmv means βᵥ-normal-order evaluation.

Summary

	Arguments can be any terms	Arguments must be values
Reduce anywhere	Full β	“Full βᵥ”
Finds a normal form	normal-order	“βᵥ-normal-order”
Stops when term is a value	call-by-name	call-by-value

References