The Halting Problem
- Turing, Church, and the Entscheidungsproblemnot yet tested
- The diagonal argument that H cannot existnot yet tested
- Decidable versus recursively enumerable problemsnot yet tested
- Rice's theorem and the limits of verificationnot yet tested
In 1928, David Hilbert — the most influential mathematician of his generation — posed a question to the world: is there a mechanical procedure that, given any mathematical statement, can determine in finite time whether the statement is provable? Hilbert called it the Entscheidungsproblem (the decision problem), and he expected the answer to be yes. Eight years later, a twenty-three-year-old graduate student at Cambridge named Alan Turing, working in parallel with the American logician Alonzo Church, gave the answer: no. There is no such procedure. Turing's proof required him to first invent a precise definition of mechanical procedure — what we now call a Turing machine — and then exhibit a problem the machine could not solve. That problem is the Halting Problem.
The Halting Problem asks: given a description of a program P and an input I, decide whether P run on I halts (terminates) or runs forever. Turing's proof that no such decision procedure exists is a diagonal argument — the same mechanism Cantor used to prove the reals are uncountable, and a close cousin of Gödel's incompleteness construction. Suppose, for contradiction, that there exists a program H that takes (P, I) and correctly decides whether P halts on I. Construct a new program D that does the following: D(P) calls H(P, P); if H says "halts," D goes into an infinite loop; if H says "doesn't halt," D halts immediately. Now ask: what does D do when given itself as input? If D(D) halts, then by D's construction H(D, D) said it doesn't halt — contradiction. If D(D) doesn't halt, then H(D, D) said it does halt — contradiction. So H cannot exist. The technique generalizes: Rice's theorem (1953) shows that almost any non-trivial property of program behavior is undecidable — you cannot, in general, write a program that detects whether another program is correct, terminating, equivalent to a given specification, or free of bugs. The theoretical wall is hard. Recursively enumerable sets are those for which a program can list members; decidable sets are those for which a program can also list non-members. The Halting Problem is recursively enumerable but not decidable. The Church–Turing thesis says all reasonable definitions of "computable" agree, suggesting that computation has a single, canonical notion of power. The connection to Gödel's incompleteness is exact: both show that systems rich enough to talk about themselves contain blind spots about themselves, and the proofs are structurally identical diagonalizations.