← Lambdica / theory-of-computation
Halting Problem
Also known as: Entscheidungsproblem (special case)
Given an arbitrary Turing machine and an input , no algorithm decides whether halts on .
Formal definition
Let
Theorem (Turing 1936). is undecidable. There exists no Turing machine such that, for every encoding ,
Proof (diagonalization). Suppose, for contradiction, that such a decider exists. Construct a new Turing machine that takes a single argument — an encoding of a machine — and behaves as follows:
Now consider . By the construction of :
- If halts on , then must have returned , so should have looped — contradiction.
- If loops on , then must have returned , so should have halted — contradiction.
Either branch contradicts the existence of .
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 is required to always halt and produce the correct answer. A program that runs on for 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 ). The undecidability result is precisely that HALT is in but not in .
Examples
The halting problem is the canonical reduction target in computability theory. Many other natural problems are proved undecidable by reduction from HALT:
- Equivalence of Turing machines. Given , decide whether . Undecidable: a decider for equivalence would let us decide HALT.
- Validity of first-order logic. Decided independently by Church (1936) and Turing (1937); the original Entscheidungsproblem.
- Post’s correspondence problem. Given pairs of strings, decide whether some sequence of indices makes the concatenation of the equal the concatenation of the . Undecidable (Post 1946).
- Rice’s theorem. Every nontrivial semantic property of the language recognized by a Turing machine is undecidable. Halting is the prototype; Rice generalizes the trick.
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 -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 -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 . Turing’s 1936 paper does not just close a door; it opens a new room.
Connections
depends_on
References
turing-1936-computablechurch-1936-unsolvablesipser-2013-introduction