The Halting Problem

In 1936, five years after Gödel shattered Hilbert's dream of completeness, Alan Turing attacked the third pillar — decidability. Could there be a mechanical procedure that, given any mathematical statement, determines whether it is provable?

Turing's answer was no. And the way he proved it gave us the modern concept of computation itself.

Turing machines: a model of computation

To prove that something cannot be computed, you first need a precise definition of what computation means. Turing provided one.

A Turing machine is an abstract device consisting of:

An infinite tape divided into cells, each holding a symbol.
A head that reads and writes symbols on the tape.
A finite set of states, including a designated start state and one or more halt states.
A transition function that, given the current state and the symbol under the head, specifies: what symbol to write, which direction to move the head, and what state to enter next.

The machine starts, follows its rules, and either eventually reaches a halt state (it halts) or runs forever.

Turing's thesis — now called the Church–Turing thesis — asserts that this simple model captures everything that can be computed by any mechanical process. Every algorithm, every programme, every computation that any physical computer can perform can be simulated by a Turing machine. This thesis is not a theorem (it cannot be proved, since "mechanical process" is informal), but it has withstood decades of scrutiny and is universally accepted.

The problem

The Halting Problem asks:

Given a programme P and an input I, does P eventually halt when run on I, or does it run forever?

This is a completely natural question. Every programmer has stared at a running process and wondered: will this terminate, or is it stuck in an infinite loop? The Halting Problem asks whether this question can be answered in general, by an algorithm, for all possible programmes and inputs.

The proof: the Halting Problem is undecidable

Theorem (Turing, 1936). There is no Turing machine that, given any programme P and input I, correctly determines whether P halts on I.

The proof is a diagonal argument — a close relative of Cantor's proof that the reals are uncountable and of Gödel's self-referential construction.

The argument

Assume, for contradiction, that a halting oracle H exists. H is a programme that takes two inputs — a programme P and an input I — and:

Outputs "halts" if P halts on I.
Outputs "loops" if P runs forever on I.

H always terminates and is always correct.

Now construct a new programme D (the "diagonaliser"):

programme D(P):
    if H(P, P) == "halts":
        loop forever
    else:
        halt

D takes a programme P as input, asks H whether P halts when given itself as input, and then does the opposite.

Now ask: what happens when we run D on itself? That is, what is D(D)?

Case 1: Suppose H(D, D) = "halts". Then D(D) enters the infinite loop branch and runs forever. But H said it halts — contradiction.
Case 2: Suppose H(D, D) = "loops". Then D(D) enters the halt branch and terminates. But H said it loops — contradiction.

Both cases lead to contradiction. Therefore, our assumption that H exists must be false. No halting oracle exists. ∎

Why the proof works

The beauty of this proof is its simplicity. It requires no deep mathematics — just the ability to treat programmes as data (passing a programme to itself as input) and the assumption that H exists.

The core mechanism is self-reference: we feed D to itself, creating a statement that effectively says "I do the opposite of what you predict." This is the same diagonal trick that powers Gödel's theorem and Cantor's proof. Self-reference is the engine of impossibility.

Consequences and generalisations

The Halting Problem is the root of a vast tree of undecidability results in computer science:

Programme analysis

If we could solve the Halting Problem, we could answer almost any question about programme behaviour:

Does this programme ever access array index out of bounds?
Does this function return the correct output for all inputs?
Does this programme contain a security vulnerability?
Are these two programmes equivalent?

All of these are undecidable in general. Each can be reduced to the Halting Problem (or, more precisely, the Halting Problem can be reduced to them).

This does not mean that programme analysis is useless — it means that every analysis tool must make trade-offs. Sound tools (which never miss a real bug) must produce false positives. Complete tools (which never raise false alarms) must miss some real bugs. No tool can be both sound and complete for non-trivial program properties. (This is essentially Rice's Theorem, which we cover in the next chapter.)

The connection to Gödel

Turing's result and Gödel's result are deeply connected. In fact, they are two sides of the same coin:

Gödel showed that there are true arithmetic statements that no fixed proof system can derive.
Turing showed that there is no algorithm to decide whether arithmetic statements are provable.

Turing explicitly noted this connection: if the Halting Problem were decidable, then we could mechanically enumerate all theorems of arithmetic, which would resolve Gödel's undecidable sentences — a contradiction.

Undecidable problems everywhere

The Halting Problem opened the floodgates. Here are a few notable undecidable problems:

Post's Correspondence Problem: Given two lists of strings, is there a sequence of indices such that concatenating the corresponding strings from each list produces the same result? Undecidable.
The Word Problem for groups: Given a finitely presented group, is a given word equal to the identity? Undecidable in general (Novikov, 1955; Boone, 1959).
Hilbert's Tenth Problem: Given a Diophantine equation (a polynomial equation with integer coefficients), does it have an integer solution? Undecidable (Matiyasevich, 1970, building on work by Davis, Putnam, and Robinson).
The Entscheidungsproblem: The original decision problem that Hilbert posed — is there an algorithm to determine the truth of any statement in first-order logic? Church and Turing independently proved this undecidable in 1936.

Practical implications

"But my linter / static analyser / type checker works fine!" Yes — because practical tools do not attempt to solve the general Halting Problem. They work by:

Restricting the input language. Total functional languages like Agda and Idris guarantee termination by limiting what programmes can express (e.g., requiring structural recursion). The trade-off is that some terminating algorithms cannot be expressed directly.
Accepting incompleteness. Most static analysers use heuristics or abstract interpretation that over-approximate or under-approximate program behaviour. They catch many bugs but not all, or flag some false positives.
Requiring human annotations. Type signatures, loop invariants, preconditions, and postconditions give the analyser extra information that narrows the problem from "analyse arbitrary code" to "verify this specific claim."
Bounding the analysis. Model checkers explore a finite state space. Fuzzers run programmes for finite time. Both are effective but cannot guarantee exhaustive coverage of all possible executions.

The Halting Problem does not make these tools useless. It makes them engineering rather than mathematics: trade-offs, approximations, and pragmatic choices, rather than total, guaranteed solutions.

The deeper lesson

The Halting Problem tells us that computation is fundamentally unpredictable from within. No algorithm can fully understand the behaviour of all algorithms. This is not a bug in our current technology — it is a feature of the mathematical universe.

For engineers, this means: be suspicious of any tool that claims to fully verify arbitrary code. Be comfortable with approximation. Design systems that are robust to partial knowledge. And appreciate that the simplicity of "does this programme halt?" conceals an abyss of irreducible complexity.

Turing proved that there are questions that are perfectly well-defined, obviously important, and forever beyond the reach of mechanical computation. The wall is real, and it is permanent.

Impossibility Theorems