12.2 The Halting Problem
Godel established that no interesting and consistent axiomatic system is capable of proving all true statements in the system. Now we consider the analogous question for computing: are there problems for which no algorithm exists?
Recall these definitions form Chapters 1and 4:
 problem: A description of an input and a desired output.
 procedure: A specification of a series of actions.
 algorithm: A procedure that is guaranteed to always terminate.
A procedure solves a problem if that procedure produces a correct output for every possible input. If that procedure always terminates, it is an algorithm. So, the question can be stated as: are there problems for which no procedure exists that produces the correct output for every possible problem instance in a finite amount of time?
A problem is computable if there exists an algorithm that solves the problem. It is important to remember that in order for an algorithm to be a solution for a problem $P$, it must always terminate (otherwise it is not an algorithm) and must always produce the correct output for all possible inputs to $P$. If no such algorithm exists, the problem is noncomputable.^{1} are sometimes used to mean the same things as computable and noncomputable.}
Alan Turing proved that noncomputable problems exist. The way to show that uncomputable problems exist is to find one, similarly to the way Godel showed unprovable true statements exist by finding an unprovable true statement.
The problem Turing found is known as the Halting Problem:^{2}
[ \textit{Halting Problem} ]
Input: A string representing a Python program.
Output: If evaluating the input program would ever finish, output True
. Otherwise, output False
.
Suppose we had a procedure halts
that solves the Halting Problem. The input to halts
is a Python program expressed as a string.
For example, halts('(+ 2 3)')
should evaluate to True
, halts('while True: pass')
should evaluate to False
(the Python pass
statement does nothing, but is needed to make the while loop syntactically correct), and
def fibo(n):
if n == 1 or n == 2: return 1
else: return fibo(n1) + fibo(n2)
fibo(60)
'''''')
should evaluate to True
. From the last example, it is clear that halts
cannot be implemented by evaluating the expression and outputting True
if it terminates. The problem is knowing when to give up and output False
. As we analyzed in Chapter 7, evaluating fibo(60)
would take trillions of years; in theory, though, it eventually finishes so halts
should output True
.
This argument is not sufficient to prove that halts
is noncomputable. It just shows that one particular way of implementing halts
would not work. To show that halts
is noncomputable, we need to show that it is impossible to implement a halts
procedure that would produce the correct output for all inputs in a finite amount of time.
Here is another example that suggests (but does not prove) the impossibility of halts
(where sumOfTwoPrimes
is defined as an algorithm that take a number as input and outputs True
if the number is the sum of two prime numbers and False
otherwise):
This program halts if there exists an even number greater than 2 that is not the sum of two primes. We assume unbounded integers even though every actual computer has a limit on the largest number it can represent. Our computing model, though, uses an infinite tape, so there is no arbitrary limit on number sizes.
Knowing whether or not the program halts would settle an open problem known as Goldbach's Conjecture: every even integer greater than 2 can be written as the sum of two primes. Christian Goldbach proposed a form of the conjecture in a letter to Leonhard Euler in 1742. Euler refined it and believed it to be true, but couldn't prove it.
With a halts
algorithm, we could settle the conjecture using the expression above: if the result is False
, the conjecture is proven; if the result is True
, the conjecture is disproved. We could use a halts
algorithm like this to resolve many other open problems. This strongly suggests there is no halts
algorithm, but does not prove it cannot exist.
Proving Noncomputability. Proving nonexistence is requires more than just showing a hard problem could be solved if something exists. One way to prove nonexistence of an $X$, is to show that if an $X$ exists it leads to a contradiction. We prove that the existence of a halts
algorithm leads to a contradiction, so no halts
algorithm exists.
We obtain the contradiction by showing one input for which the halts
procedure could not possibly work correctly. Consider this procedure:
if halts('paradox()'): while True: pass
The body of the paradox
procedure is an if expression. The consequent expression is a neverending loop.
The predicate expression cannot sensibly evaluate to either True
or False
:
 halts(
paradox()
) $\Rightarrow$ True: If the predicate expression evaluates toTrue
, the consequent block is evaluated producing a neverending loop. Thus, ifhalts('paradox()')
evaluates toTrue
, the evaluation of an application ofparadox
never halts. But, this means the result ofhalts('paradox()')
was incorrect.  halts(
paradox()
) $\Rightarrow$ False: If the predicate expression evaluates toFalse
, the alternate block is evaluated. It is empty, so evaluation terminates. Thus, the evaluation ofparadox()
terminates, contradicting the result ofhalts('paradox()')
.
Either result for halts('paradox()')
leads to a contradiction! The only sensible thing halts
could do for this input is to not produce a value. That means there is no algorithm that solves the Halting Problem. Any procedure we define to implement halts
must sometimes either produce the wrong result or fail to produce a result at all (that is, run forever without producing a result). This means the Halting Problem is noncomputable.
There is one important hole in our proof: we argued that because paradox
does not make sense, something in the definition of paradox
must not exist and identified halts
as the component that does not exist. This assumes that everything else we used to define paradox
does exist.
This seems reasonable enoughthey are builtin to Python so they seem to exist. But, perhaps the reason paradox
leads to a contradiction is because True
does not really exist or because it is not possible to implement an if expression that strictly follows the Python evaluation rules. Although we have been using these and they seems to always work fine, we have no formal model in which to argue that evaluating True
always terminates or that an if expression means exactly what the evaluation rules say it does.
Our informal proof is also insufficient to prove the stronger claim that no algorithm exists to solve the halting problem. All we have shown is that no Python procedure exists that solves halts
. Perhaps there is a procedure in some more powerful programming language in which it is possible to implement a solution to the Halting Problem. In fact, we will see that no more powerful programming language exists.
A convincing proof requires a formal model of computing. This is why Alan Turing developed a model of computation.

The terms decidable and undecidable ↩

This problem is a variation on Turing's original problem, which assumed a procedure that takes one input. Of course, Turing did not define the problem using a Python program since Python had not yet been invented when Turing proved the Halting Problem was noncomputable in 1936. In fact, nothing resembling a programmable digital computer would emerge until several years later. ↩