Can a computer decide?
The question
Some programs stop and some loop forever. Could someone write one clever program that looks at any program, together with its input, and always correctly says whether it will stop?
Try the experiment before reading on. There’s no wrong way to explore.
Experiment
The diagonal machine
Here is a list of infinite 0–1 sequences (we can only show the start). The gold sequence d flips the diagonal.
| s1 | … | ||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| s2 | … | ||||||||||
| s3 | … | ||||||||||
| s4 | … | ||||||||||
| s5 | … | ||||||||||
| s6 | … | ||||||||||
| d | 1 | 0 | 1 | 0 | 0 | 1 | ? | ? | ? | ? | … |
Point at (or tab to) a row to see where d differs from it. Click any digit to change the list.
Add d to the list and a new d appears that is different again. No list — however long — can contain every sequence.
Hints, if you want them
What’s going on
What’s going on
In 1936 Alan Turing proved that no such checker can exist. The argument is short.
Suppose a program could take any program and input and always answer correctly " stops on " or " runs for ever on ". Build a new program : given a program , it asks whether stops when given its own text as input, and then does the opposite — if says "stops", loops for ever; if says "runs for ever", stops.
Now run on its own text. If stops, then said " runs for ever" — wrong. If runs for ever, then said " stops" — wrong again. Either way makes a mistake, so the perfect checker cannot exist. This is the halting problem, and it is undecidable.
This is the same diagonal trick Cantor used to show that some infinities are bigger than others, and Gödel used to show that no consistent formal system can prove every true statement about whole numbers. It does not say that we can never tell whether a particular program stops — often we can — only that no single program can do it for all programs. Henry Rice later showed that the same holds for every non-trivial question about what programs compute.
Analogy, not a formal construction: The experiment shows Cantor's diagonal argument for 0–1 sequences. The halting proof below uses the same diagonal idea, applied to programs; the experiment is an illustration of the idea, not the halting proof itself.
Where this leads
- Advanced undergraduate · Lesson availableComputabilityTuring machines and other models of computation, the Church–Turing thesis, decidable and recursively enumerable sets, the undecidability of the halting problem, reductions and Rice's theorem.
- First-year graduate · Lesson availableGödel's incompleteness theoremsArithmetisation of syntax, representability of computable functions, the diagonal lemma, Gödel's first and second incompleteness theorems and Tarski's undefinability of truth.
- Advanced undergraduate · Lesson availableComputational complexityTime and space complexity classes, P and NP, polynomial-time reductions, NP-completeness and the Cook–Levin theorem, and the status of the P versus NP problem.