Weak Normalisation Theorem

lambda-calculus

Definition

Weak Normalisation Theorem

The weak normalisation theorem states that repeated normal order reduction always reaches a normal form, if there is one.

Examples

Expression without Normal Form

$$\begin{array}{rl}(\lambda x.xx)[\lambda x.xx]& \to (\lambda x.xx)[\lambda x.xx]\\ & \to (\lambda x.xx)[\lambda x.xx]\\ & \to (\lambda x.xx)[\lambda x.xx]\\ & \to \dots \end{array}$$