Normalization property

Remarks

A strongly normalizing system is weakly normalizing. Indeed, from any $a$, follow reduction steps as long as possible; the path is finite, so it ends in a normal form.

Example: let $A = \N$ and $n \to n - 1$ for $n \ge 1$. Every path from $n$ has exactly $n$ steps, so the system is strongly normalizing, and $0$ is the only normal form.

Non-example: let $A = \set{a, b}$ with $a \to a$ and $a \to b$. The element $a$ has the normal form $b$, so the system is weakly normalizing. It is not strongly normalizing, because $a \to a \to a \to \cdots$ is infinite.

In the untyped lambda calculus with $\beta$-reduction, $(\lambda x.\, x\, x)(\lambda x.\, x\, x)$ has no normal form, so the system is not weakly normalizing.