Simple halting problem proof found in SICP1:
Exercise 4.15. Given a one-argument procedure
pand an object
pis said to ``halt’’ on
aif evaluating the expression
(p a)returns a value (as opposed to terminating with an error message or running forever). Show that it is impossible to write a procedure
halts?that correctly determines whether
afor any procedure
a. Use the following reasoning: If you had such a procedure
halts?, you could implement the following program:
(define (run-forever) (run-forever)) (define (try p) (if (halts? p p) (run-forever) 'halted))
Now consider evaluating the expression (try try) and show that any possible outcome (either halting or running forever) violates the intended behavior of halts?
try halts when passed itself as input. Hence, halts? would return
try would loop forever — a contradiction.
try loops forever. Hence,
halt?(try, try) returns false,
halts on input
try — a contradiction.
A program is really just one big number, which means that all possible programs are countably infinite. So, for the sake of contradiction, suppose an oracle exists that solves the halting problem. First we list out all of the possible programs. Next, we can create a grid by listing all the possible inputs for each program on the adjacent axis.
A B C D E … All all possible inputs on X-axis. A B C D E … All possible programs on Y-axis.
Each program, when run on each input, will either halt or loop forever, thus our outputs will fill the table, e.g.
A B C D E A H L H L H B H H H H H C L H L H H D H L L L H E H H H L H H: Halts, L: Loops
Now, we create a new row by taking the elements at the diagonal (i.e the first element from the first row, the second element from the second row, etc.) and flipping Halt to Loop and Loop to Halt.
L L H H L
Where does this new row appear on the list? It cannot appear on the list because it is different from each row by at least one element.
This table is defined as the complete list of all possible programs and inputs, but we can never write a program that matches this new row for all inputs.
Cantor Diagonalization is actually very similar to the first proof. The
procedure does the opposite of what each program does, just as we constructed
the row from the diagonal, and the
halt? procedure is the oracle. We assumed
that the oracle exists, but have shown that it cannot exist. Hence, we have
proven by contradiction that the halting problem is undecidable.