Joachim Breitner's Homepage

A little, not very significant, observation about lambda calculus and reduction strategies.

A reduction strategy determines, for every lambda term with redexes left, which redex to reduce next. A reduction strategy is normalizing if this procedure terminates for every lambda term that has a normal form.

A fun fact is: If you have two normalizing reduction strategies s₁ and s₂, consulting them alternately may not yield a normalizing strategy.

Here is an example. Consider the lambda-term o = (λx.xxx), and note that oo → ooo → oooo → …. Let M_i = (λx.(λx.x))(ooo…o) (with i ocurrences of o). M_i has two redexes, and reduces to either (λx.x) or M_i + 1. In particular, M_i has a normal form.

The two reduction strategies are:

• s₁, which picks the second redex if given M_i for an even i, and the first (left-most) redex otherwise.
• s₂, which picks the second redex if given M_i for an odd i, and the first (left-most) redex otherwise.

Both stratgies are normalizing: If during a reduction we come across M_i, then the reduction terminates in one or two steps; otherwise we are just doing left-most reduction, which is known to be normalizing.

But if we alternatingly consult s₁ and s₂ while trying to reduce M₂, we get the sequence

M₂ → M₃ → M₄ → …

which shows that this strategy is not normalizing.

Afterthought: The interleaved strategy is not actually a reduction strategy in the usual definition, as it not a pure (stateless) function from lambda term to redex.