IV. Turing's Proof of the Unsolvability of the Halting Problem

Synopsis

Discussion

In my work in Chapter V, I'll follow Turing's approach and ignore the internal structure of the formal axiomatic system.

So let's use LISP to put some meat on the discussion in Chapter I of Turing's proof of the unsolvability of the halting problem. The halting problem asks for a way to determine in advance whether a program will halt or not. In the context of LISP, this becomes the question of whether a LISP expression has no value because it goes into an infinite loop, i.e., because evaluation never completes. Of course, a LISP expression can also fail to have a value because something else went wrong, like applying a primitive function to the wrong kind of argument. But we're not going to worry about that; we're going to lump together all the different ways a LISP expression can fail to have a value. [In fact, in my LISP the only way an expression can fail to have a value is if it never halts. That's because I have a very permissive LISP that always goes ahead and does something, even if it didn't get the kind of arguments that are expected for a particular primitive function. More precisely, all this is true if you turn off the part of my LISP that can give an ``out of data'' error message. That's part of my LISP that isn't used at all in this book. It's only needed for my course on The Limits of Mathematics.]

The kind of failure that we have in mind is exemplified by the following program which runs forever while displaying all the natural numbers.

  [display N & bump N & loop again]
   let (loop N) (loop + 1 display N) [calls itself]
  (loop 0) [start looping with N = 0]

Here is an interesting exercise for the reader. Write a LISP expression that has a value iff Fermat's last theorem is false. It halts iff there are natural numbers x > 0, y > 0, z > 0, n > 2 such that

I.e., it halts iff it finds a counter-example to Fermat's last theorem, which states that this equation has no solutions. In fact, the natural value to return if you halt is the quadruple (x y z n) refuting Fermat. It took three-hundred years for Andrew Wiles to prove Fermat's last theorem and settle negatively this one instance of the halting problem. [For an elementary account, see S. Singh, Fermat's Enigma—The Epic Quest to Solve the World's Greatest Mathematical Problem.] So some special cases of the halting problem are extremely interesting!

A more sophisticated example of an interesting instance of the halting problem is the conjecture called the Riemann hypothesis, probably the most famous open question in pure mathematics today. This is a conjecture that the distribution of the prime numbers is smooth couched as a statement that a certain function ζ(s) of a complex variable never assumes the value zero within a certain region of the complex plane. As was the case with Fermat's last theorem, if the Riemann hypothesis is false one can refute it by finding a counter-example. [For more information on expressing the Riemann hypothesis as an instance of the halting problem, see Section 2 ``Famous Problems'' in the article by M. Davis, Y. Matijasevic and J. Robinson on Hilbert's 10th problem in the publication Mathematical Developments Arising from Hilbert Problems, Proceedings of Symposia in Pure Mathematics, Volume XXVIII, American Mathematical Society, 1976, pp. 323-378.]

So here is how we'll show that the halting problem cannot be solved. We'll derive a contradiction by assuming that it can be solved, i.e., that there's a LISP subroutine (halts? s-exp) that returns true or false depending on whether the S-expression s-exp has a value.

Then using this hypothetical solution to the halting problem, we construct a self-referential S-expression the same way that we did in Chapter III. We'll define ``turing'' to be the lambda expression for a function of x that makes x into (('x)('x)) and then halts iff (('x)('x)) doesn't. I.e., the function ``turing'' of x halts iff the function x applied to x doesn't halt. But then applying this function to itself yields a contradiction! Because applying it to itself halts iff applying it to itself doesn't halt!

Here it is in more detail:

define (turing x) 
[Insert supposed halting algorithm here.]
let (halts? S-exp) ..... [<=============]
[Form ('x)]
let y [be] cons "' cons x nil [in]
[Form (('x)('x))]
let z [be] display cons y cons y nil [in]
[If (('x)('x)) has a value, then loop forever, otherwise halt]
if (halts? z) [then] eval z [loop forever]
              [else] nil [halt]

  (turing turing)

The proof of the pudding is that this expression displays itself, which shows that the self-reference works. It halts if we put in a ``halts?'' function that always returns ''false''. And it loops forever if we put in a ``halts?'' function that always returns ''true''. The error message ``Storage overflow!'' is due to the fact that looping forever overflows the push-down stack used by the LISP interpreter to keep track of the work that remains for it to do. [Even though running (turing turing) shows that it loops forever, it's not completely obvious why this works. (This is what happens when the halting problem subroutine predicts that (turing turing) will halt.) ``eval z'' seems like a funny way to make our expression loop forever. Well, this only works at the fixed point, because it reduces evaluating (turing turing) to evaluating it all over again, and therefore loops endlessly. In other words, my paradoxical function ``turing'' of x is only supposed to work when applied to itself. An alternative version that always loops forever would be to replace ``eval z'' by ``let (L) [be] (L) [in] (L)'' which is the simplest endless loop in my LISP. Furthermore, here is a deeper argument that ``eval z'' has to loop. ``eval z'', z = (turing turing) has to loop forever because if it returned a value, then we could change it and return that as our value, and then (turing turing) is not = to (turing turing), which is a contradiction!]

From the unsolvability of the halting problem it is easy to see that no truthful formal axiomatic system settles all instances of the halting problem. Because if we could prove all true assertions of the form (does-halt x) or (does-not-halt x) then we could solve the halting problem by running through all possible proofs in size order and applying the proof-checking algorithm to each in turn. [Simple as this algorithm is, we cannot do it with the toy LISP that I've presented here. Why not? Because running through all possible proofs in size order means generating all possible S-expressions and applying the proof-checking algorithm to each in turn. But the toy LISP in this book is not quite up to the task; I haven't provided the necessary machinery. What machinery is needed? Well, it's basically a way to convert bit strings (lists of 0's and 1's) into S-expressions. (This is equivalent to having a way to handle character strings and convert them into S-expressions.) But my LISP actually does provide a way to do this, except that I haven't talked about it here. You can do it using the ``read-exp'' primitive function together with the ``try'' mechanism that is at the heart of my book The Limits of Mathematics. Also, in the next chapter, Chapter V, I'll show how to side-step the issue. I'll cheat a little bit and I'll have the proof-checking function accept as its operand not the S-expression for a proof, but the number for an S-expression. I.e., I'll suppose that all proofs are numbered and work with the numbers instead. That makes it easy to run through all possible proofs. It enables me to give the flavor of my work in Chapter V while avoiding the technical complications.]

In Chapter V, I'll follow the spirit of Turing's approach, applied to the question of whether it's possible to prove that specific LISP S-expressions are elegant, i.e., have the property that no smaller expression has the same value. We'll pay absolutely no attention to the internal details of the formal axiomatic system that we'll be studying, we'll only care about the complexity of its proof-checking algorithm.

Turing's Proof in LISP

LISP Interpreter Run

[[[[[

 Proof that the halting problem is unsolvable by using
 it to construct a LISP expression that halts iff it doesn't.

]]]]]

define (turing x) 
[Insert supposed halting algorithm here.]
let (halts? S-exp) false [<=============]
[Form ('x)]
let y [be] cons "' cons x nil [in]
[Form (('x)('x))]
let z [be] display cons y cons y nil [in]
[If (('x)('x)) has a value, then loop forever, otherwise halt]
if (halts? z) [then] eval z [loop forever]
              [else] nil [halt]

define      turing
value       (lambda (x) ((' (lambda (halts?) ((' (lambda (y) (
            (' (lambda (z) (if (halts? z) (eval z) nil))) (dis
            play (cons y (cons y nil)))))) (cons ' (cons x nil
            ))))) (' (lambda (S-exp) false))))


[
 (turing turing) decides whether it itself has a value, 
 then does the opposite!

 Here we suppose it doesn't have a value, 
 so it turns out that it does:
]

(turing turing)

expression  (turing turing)
display     ((' (lambda (x) ((' (lambda (halts?) ((' (lambda (
            y) ((' (lambda (z) (if (halts? z) (eval z) nil))) 
            (display (cons y (cons y nil)))))) (cons ' (cons x
             nil))))) (' (lambda (S-exp) false))))) (' (lambda
             (x) ((' (lambda (halts?) ((' (lambda (y) ((' (lam
            bda (z) (if (halts? z) (eval z) nil))) (display (c
            ons y (cons y nil)))))) (cons ' (cons x nil))))) (
            ' (lambda (S-exp) false))))))
value       ()


define (turing x) 
[Insert supposed halting algorithm here.]
let (halts? S-exp) true [<==============]
[Form ('x)]
let y [be] cons "' cons x nil [in]
[Form (('x)('x))]
let z [be] [[[[display]]]] cons y cons y nil [in]
[If (('x)('x)) has a value, then loop forever, otherwise halt]
if (halts? z) [then] eval z [loop forever]
              [else] nil [halt]

define      turing
value       (lambda (x) ((' (lambda (halts?) ((' (lambda (y) (
            (' (lambda (z) (if (halts? z) (eval z) nil))) (con
            s y (cons y nil))))) (cons ' (cons x nil))))) (' (
            lambda (S-exp) true))))


[
 And here we suppose it does have a value, 
 so it turns out that it doesn't.

 It loops forever evaluating itself again and again!
]

(turing turing) 

expression  (turing turing)
Storage overflow!