No Lambda Normal Form

Question

How can we show that the term $\Omega = (\lambda x.x\ x)\ (\lambda x.x\ x)$ does not have a normal form? Building on this, what is an example term different than Omega that is not normalizing (meaning a term that every reduction sequence starting from it is infinite)?

Answer 1

If a term has a normal form then there is a sequence of $\beta$-reductions leading to it. However, $\Omega$ has only one $\beta$-redex, which leads back to $\Omega$. Therefore, because $\Omega$ is not already in normal form it has no normal form.

It is easy to generate other terms that have only infinite chains of reductions. For instance, the related $Y$ combinator $Y = \lambda f . (\lambda x . (f (x x)) (\lambda x . (f (x x))$ gives $$Y \to \lambda f . f Y \to \lambda f . f(f Y) \to \lambda f . f(f(f Y)) \to \cdots$$ Note that by applying $Y$ to a specific $f$ we may get a normalizing term (because for a specific $f$ there will be additional reductions that may lead to a normal form). In fact, $Y$ is quite useful because for any term $g$ we have $Y g = g (Y g)$, so $Y$ computes fixed points.

Answer 2

It's very easy to show that $\Omega$ has no normal form, because there's only one way to reduce it: $\Omega = (\lambda \color{magenta}{x}. \color{magenta}{x} \color{magenta}{x}) \color{magenta}{(\lambda x. x x)} \to_\beta (\lambda x. x x) (\lambda x. x x) = \Omega$. The set of lambda terms that $\Omega$ reduces to is the singleton $\{\Omega\}$. Since $\Omega$ reduces, it is not in normal form, so it does not reduce to any term in normal form.

More generally, a term is non-normalizing iff no sequence of reduction from this term ends in a normal form, i.e. every reduction sequence is infinite. There are two ways a reduction sequence can be infinite: it can either loop back at some point ($M_0 \to_\beta M_1 \to_\beta \ldots \to_\beta M_n \to_\beta \ldots M_{n+k} = M_n $), or it can involve infinitely many different terms (in which case the terms have to grow larger asymptotically, because there are only finitely many distinct terms of any specific finite size). More formally, the sequence of expansions either repeats or doesn't repeat. Of course, from a given term, it's possible to have some sequences that reach a normal form, others that repeat and yet others that reach infinitely many terms, depending on the choice of regex at each stage.

You can build simple examples of looping or growing terms by tweaking $\Omega$. For example, $(\lambda x. I x x) (\lambda x. I x x)$ can loop in various ways: $$ \begin{align*} (\lambda \color{red}{x}. I \color{red}{x} \color{red}{x}) \color{red}{(\lambda x. I x x)} \to_\beta & I (\lambda x. I x x) (\lambda x. I x x) \to_\beta (\lambda x. I x x) (\lambda x. I x x) \\ (\lambda x. I x x) (\lambda x. \color{blue}{I} \color{blue}{x} x) \to_\beta & (\lambda x. I x x) (\lambda x. x x) \to_\beta I (\lambda x. x x) (\lambda x. x x) \\ (\lambda x. \color{green}{I} \color{green}{x} x) (\lambda x. I x x) \to_\beta & (\lambda x. x x) (\lambda x. I x x) \to_\beta (\lambda x. I x x) (\lambda x. I x x) \\ \end{align*} $$ And here's a straightforward example of a term that keeps growing: $$ (\lambda x y. x x) (\lambda x y. x x) \to_\beta \lambda y_1. (\lambda x y. x x) (\lambda x y. x x) \to_\beta \lambda y_2. (\lambda y_1. (\lambda x y. x x) (\lambda x y. x x)) \to_\beta \ldots $$

With a programmer's intuition, you get a growing chain with a recursive function that keeps using more and more memory, and a looping chain with a recursive function that works in bounded memory (typically obtained through tail recursion).

The shape of the reductions of a term is captured by its Böhm tree. A term has a normal form iff its Böhm tree is finite; if a term lacks a normal form then at least one of its branches is infinite, either by growing indefinitely or by looping back to a node in the tree.

There are also non-syntactic ways of characterizing terms without normal forms. For example, with intersection types, you can characterize the terms without a normal form: they are terms that lack a type without $\top$ (i.e. a term has a normal form iff it has a type without $\top$). Of course, type checking is undecidable for intersection types.