2 Sketch of proof

The proof proceeds by reductio ad absurdumReductio ad absurdum ( Latin for "reduction to the absurd", traceable back to the Greek ἡ εις το αδυνατον απαγωγη, "reduction to t. We will assume that there is an algorithm described by the function 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 a function halt(a, i) that returns true if the algorithm represented by the string a halts when given as input the string i, and returns false otherwise. Given this algorithm we can construct another algorithm trouble(s) as follows:

The following is wikicode , a proposed pseudocode for use in many articles:

function trouble(string s) if halt(s, s) = false return true else loop forever

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 initial data to feed to that algorithm. If halt returns false, then trouble returns true, otherwise trouble goes into an infinite loop. Since all algorithms can be represented by strings, there is a string t that represents the algorithm trouble. We can now ask the following question:

Does trouble(t) halt?

Let us consider both possible cases:

1. Assume that trouble(t) halts. The only way this can happen is that halt(t,t) returns false, but that in turn indicates that trouble(t) does not halt. Contradiction.
2. Assume that trouble(t) does not halt. Since halt always halts, this can only happen when trouble goes into its infinite loop. This means that halt(t,t) must have returned true, since trouble would have returned immediately if it returned false. But that in turn would mean that trouble(t) does halt. Contradiction.

Since both cases lead to a contradiction, the initial assumption that the algorithm halt exists must be false.

3 Formalization of the Halting Problem

In his original proof Turing formalized the concept of algorithm by introducing Turing machineThe Turing machine is an abstract model of computer execution and storage introduced in 1936 by Alan Turing to give a mathematically precise definition of algorithm or 'mechanical procedure'. As such it is still widely used in theoretical computer sciences. However, the result is in no way specific to them; it applies equally to any other model of computationComputation Discrete mathematics Computation can be defined as finding a solution to a problem from given inputs by means of an algorithm. This is what the theory of computation a subfield of computer science and mathematics, deals with. For thousands of that is equivalent in its computational power to Turing machines, such as Markov algorithmA Markov algorithm is a string rewriting system that uses grammar-like rules to operate on strings of symbols. Markov algorithms have been shown to have sufficient power to be a general model of computation, and can thus be shown to be equivalent in powers, Lambda calculusThe lambda calculus is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used the lambda calculus in 1936 to give a negative an, Post systems or register machineA register machine is a hypothetical model of computation that is equivalent in its computational power to Turing machines. Definition A register machine can be seen as a finite set of registers r . r each of which can hold a non-negative integer, and a fs.

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 numeral system.

4 Relationship with Gödel's Incompleteness Theorem

The concepts raised by 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 unachievable. 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 Gödel'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) yields 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.

5 Can humans solve the Halting Problem?

It might seem like humans could solve the halting problem. After all, a programmer can often look at a program and tell whether it will halt. It is useful to understand why this cannot be true. For simplicity, we will consider the halting problem for programs with no input, which is also undecidable.

To "solve" the halting problem means to be able to look at any program and tell whether it halts. It is not enough to be able to look at some programs and decide. A Turing machine can do that. In fact, even a finite state machine can do that. There exists a finite state machine that, given any program less than a gigabyte long, immediately returns whether the program will halt (we do not know that finite state machine however—see below for why). But if a program is long enough, the usual bound on lifespan would prevent a human from even reading the entire program. After just a few decades of reading spaghetti code, the human would already start to forget some of the details. Humans can't solve the halting problem, due to the sheer size of the input.

Even for short programs, it isn't clear that humans can always tell whether they halt. For example, we might ask if this pseudocode function, which corresponds to a particular Turing machine, ever halts:

function searchForOddPerfectNumber() var int n:=1 // arbitrary-precision integer loop { var int sumOfFactors := 0 for factor from 1 to n-1 if factor is a factor of n sumOfFactors := sumOfFactors + factor if sumOfFactors = n then exit loop n := n + 2 } return

This program searches until it finds an odd perfect number, then halts. It halts if and only if such a number exists, which is a major open question in mathematics. So, after centuries of work, mathematicians have yet to discover whether a simple, ten-line program halts. This makes it difficult to see how humans could solve the halting problem.

More generally, it's usually easy to see how to write a simple brute-force search program that looks for counterexamples to any particular conjecture in number theory; if the program finds a counterexample, it stops and prints out the counterexample, and otherwise it keeps searching forever. For example, consider the famous (and still unsolved) twin prime conjecture. This asks whether there are abritrarily large prime numbers p and q with p+2 = q. Now consider the following program, which accepts an input N:

function findTwinPrimeAbove(int N) int p := N loop if p is prime and p + 2 is prime return else p := p + 1

This program searches for twin primes p and p+2 both at least as large as N. If there are arbitrarily large twin primes, it will halt for all possible inputs. But if there is a pair of twin primes P and P+2 larger than all other twin primes, then the program will never halt if it is given an input N larger than P. Thus if we could answer the question of whether this program halts on all inputs, we would have the long-sought answer to the twin prime conjecture. It's similarly straightforward to write programs which halt depending on the truth or falsehood for many other conjectures of number theory.

Because of this, one might say that the halting theorem itself is unsurprising. If there were a mechanical way to decide whether arbitrary programs would halt, then many apparently difficult mathematical problems would succumb to it. A counterargument to this, however, is that even if the halting problem were decidable, it might still be infeasible in practice, because it takes too much time or memory to execute. For example, there are some very large upper bounds on numbers with certain properties in number theory, but it's not feasible to check all values below this bound in a naive way with a computer — they can't even hold some of these numbers in memory.

6 Recognizing partial solutions

No program can solve the halting problem. There are programs that give correct answers for some instances of it, and run forever on all other instances. A program that returns answers for some instances of the halting problem might be called a partial halting solver (PHS). Can we recognize a correct PHS when we see it? Let the PHS recognition problem be this: given a PHS, determine whether it returns only correct answers. This problem sounds like it might be easier than the halting problem itself. It is not. It is just as undecidable as the halting problem. This follows trivially from Rice's theorem. It also follows from the undecidability of the halting problem, as will now be shown.

For every instance of the halting problem, there is an instance of the PHS recognition problem that is just as hard to solve. For example, the previous section showed an instance of the halting problem for which no one knows the answer. Here is how it can be converted into an instance of the PHS recognition problem for which no one knows the answer:

input a program P if P = (one of the example programs above) output "Yes, that program halts" else loop forever

Does that program return only correct answers? No one knows. This shows further just how difficult the halting problem is. There is no way to solve it in general. There isn't even a general way to know whether a program partially solves it.

Another example, H_T, of a Turing machine which gives correct answers only for some instances of the halting problem can be described by the requirements that, if H_T is started scanning a field which carries the first of a finite string of a consecutive "1"s, followed by one field with symbol "0" (i. e. a blank field), and followed in turn by a finite string of i consecutive "1"s, on an otherwise blank tape, then

• H_T halts for any such starting state, i. e. for any input of finite positive integers a and i;
• H_T halts on a completely blank tape if and only if the Turing machine represented by a does not halt when given the starting state and input represented by i; and
• H_T halts on a nonblank tape, scanning an appropriate field (which however does not necessarily carry the symbol "1") if and only if the Turing machine represented by a does halt when given the starting state and input represented by i. In this case, the final state in which H_T halted (contents of the tape, and field being scanned) shall be equal to some particular intermediate state which the Turing machine represented by a attains when given the starting state and input represented by i; or, if all those intermediate states (including the starting state represented by i) leave the tape blank, then the final state in which H_T halted shall be scanning a "1" on an otherwise blank tape.

While its existence has not been refuted (essentially: because there's no Turing machine which would halt only if started on a blank tape), such a Turing machine H_T would solve the halting problem only partially either (because it doesn't necessarily scan the symbol "1" in the final state, if the Turing machine represented by a does halt when given the starting state and input represented by i, as explicit statements of the halting problem for Turing machines may require).

7 See

• A control flow graph can be used to quickly categorize whether a program has no loops (and so halts), has trivial loops (and so halts), has non-trivial loops (undecided), or goes into an infinite loop.

8 References

• 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, formulates the halting problem, and shows that it (as well as the Entscheidungsproblem) is unsolvable.

• Wiki:HaltingProblem

Computability Logic

<Hide>