The halting problem, in λ-calculus

Why no program can decide whether another program halts — Church's 1936 proof, built one step at a time. Click Next to advance.

1

The question

Some λ-terms reduce to a normal form (they halt). Others don't — like Ω = (λx. x x)(λx. x x), which β-reduces to itself forever.

Could there be a single λ-term H that decides halting? Specifically: a closed term such that for every closed term M: 

H M  →*  true   if M reduces to a normal form
H M  →*  false  if M reduces forever

That would be a programmatic answer to "does this code terminate?" — the dream of every static analyser. We're going to show it can't exist.

2

Suppose H exists

We argue by contradiction. Assume some such H exists. We don't know its definition; we only know its specification — H M reduces to true exactly when M halts.

Using H, we'll build a small λ-term that turns out to be impossible for H to classify.

3

The diagonal trick

Define a term D that takes an input x, asks H whether x x halts, and then deliberately does the opposite: 

D = λx. H (x x) Ω I

Reading this with Church booleans: if H (x x) = true (so x x halts), D picks Ω — the canonical non-terminating term. If H (x x) = false (so x x diverges), D picks I — the identity, which halts trivially.

So D x halts iff x x doesn't.

D — pre-application
4

Now apply D to itself

The contradiction comes from feeding D to itself: 

D D  =  (λx. H (x x) Ω I) D
     →  H (D D) Ω I

This D D term either halts or it doesn't. We'll examine both cases — and both will lead nowhere good for H.

5

Case 1: H says D D halts

Suppose H (D D) = true. By our assumption that means D D halts. Now reduce D D: 

D D  →  H (D D) Ω I  →  true Ω I  →  Ω

But Ω diverges. So D D reduces to a divergent term, meaning D D itself diverges. That contradicts our assumption that it halts.

⚠ contradiction
6

Case 2: H says D D diverges

Now suppose H (D D) = false — D D doesn't halt, according to H. Reduce again: 

D D  →  H (D D) Ω I  →  false Ω I  →  I

But I is the identity — it's already a normal form. So D D halts. That contradicts our assumption that it diverges.

⚠ contradiction
7

Both cases contradict the assumption

Whatever H says about D D, the term itself does the opposite. Since this works for any hypothetical H, the only consistent conclusion is that no such H can exist.

The halting problem is undecidable in λ-calculus.

∎ Q.E.D.
8

What this is, historically

This is essentially Church's 1936 proof that the Entscheidungsproblem is unsolvable. A few months later, Turing proved the same result independently using machines that read and write tape — and the proofs share the same diagonal shape: build a program that contradicts any oracle deciding its own behavior.

The diagonal trick goes back to Cantor (1891) — used to show that the reals are uncountable — and is the same machinery that powers Gödel's incompleteness (1931). Three foundational results in mathematics, all built on the same idea: if there were a decision procedure, you could fool it by asking about itself.

Try Ω in the visualizer ↗

1 / 8