Lambda Calculus: Reductions, Normal Forms, and Normalisation

A gentle, self-contained explanation of the key ideas from a classic lambda calculus lecture: β, η, and βη reduction, normal forms, and weak vs strong normalisation.

Contents

1. Lambda terms and redexes

In the untyped lambda calculus, every expression (called a term) is built from:

A redex (reducible expression) is a part of a term where a reduction rule can be applied. Different reduction rules give different kinds of redexes (β-redexes, η-redexes, etc.).

Idea: A redex is a “computable spot” in the term – a place where we can take a step of evaluation.

2. β-reduction, η-reduction, and βη-reduction

2.1 β-reduction (function application)

β-reduction is the basic notion of function application in lambda calculus. It says: if you have a function λx.M and you apply it to an argument N, you can substitute N for x in M.

β-redex: An expression of the form (λx.M) N.
β-reduction step: (λx.M) N →β M[x := N] (substitute N for x in M).
Example (β-reduction):
(λx.x) y →β y
Here, (λx.x) y is a β-redex. We replace x by y in the body x, giving y.

2.2 η-reduction (extensionality for functions)

η-reduction captures the idea that two functions are the same if they behave the same on all inputs. In lambda calculus, this is expressed by the rule:

η-redex: An expression of the form λx.(A x) where x does not occur free in A.
η-reduction step: λx.(A x) →η A (when x is not free in A).

Intuitively, λx.(A x) is a function that takes an argument x and just passes it to A. If x is not used inside A itself, then this function is “the same as” A as a function.

Example (η-reduction):
λx.(z x) →η z (assuming x is not free in z).
Here, λx.zx is an η-redex.

2.3 Combining them: βη-reduction

Often we want to treat β- and η-reduction as part of one combined reduction system. The lecture defines:

Combined step: If A →β B or A →η B, we write A →βη B.
In words: →βη is “one step of either β or η reduction”.

So →βη is just a convenient shorthand for “a single step that is either β or η”.

3. Multi-step reduction and convertibility

3.1 Multi-step reduction (reflexive, transitive closure)

A single step A →r B (for some reduction r) means “one reduction step”. But in practice, we usually perform many steps. To talk about “zero or more steps”, we use the reflexive, transitive closure.

Multi-step reduction:
A →→r B means that B can be reached from A by zero or more r-steps.
Formally, →→r is the reflexive, transitive closure of →r.

For the combined system, the lecture defines:

βη multi-step reduction:
→→βη is the reflexive, transitive closure of →βη.
So A →→βη B means “A reduces to B by zero or more β or η steps”.

3.2 Convertibility (equivalence via reduction)

Sometimes we want to say that two terms are “the same” up to reduction, allowing steps in both directions. This is called convertibility.

βη-convertibility:
A =βη B means that A and B are related by the reflexive, symmetric, transitive closure of →βη.
In other words, you can go from A to B by a sequence of β or η steps, possibly forwards or backwards.

This makes =βη an equivalence relation: it is reflexive, symmetric, and transitive.

3.3 Extensionality via η-conversion

The lecture highlights that η-conversion gives us a form of extensionality for functions:

Extensionality principle:
For a variable v that is free in both A and B, if A v =βη B v, then A =βη B.
In words: if two functions give the same result on the same argument (up to βη-convertibility), then the functions themselves are βη-convertible.

This is exactly the idea that “functions are equal if they behave the same on all inputs”.

4. Normal forms: β, η, and βη

A term is in normal form (for a given reduction system) if it cannot be reduced any further using that system. Think of it as “fully evaluated” with respect to that kind of reduction.

4.1 β-normal form

β-normal form:
A term A is in β-normal form if there are no β-redexes in A.
Equivalently, there is no B such that A →β B.
Examples:
• λx.zx is in β-normal form (no (λx.M) N inside).
• (λyx.yx) z is not in β-normal form, because (λyx.yx) z is a β-redex.

4.2 η-normal form

η-normal form:
A term A is in η-normal form if there are no η-redexes in A.
Equivalently, there is no B such that A →η B.
Examples:
• λx.zx is not in η-normal form, because λx.zx is an η-redex and can reduce to z.
• λx.xx is in η-normal form, because λx.(x x) is not an η-redex (the variable x is free in x).

4.3 βη-normal form

βη-normal form:
A term A is in βη-normal form if it has no β-redexes and no η-redexes.
Equivalently, there is no B such that A →βη B.
Example:
λx.xx is in βη-normal form: it has no β-redex and no η-redex.

4.4 Unified definition

Let r ∈ {β, η, βη}.
A term A is in r-normal form iff there are no r-redexes in A, i.e. there is no B such that A →r B.

In short: “in r-normal form” means “no more r-steps are possible”.

5. “Has a normal form” vs “is in normal form”

There is an important distinction between:

Let r ∈ {β, η, βη}.
A term A has an r-normal form B if:
Example (has β-normal form):
Consider (λxyz.xyz)(λx.xx)(λx.x) x.
This term is not in β-normal form (it has β-redexes), but it can be reduced (by β-steps) to x, which is in β-normal form.
So the term has a β-normal form (namely x), even though it is not itself in β-normal form.
Example (no β-normal form):
Consider (λx.xx)(λx.xx).
This term is not in β-normal form, and it reduces to itself forever: 
(λx.xx)(λx.xx) →β (λx.xx)(λx.xx) →β (λx.xx)(λx.xx) → …
There is no term B in β-normal form such that (λx.xx)(λx.xx) =β B.
So it does not have a β-normal form.
Key idea:
• “In normal form” = already fully reduced.
• “Has a normal form” = there exists some reduction path that eventually reaches a fully reduced term.

6. Weakly vs strongly normalising terms

Now we look at how terms behave under repeated reduction. Do they always terminate? Can they terminate at least once? Or do they loop forever?

6.1 Strongly normalising

Let r ∈ {β, η, βη}.
A term A is strongly r-normalising (or “always r-terminates”) if there are no infinite r-reduction sequences starting from A.
In other words, every possible way of repeatedly applying r-steps to A eventually stops.
Example (not strongly β-normalising):
(λx.xx)(λx.xx) is not strongly β-normalising, because we have an infinite β-reduction sequence: 
(λx.xx)(λx.xx) →β (λx.xx)(λx.xx) →β (λx.xx)(λx.xx) → …

6.2 Weakly normalising

A term A is weakly r-normalising (or “weakly r-terminates”) if there exists some term B in r-normal form such that:
A →→r B.
That is, there is at least one reduction path from A that terminates in an r-normal form.
Example (weakly β-normalising):
Consider (λx.xx)(λy.y) z.
We can reduce it by β-steps to z: 
(λx.xx)(λy.y) z →→β z
Since z is in β-normal form, the original term is weakly β-normalising.

6.3 Relationship between strong and weak normalisation

Lemma: If A is strongly r-normalising, then:

Intuitively, if every reduction path from A terminates, then in particular there is at least one terminating path, and it must end in an r-normal form.

Key difference:
• Strongly normalising = all reduction paths terminate.
• Weakly normalising = at least one reduction path terminates.
A term can be weakly normalising but not strongly normalising.

7. Properties of terms and uniqueness of normal forms

The lecture then asks a series of conceptual questions about terms and their behaviour under reduction:

The answers are subtle but very important.

7.1 Not all expressions have normal forms

As we saw, some terms loop forever and never reach a normal form. For example:

Non-terminating term:
(λx.xx)(λx.xx) has no β-normal form and is neither weakly nor strongly β-normalising.

7.2 Uniqueness of normal forms

The lecture states an important fact:

Uniqueness of normal forms:
For r ∈ {β, η, βη}, if an r-normal form exists for a term, then it is unique (up to syntactic equality).

In other words, if:

then B₁ and B₂ must be the same term (often written B₁ ≡ B₂).

Intuition:
Even though there may be many different ways to reduce a term, if you manage to reach a normal form, that final “fully evaluated” result is uniquely determined.

7.3 Dependence on reduction order

The lecture also emphasises that:

Important:
Having a normal form does not guarantee that every reduction strategy will find it. Some strategies may loop forever even though a normal form exists.

8. Reduction strategies and termination

Because the order of reduction matters, we care about reduction strategies: systematic ways of choosing which redex to reduce next.

The lecture notes that:

In lambda calculus, a well-known example of such a strategy is normal-order reduction (always reduce the leftmost, outermost redex first). A key result (not fully developed here) is:

Idea (informal):
If a term has a normal form, then normal-order reduction will find it.

This is extremely important for programming languages: it means that if a program has a final value, there is a systematic way of evaluating it that is guaranteed to reach that value.

Summary