Halting problem

The Halting Problem poses a particular limited question about the predictability of the future operation of a computer program: whether it is possible to tell, from just examining a particular program, whether it will ever terminate (i.e. come to a step of its instructions which tell it to cease operation).

The surprising answer of "No" was given in 1936, in the form of the Church-Turing Thesis (due to Alonzo Church and Alan Turing). This theorem proved that no systematic method exists, or can ever exist, which can reliably predict this aspect of the behavior of all computer programs. Specific programs may be predictable, but there will always exist other programs whose long-term behavior is unpredictable.

This result was one of the earliest undecidability results. At the time, a revolution in mathematical thought was already underway due to Gödel's Incompleteness Theorem of 1931, which demonstrated that certain theorems in mathematics, although true, cannot be proven. In other words, limits had been discovered to the power of formal, axiomatic reasoning. The Halting Problem can be viewed as a variant of this result in the field of computation; limits were found to the power of analyzing computational processes.

To put it another way, sometimes there is no simpler way to model the operation of a program than the operation of the program itself, and the only way to discover exactly what it will do is to run it and observe. This is analagous to (and in fact mathematically related to) the behaviour of many cellular automata, such as the computer game Life, in which there is no shortcut to reliably predicting the future evolution of many patterns, other than to let them evolve, and observe.

Details

In more formal terms, the Halting Problem seeks to determine, for any given program P,

Will P terminate (halt) or continue indefinitely ?

The solution was sought in a general sense for all programs P, that is, can we write a 'halting detector' program H, which will read any program P and determine if P terminates.

Intuitively one might be tempted to suggest simply executing P, and seeing what happens. The problem with this is one can never be certain that one has waited long enough for P to terminate; it could be that after watching P for a certain period, and giving up, thinking it will not terminate, it might have terminated on its own shortly thereafter. In other words, one can only assert that P has been observed to terminate, or that it has been observed through N steps, and that it had not terminated yet; one cannot assert, based on observation, that it will never terminate.

The halting-detector H must be guaranteed to terminate in a finite period of time. (In other words, it's of no use to have a program H which can determine if P will halt, if H itself may never halt. Were that the case, one would have the exact same problem as previously with P, only now with H: one might give up on a particular run of H which is not terminating, thereby leaving one without an answer to the question of whether P will terminate.)

Were H to exist (which it doesn't), it would be a valuable tool indeed. To know that a program halts is equivalent to knowing that it was successful. For example, it would determine whether a counter-example to Goldbach's Conjecture (that every even number is the sum of two primes) exists. Simply write a program Pg which ascends the even numbers, testing whether each is the sum of two primes. If a halting-detector H existed, it could determine if Pg ever terminates (by calculating H(Pg)), and thereby dispose of Goldbach's Conjecture.

Many programs are naturally written to continue running until something is found, or a certain condition is attained. Other programs can always be trivially modified to behave this way. Any well defined question about the eventual behavior of a program can be restated in terms of halting. Thus, the Halting Problem is really question about a program's long-term behavior in general.

Sketch of Proof

This is by no means faithful to the historical development of the Church-Turing theorem. Rather, this sketch is intended to convince the modern reader familiar with computer programming that the theorem is true.

Suppose we have a programming language 'like' (isomorphic to) Lisp. While programming languages differ in terms of style, all 'sufficiently powerful' languages are identical in terms of which computations can be performed. (The weaker languages are not of interest for the purposes of this discussion.) So the choice of language is arbitrary.

       a) 'Quine' Lemma : A program can assign its own source code to a variable name. 

We omit the proof here; this is a common puzzle posed to computer science students. In other words, "Write a program which prints out its own source code." To thwart 'cheating' by, say, reading the disk for the source code we add a condition : memory cannot be accessed that was populated before the program was run. That is, no scanning the disk or RAM for the incidental presence of the source code, the program must assemble its code 'by hand'. This is often called 'Quining'. (The term is a reference to Willard Van Orman Quine, perhaps first used by Douglas Hofstadter in his pulitzer prize-winning book Godel, Escher, Bach : An Eternal Golden Braid.)

This lays the groundwork for a self-referential paradox under the assumption that the Halting Problem is solvable.

       Suppose a halting detector, H(P), exists. H reads any program P, and returns True only if P halts. 

We construct a program, Spite, which defies H by design. We provide the following pseudo-code :

       Define Spite :

           If H(Spite) is True, hang in an infinite loop. 
           If H(Spite) is False, terminate. 

Spite uses the Quine trick to make a liar of H.

Hence H cannot exist.