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]There is nothing wrong with this LISP expression except for the fact that it runs forever.

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]Then giving the function ``turing'' its own definition gives us an expression

(turing turing)that halts iff it doesn't, which proves that the halting problem cannot be solved in LISP (or in any other programming language). [A technical point. The expression (turing turing) cheats a bit; it's not a self-contained LISP expression. But the alternate version of itself that it displays so that we can verify that the fixed-point machinery worked

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.

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!