Turing's proof

Alan Turing’s 1936 argument shows that no algorithm can decide whether every possible Turing machine halts on every possible input. It uses a self-referential machine to derive a contradiction.

Connect

Halting problem: The decision problem of determining whether a program eventually stops on a given input. Turing’s construction proves that no algorithm solves this problem for all machines and inputs.
Turing machine: An abstract model of computation with a tape, a read-write head, and a finite set of rules. Turing formalizes algorithms as machines whose halting behavior can be analyzed.
Alan Turing: A British mathematician and logician whose work founded theoretical computer science. Turing introduced the machine model and proved the undecidability result in 1936.
Undecidable problem: A decision problem for which no algorithm returns the correct yes-or-no answer on every input. Turing’s proof establishes the halting problem as a canonical undecidable problem.
Diagonal argument: A proof technique that constructs an object differing from every item in a proposed enumeration at a selected position. Turing adapts diagonalization to make a machine behave contrary to a supposed universal halting decider.
Algorithm: A finite, unambiguous procedure for carrying out a computation. The proof rules out any algorithm that decides halting in every case.
On Computable Numbers, with an Application to the Entscheidungsproblem: Turing’s 1936 paper defining automatic machines and proving limits on mechanical computation. This paper contains the original argument and its application to Hilbert’s decision problem.
Rice's theorem: A theorem stating that every nontrivial semantic property of partial computable functions is undecidable. It extends the lesson that general facts about program behavior resist algorithmic decision.
Self-reference: A structure in which an expression, description, or system refers to itself. The contradiction arises when the constructed machine is run on its own description.
Gödel numbering: A systematic assignment of numbers to formal symbols, expressions, or proofs. Machine descriptions can be encoded as data so one machine can examine another’s description.