More about evaluation (graduate only)

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

Why “at most”? Some terms, like Ω ≡ (λx. x) (λx. x), have no normal form. No matter how you try to reduce it, it always stays the same:

(λx. x) (λx. x)
⟶ (λx. x) (λx. x)
⟶ ...

It can also happen that a term has some paths that lead to a normal form and some paths that do not, like (λx. λy. y) Ω.

If all the evaluation paths of a term lead to a normal form, it is called strongly normalizing. If some of the paths lead to a normal form, it is called weakly normalizing. So (λx. λy. y) Ω is weakly normalizing but not strongly normalizing. Ω is neither weakly nor strongly normalizing.

It would be a problem if a term had a normal form but we didn’t know how to find it. Fortunately, there is a simple, deterministic evaluation strategy that is guaranteed to find a normal form if there is one. In normal-order evaluation, the leftmost, outermost redex is reduced first. For example, in (λx. λy. y) Ω, there are two redexes, (λx. λy. y) and Ω. Since (λx. λy. y) is leftmost, it is reduced first.

Call-by-name evaluation

Call-by-name evaluation is similar to normal-order evaluation, except that we do not perform reductions inside lambdas. Intuitively, this means that a function only starts running after we call it.

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 can be thought of as similar to normal-order evaluation, but it 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 we mentioned briefly earlier. In βᵥ-reduction, the argument of a redex must be a value. Another way of thinking about this restriction is in terms of what variables can be bound to: in full β-reduction and call-by-name, 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. So call-by-value evaluation can be thought of as similar to βᵥ-normal-order evaluation, but it stops as soon as it reaches a value.

Summary

References