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)

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!


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: