Normal forms

Normalization is the process of reducing a term to a “simpler” form. For instance, in most arithmetics 0 + 0 is not in normal form, because we could reduce it to 0.

Note that reducing a term might not always lead to a normal form. Indeed, the term (\x . x x) (\y . y y) has no normal form, despite the fact that it can be reduced. For this reason, the untyped Lambda Calculus is not normalizing, that is, there are terms that don’t have a normal form.

Normalizing Systems

There is a heirachacy of exactly how “normal” a system is.

1. Not normalizing: there are terms that can’t be reduced to a normal form.
2. Weakly normalizing: Each term can be reduced to a normal form
3. Strongly normalizing: Each term must be reduced to a normal form, that is, there are no infinite reduction sequences.
4. Canonical: Each term is already in normal form