← Lambdica / theory-of-computation

Halting Problem

Also known as: Entscheidungsproblem (special case)

Given an arbitrary Turing machine MM and an input ww, no algorithm decides whether MM halts on ww.

Formal definition

Let

HALT={M,wM is a Turing machine that halts on input w}.\text{HALT} = \{\,\langle M, w \rangle \mid M \text{ is a Turing machine that halts on input } w\,\}.

Theorem (Turing 1936). HALT\text{HALT} is undecidable. There exists no Turing machine HH such that, for every encoding M,w\langle M, w \rangle,

H(M,w)={1if M halts on w0otherwise.H(\langle M, w \rangle) = \begin{cases} 1 & \text{if } M \text{ halts on } w \\ 0 & \text{otherwise.} \end{cases}

Proof (diagonalization). Suppose, for contradiction, that such a decider HH exists. Construct a new Turing machine DD that takes a single argument — an encoding of a machine — and behaves as follows:

D(M)={loop foreverif H(M,M)=1,haltotherwise.D(\langle M \rangle) = \begin{cases} \text{loop forever} & \text{if } H(\langle M, \langle M \rangle \rangle) = 1, \\ \text{halt} & \text{otherwise.} \end{cases}

Now consider D(D)D(\langle D \rangle). By the construction of DD:

Either branch contradicts the existence of HH. \blacksquare

Intuition

The halting problem fails for the same reason Russell’s paradox fails: any decider for halting can be turned against itself by feeding it a description of a machine that does the opposite of what the decider says. The construction is a self-referential trap. It is the same shape as Cantor’s diagonal argument for the uncountability of the reals, and the same shape as Gödel’s first incompleteness theorem — three incarnations of the same anti-fixed-point structure.

Notice what the theorem does not say. It does not say that some programs are hard to analyze. Particular programs can absolutely have decidable halting analysis: a program with no loops always halts, and a program with explicitly bounded loops always halts. The theorem says there is no single uniform algorithm that works on all programs. The obstruction is to a general decision procedure, not to case-by-case reasoning. Static analyzers, type systems, and termination provers all live inside the gap that this leaves: they decide halting on restricted classes of programs, at the cost of either rejecting programs that do halt or accepting programs that do not.

A second clarification: the decider HH is required to always halt and produce the correct answer. A program that runs MM on ww for nn steps and reports “halts” if it stops, “unknown” otherwise, is not a decider — it is a semi-decider, and HALT is semi-decidable (it lives in the class RE\text{RE}). The undecidability result is precisely that HALT is in RE\text{RE} but not in R\text{R}.

Examples

The halting problem is the canonical reduction target in computability theory. Many other natural problems are proved undecidable by reduction from HALT:

Notes

Turing’s 1936 paper On Computable Numbers, with an Application to the Entscheidungsproblem targets a much older question: David Hilbert and Wilhelm Ackermann’s 1928 Entscheidungsproblem, which asked whether there exists a procedure to decide, for any sentence of first-order logic, whether it is universally valid. Turing reduces this to the halting problem on a universal machine and shows the answer is no.

Church’s contemporaneous proof (Church 1936) used the λ\lambda-calculus and arrived at the same negative answer through different machinery. Stephen Kleene later showed the two formalisms compute the same class of functions, and the Church–Turing thesis emerged from this convergence: every “effectively computable” function is computable by a Turing machine, equivalently λ\lambda-definable, equivalently general recursive in the sense of Gödel and Herbrand. The halting problem then becomes the boundary between what mechanical computation can decide and what it cannot — the first concrete coordinate on the map of impossibility.

There is a temptation to treat HALT as a purely negative result. It is not. The same diagonal trick that refutes uniform halting decidability constructs a function not computable by any Turing machine, which is exactly what makes the universe of computable functions a strict subset of all functions NN\mathbb{N} \to \mathbb{N}. Turing’s 1936 paper does not just close a door; it opens a new room.

Connections

depends_on

References

  • turing-1936-computable
  • church-1936-unsolvable
  • sipser-2013-introduction