Lambda Calculus: Reduction, Convertibility & Normal Forms

Foundations 1 – Lecture 6 Companion

Clear, step-by-step explanation of β, η, convertibility, and normal forms.

1. Reduction: →r and Multi-Step →→r

A →r B means: A reduces to B in one step using reduction rule r.

Multi-step reduction

→→r is the reflexive and transitive closure of →r.

Formal structure:

A ≡ A₁ →r A₂ →r … →r Aₙ ≡ B

2. r-Convertibility =r

=r is the smallest relation that is:

If A →r B then A =r B

Convertibility allows moving both forward and backward between terms.

3. Compatibility

If A reduces to B, then reductions also work inside larger expressions.

Given Then
A →→r B AC →→r BC
A →→r B λx.A →→r λx.B

4. β and η Reduction

β-Reduction

(λx. M) N →β M[x := N]

η-Reduction

λx. A x →η A

Provided x is not free in A.

5. Normal Forms

β-Normal Form

No β-redex of the form (λx.M) N exists.

η-Normal Form

No expression of the form λx.A x where x is not free in A.

βη-Normal Form

No β-redex and no η-redex inside the term.

Example:

λx. x x

This is in βη-normal form.

6. Summary

Concept Meaning
→r Single reduction step
→→r Zero or more steps
=r Two-way convertibility
r-Normal Form No possible r-reduction