1. Normalisation Concepts
Let \( r \in \{\beta, \eta, \beta\eta\} \).
- Weakly \( r \)-normalising: \( A \) is weakly \( r \)-normalising iff \( A \twoheadrightarrow_r B \), where \( B \) is in \( r \)-normal form.
- Strongly \( r \)-normalising: Every possible reduction path from \( A \) terminates.
Lemma.
If \( A \) is strongly \( r \)-normalising, then
\( A \) is weakly \( r \)-normalising and has an \( r \)-normal form.
2. Uniqueness and Confluence
The Church–Rosser Property
If a term reduces to \( B_1 \) and \( B_2 \), then \( B_1 \equiv_\alpha B_2 \). Hence, if a normal form exists, it is unique.
Confluence:
Different reduction orders lead to the same result if they terminate.
3. Reduction Behaviour
A. Non-terminating Terms
The term \( (\lambda x.\, x x)(\lambda x.\, x x) \) is not weakly \( \beta \)-normalising.
B. Growing Terms
\[
(\lambda x.\, x x x)(\lambda x.\, x x x)
\;\to_\beta\;
(\lambda x.\, x x x)(\lambda x.\, x x x)(\lambda x.\, x x x)
\;\to_\beta\; \dots
\]
C. Path Dependency
- Term: \( (\lambda y.\, z)((\lambda x.\, x x)(\lambda x.\, x x)) \)
- Path 1: outer reduction \( \to z \) (terminates)
- Path 2: inner reduction loops forever
4. Strategy & Notation
A safe reduction strategy guarantees finding the normal form whenever one exists.
All reduction orders of
\( (\lambda x y z.\, x z (y z))(\lambda x.\, x)(\lambda x.\, x) \)
converge to:
\[
\lambda z.\, z z
\]
Left associativity:
\( x z (y z) \) means \( (x z)(y z) \).