An incredibly simple proof of the halting problem (in Scheme)

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.

This proof by construction can be implemented in any language where functions are first-class objects, such as Python, JavaScript, and many other modern ones (not Java, of course. Java kind of sucks).

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!

This entry was posted on Tuesday, December 20th, 2011 at 5:35 am and is filed under Math/Comp Sci. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.