Limits to computation

A Racket program is a sequence of S-expressions. We can write an interpreter in Racket that operates on a list of S-expressions, which would be a miniature version of DrRacket itself. We might want to build features into our interpreter to detect problematic situations. Consider the following Racket program:

When this program is run, it does not produce a value, but runs forever. Can we detect behaviour like this? Can we have our interpreter stop and say "Program runs forever without producing a value"?

As it turns out, we can’t, and we can prove that we can’t. What we are hoping for is a function such as this:

The function halting? we are hoping for consumes a list of S-expressions sxl (representing a program) and a value arg, and produces true if and only if the last function in sxl (assumed to be a function of one argument) halts (that is, does not run forever, but produces a value) on argument arg.

If we had such a function, we could test programs in our interpreter and signal when they fail to halt. But, as we will see, there is no way to complete the definition of halting?. Suppose there were. Then consider the following interesting function.

Let p be the list of S-expressions with the definitions of halting?, eternity, and perverse.

We now consider the following question: Does (perverse p) halt or not?

It has to do one or the other. But we will see that in either case, we reach a contradiction. Thus our assumption that halting? could be written is incorrect.

Suppose (perverse p) halts. Examining the code for perverse, we see that (halting? p p) must evaluate to false, otherwise the answer (eternity 1) would be evaluated. But if (halting? p p) is false, then the last function in p, when given the argument p, must not halt. The last function in p is perverse. Thus (perverse p) does not halt, a contradiction.

Now suppose (perverse p) does not halt. Examining the code for perverse, we see that (halting? p p) must evaluate to true, otherwise the else case is reached. But if (halting? p p) is true, then the last function in p, when given the argument p, must halt. The last function in p is perverse. Thus (perverse p) does halt, a contradiction.

This proof is due to Alan Turing, from 1936. A few months after Alonzo Church defined the lambda calculus and showed that there was no function that could tell if two lambda calculus expressions were equivalent (a lengthy proof that drew heavily on Gödel’s incompleteness proof), Turing defined what is now known as a Turing machine (another theoretical model of computation) and showed that there was no Turing machine program that could tell if a Turing machine program could halt. That proof, adapted to Racket (which is just the lambda calculus with syntactic sugar for notational convenience) is what we’ve just seen.

Both Church and Turing were trying to demonstrate the impossibility of the formalist goal of an algorithm that could decide whether any statement in first-order predicate logic had a proof or not. Although their motivation was firmly centred in logic, the work of these two men had a major influence on the development of computer science.