# Joachim Breitner's Homepage

## Interleaving normalizing reduction strategies

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*_{1} and *s*_{2}, consulting them alternately may not yield a normalizing strategy.

Here is an example. Consider the lambda-term *o* = (*λ**x*.*x**x**x*), and note that *o**o* → *o**o**o* → *o**o**o**o* → …. Let *M*_{i} = (*λ**x*.(*λ**x*.*x*))(*o**o**o*…*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*_{1}, which picks the second redex if given*M*_{i}for an*even**i*, and the first (left-most) redex otherwise.*s*_{2}, 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*_{1} and *s*_{2} while trying to reduce *M*_{2}, we get the sequence

*M*_{2} → *M*_{3} → *M*_{4} → …

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.

Have something to say? You can post a comment by sending an e-Mail to me at <mail@joachim-breitner.de>, and I will include it here.