Properties of \( \lambda \)-Terms

Core Properties & Lemmas

Let \( r \in \{\beta, \eta, \beta\eta\} \). We analyse reduction paths to determine termination.

• Weakly \( r \)-normalising: \( A \) is weakly \( r \)-normalising iff \( A \twoheadrightarrow_r B \) for some normal form \( B \).
• Strongly \( r \)-normalising: Every possible reduction path terminates.
• Normalisation Lemma: Strong normalisation implies weak normalisation.

Existence and Uniqueness of Values

• Non-existence: Some terms have no \( \beta \)-normal form.
• Uniqueness: If a normal form exists, it is unique.
• Church–Rosser: All terminating paths reach the same normal form.

Reduction Examples

1. Infinite Loop

The term \( (\lambda x.\, x x)(\lambda x.\, x x) \) never reaches a normal form.

2. Term Growth

3. Weak vs Strong

\( (\lambda y.\, z)((\lambda x.\, x x)(\lambda x.\, x x)) \) has:

• a terminating path → \( z \)
• a looping path → infinite reduction