The halting problem is a decision problem which can be informally stated as follows:
- Given a description of an algorithm and a description of its initial arguments, determine whether the algorithm, when executed with these arguments, ever halts (the alternative is that it runs forever without halting).
The importance of the halting problem lies in the celebrated theorem, first proved in 1936 by Alan Turing, which shows that the problem is in fact undecidable, i.e., there is no way to construct an algorithm which is always able to determine whether another algorithm halts or not. A consequence of this is that the Entscheidungsproblem is unsolvable, and in particular there cannot be an algorithm that decides whether a given statement about natural numbers is true or not. The reason for this is that the proposition that states that a certain algorithm will halt given a certain input can be automatically reformulated as a statement about numbers. Since there is no algorithm that can decide if the original statement about algorithms is true or not, there can also not be an algorithm for deciding this for the corresponding statement about numbers.
Another reason why the undecidability of the Halting problem is interesting is because it provides an alternative proof of Gödel's incompleteness theorem (more precisely, a weaker form of the First Incompleteness Theorem). This is because if there were a complete and consistent axiomatization of all true statements about natural numbers, then we would be able to construct an algorithm that decides wheter such a statement is true or not. (This will be discussed in more detail later on.) But we saw above that that is impossible.
Yet another, quite amazing, consequence of the undecidability of the Halting problem is Rice's theorem which states that the truth of any non-trivial statement about the function that is defined by an algorithm is undecidable. So, for example, the decision problem "will this algorithm halt for the empty string" is already undecidable. Note that this theorem holds for the function defined by the algorithm and not the algorithm itself. It is, for example, quite possible to decide if an algorithm will halt within 100 steps, but this is not a statement about the function that is defined by the algorithm.
Many problems can be shown to be undecidable by reducing them to the Halting problem, and this is the standard method of proof for such questions. However, Gregory Chaitin has given an undecidable problem in algorithmic information theory which does not depend on the Halting problem. Chaitin also gave the intruiging definition of the Halting probability which represents the probability that a randomly produced program halts.
While Turing's proof shows that there can be no general method or algorithm to determine whether algorithms halt, individual instances of that problem may very well be susceptible to attack. Given a specific algorithm, one can often show that it must halt, and in fact computer scientists often do just that as part of a correctness proof. But every such proof requires new arguments; there is no mechanical, general way to determine whether algorithms halt.
Another caveat: the undecidability of the halting problem relies on the fact that algorithms are assumed to have actually finite but potentially infinite storage: at any one time they can only store finitely many things, but they can always store more and they never run out of memory. If the memory of a machine is limited, as it is in actually existing computers, then the Halting problem for programs running on that machine can be solved with a general algorithm (albeit an extremely inefficient one).
Sketch of Proof
The proof proceeds by reductio ad absurdum; we will assume that there is an algorithm Halt(a, i) that decides if the algorithm encoded by the string a will halt when given as input the string i, and then show that this leads to a contradiction.
We start with assuming that there is an algorithm Halt(a, i) the returns the string "yes" if the algorithm represented by the string a halts when given as input the string i, and returns the string "no" otherwise. Given this algorithm we can construct another algorithm Trouble(s) as follows:
function Trouble ( s : string ) : string begin if Halt(s, s) = "no" then return("yes") else ... some infinite loop ... end
This algorithm takes a string s as its argument and runs the algorithm Halt, giving it s both as the description of the algorithm to check and as the the initial data to feed to that algorithm. If Halt outputs "no", then Trouble outputs "yes", otherwise Trouble goes into an infinite loop. Since all algorithms can be represented by strings there will be a string T that represents the algorithm Trouble. We can now ask the following question:
- What is the output of Halt(T, T)?
We know by the definition of Halt that the output must be either "yes" or "no". Let us consider both cases:
- Assume that the output is "no". Since Halt decides if the encoded algorithm halts for the given input, it follows that Trouble does not halt on input T. If we look at the algorithm of Trouble we can see that this is only the case if the result of Halt(T, T) is "yes", which contradicts the assumption that the output is "no".
- Assume that the output is "yes", then it follows by the definition of Halt that Trouble does not halt on input T. If we again look at the algorithm of Trouble we see that the result of Halt(T, T) then must be "no", which contradicts the assumption that it is "yes".
Since both cases lead to a contradiction there will always be a contradiction, and so the first assumption that the algorithm Halt exists must be false.
Formalization of the Halting Problem
In his original proof Turing formalized the concept of algorithm by introducing Turing machines. However, the actual choice of formalization turns out to be of little importance. One can choose any of the many known models of computability (such as Markov algorithms, Lambda calculus, Post systems or any other Turing complete programming language.
What is important is that the formalization allows a straightforward mapping of algorithms to some data type that the algorithm can operate upon. For example, if the formalism lets algorithms define functions over strings (such as Turing machines) then there should be a mapping of these algorithms to strings, and if the formalism lets algorithms define functions over natural numbers (such as recursive functions) then there should be a mapping of algorithms to natural numbers. The mapping to strings is usually the most straightforward, but strings over an alphabet with n characters can also be mapped to numbers by interpreting them as numbers in an n-ary number system.
The Halting problem as a statement about numbers
- yet to be written
Relationship with Gödel's Incompleteness Theorem
The concepts raised by the Gödel's incompleteness theorems are very similar to those raised by the halting problem, and the proofs are quite similar. In fact, a weaker form of the First Incompleteness Theorem is an easy consequence of the undecidability of the Halting Problem. This weaker form differs from the standard statement of the incompleteness theorem by asserting that a complete, consistent and sound axiomatization of all statements about natural numbers is unacheivable. The "sound" part is the weakening: it means that we require the axiomatic system in question to prove only true' statements about natural numbers (it's very important to observe that the statement of the standard form of Godel's First Incompleteness Theorem is completely unconcerned with the question of truth, but only concerns the issue of provability).
The weaker form of the theorem can be proved from the undecidability of the Halting Problem as follows. Assume that we have a consistent and complete axiomatization of all true first-order logic statements about natural numbers. Then we can build an algorithm that enumerates all these statements. This means that there is an algorithm N(n) that given a natural number n computes a true first-order logic statement about natural numbers such that for all the true statements there is at least one n such that N(n) is that statement. Now suppose we want to decide if the algorithm with representation a halts on input i. We know that this statement can be expressed with a first-order logic statement, say H(a, i). Since the axiomatization is complete it follows that either there is an n such that N(n) = H(a, i) or there is an n' such that N(n' ) = ¬ H(a, i). So if we iterate over all n until we either find H(a, i) or its negation, we will always halt. This means that this gives us an algorithm to decide the Halting problem. Since we know that there cannot be such an algorithm it follows that the assumption that there is a consistent and complete axiomatization of all true first-order logic statements about natural numbers, must be false.
- Alan Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, Series 2, 42 (1936), pp 230-265. online version This is the epochal paper where Turing defines Turing machines and formulates and solves the halting problem as well as the Entscheidungsproblem