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(n-1) + fibo(n-2)

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):

halts('n = 4; while sumOfTwoPrimes(n): n = n + 2')

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 non-existence is requires more than just showing a hard problem could be solved if something exists. One way to prove non-existence 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:

def paradox():
    if halts('paradox()'): while True: pass

The body of the paradox procedure is an if expression. The consequent expression is a never-ending loop.

The predicate expression cannot sensibly evaluate to either True or False:

  • halts(paradox()) $\Rightarrow$ True: If the predicate expression evaluates to True, the consequent block is evaluated producing a never-ending loop. Thus, if halts('paradox()') evaluates to True, the evaluation of an application of paradox never halts. But, this means the result of halts('paradox()') was incorrect.
  • halts(paradox()) $\Rightarrow$ False: If the predicate expression evaluates to False, the alternate block is evaluated. It is empty, so evaluation terminates. Thus, the evaluation of paradox() terminates, contradicting the result of halts('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 enough---they are built-in 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.

  1. The terms decidable and undecidable 

  2. 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.