Don’t know the programming language Scheme? Don’t have to! (Even if you *had* to it would take less than an hour to learn basic syntax).
When I began this blog I intended to make a blog post explaining a formal proof of Turing’s halting theorem (eg. no algorithm can exist which determines whether a computational procedure always halts for every input. For example, a program that took in a number and printed every number greater than that up to 100 would not halt for every number, for obvious reasons). Both Alan Turing, with Turing machines, and Alonzo Church, with the lambda calculus, independently proved the halting problem (“Entscheidungsproblem”). However, both of these proofs require a lot of background explanation, and they’re not the best way to do it anyways.
The best way, I found, was a simple exercise from the textbook, Structure and Interpretation of Computer Programs. Here is a construction of the proof:
Suppose we have “a procedure halts? that correctly determines whether p halts on a for any procedure p and object a.”
Then we write the following procedures:
(define (run-forever) (run-forever))
(This is an infinite loop), and then a specially constructed:
(define (try p) (if (halts? p p) (run-forever) 'halted))
Now, imagine that we called the expression (try try) and let it run. If (halts? try try) evaluates to true, signaling that the function try halts when called on itself, then try runs forever, a contradiction. Similarly, if halts? decides that try does NOT halt when called on itself, the function halts.
And there you have it – the contradiction! By reductio ad absurdum, a function such as halts? cannot exist.
And in addition, if you’re ever taking a computer science course which uses SICP as a textbook, Exercise 4.15 is answered for you!