Halting problem

The Halting problem asks whether a program eventually stops when given a particular input. Formally, for a program encoded as a finite string P and an input x, the question is whether P(x) halts or continues forever. A hypothetical halting decider would accept the pair when execution stops and reject it when execution runs indefinitely. The requirement is universal: the same method must work for every program and input, rather than merely for a particular programming language or a restricted class of programs.

The problem is undecidable, not merely difficult or slow. Turing showed that no algorithm can always produce the correct yes-or-no answer for all such pairs.¹ A simulator can establish some positive cases by observing a program stop, but indefinite observation cannot by itself establish nontermination.

The impossibility proof turns a proposed halting decider against itself. Assume a machine H correctly predicts whether any program halts on any input. Construct another machine D that examines a program description, halts if H predicts nonhalting, and loops forever if H predicts halting. When D is given its own description, both possible predictions lead to contradiction: a prediction of halting makes it loop, while a prediction of looping makes it halt.

This diagonalization resembles the self-reference used in Cantor's theorem and connects computability with mathematical logic. Turing presented the argument through abstract machines, while the same reasoning applies to ordinary programming languages capable of representing general computation.¹ The result is closely related to the Entscheidungsproblem, the search for a general decision procedure for logic.

The Halting problem marks a boundary between recognizable and decidable questions. The set of program-input pairs that eventually halt is recognizable: a universal machine can simulate a pair and accept whenever the simulation stops. Its complement is not recognizable in the same unrestricted sense, because no procedure can reliably certify every infinite computation. This asymmetry is a central distinction in computability theory.²

Many other impossibility results are proved by reducing the Halting problem to them. If a proposed algorithm could decide a sufficiently general property of program behavior, it could be used to decide halting as well. Rice's theorem formalizes a broad version of this idea: every nontrivial semantic property of programs is undecidable for suitable computational models.² Practical analyzers therefore rely on restricted languages, sound approximations, time limits, or answers such as “unknown.”

The theorem does not say that no individual program can be shown to halt or run forever; it says that no one algorithm settles every case. Direct proofs, mathematical invariants, bounded model checking, and exhaustive state analysis can resolve many particular instances. The obstacle appears when the method must handle arbitrary programs with unrestricted self-reference.

The result also depends on the computational model being general enough to simulate other computations. For finite-state programs, termination can be decidable by exploring the finite state graph, whereas adding unbounded memory restores the general impossibility result. The theorem is therefore a statement about expressive computational systems, not a claim that every real software system is equally opaque. Its influence extends beyond software to automated theorem proving, formal verification, programming-language semantics, and questions about the limits of mechanical reasoning.³

Undecidable

Not solvable by any algorithm that gives a correct answer for every permitted input.

Decidable

Solvable by an algorithm that eventually returns the correct answer for every input.

Recognizable

A property for which an algorithm confirms positive instances, though it may run forever on negative ones.

Diagonalization

A proof technique that constructs an object differing from each supposed complete list or decision procedure in a decisive case.

Rice's theorem

A theorem stating that every nontrivial semantic property of programs is undecidable for general computational models.