3.1. The halting problem

Let's have a look at the mother of all undecidable problems: the halting problem.

Here's a motivation: As you will be painfully aware of, computer programs can sometimes "hang", i.e. enter an infinite loop. It'd be great if we had a tool that would scan the source code of a program and alert us to possible infinite loops.

In order to get a feeling for the problem, let us look at a few pieces of code. For example:

The program prints a greeting and terminates (ignoring any input). In computability theory, one says that a program halts if it will terminate after finitely many steps when run on a computer.

Contrast this with prog2:

  def prog2 (input : Data) := do
    while True do
      IO.print "...hello again..."

Executed on an idealized computer, it will go on forever, printing the string again and again.

The halting problem is: Given a pair ⟨prog, input⟩, decide whether the program prog, executed with input data will eventually halt.

In the two examples considered, we were easily able to see that the first one does halt while the second one does not. So one might guess that the process can be automatized, i.e. that it is possible to write a computer program that decides the halting problem. But these simple examples are deceptive!

To appreciate the difficulty of the problem, recall Goldbach's Conjecture which we briefly met before. It claims that any even integer larger than 2 is the sum of two primes. Now, one can easily write a function IsGoldbachCounterExample, which takes a natural number n as its input, and checks in finitely many steps whether n is a counter-example to the conjecture (e.g. by going through all pairs of primes small than n). Using this subroutine, consider the following program, which checks ever-larger numbers until it finds a counter-example:

Clearly, CheckGoldbach halts if and only if the conjecture is wrong. Thus to solve the halting problem, we will in particular have to settle this open problem, a task at which the smartest mathematicians have failed for almost 300 years. Hm. Maybe things aren't that simple after all!

Remark:

• In the above argument, we only used that, for every n, IsGoldbachCounterExample n is decidable in finitely many steps. Call such a function a decidable predicate. Hence, if we could solve the halting problem, we could also decide the first-order proposition ∃ n, P n for any decidable predicate P. That's upping the ante even more!

3.2. Computers can't decide their own halting problem

For the purpose of this section, a computational model is a function eval that takes a program prog and input input, and returns that result of running prog on input.

(We'll make these notions more precise soon. For now, we'll rely on your intuition of what "computers running programs" are capable of -- very much in JPG mode).

A computational model can decide its halting problem if there is a program decider such that evaluating decider on ⟨prog, input⟩ returns true if prog will halt when run on input, and false else.

The definition presumes that decider itself halts on every input (otherwise it wouldn't make sense to talk about its return value). Such programs are called total.

We will now sketch an argument showing that, under mild assumptions, no computational model can solve its own halting problem. In fact, the problem fails already "on the diagonal", where input = prog (and where input thus becomes redundant as an argument to decider). Explicitly: There isn't even a total program decider such that eval decider prog returns true if and only if prog will halt on input prog.

The proof is sometimes said to be "by contradiction", but it is constructive in the same way as the proof of √2 ∉ ℚ is. Here's our strategy: Given any total program candidate, we construct a program spoiler such that

• if eval candidate spoiler is true, then spoiler will not halt when run with input spoiler

• if eval candidate spoiler is false, then spoiler will halt when run with input spoiler.

That's just saying that, whatever it is that candidate does, it's not solving the halting problem, because it fails to give the correct answer at least on input spoiler.

The construction amounts to the computer science version of a petulant toddler: spoiler first checks what it is supposed to do (according to candidate), and then does the opposite:

The "mild assumptions" alluded to before are now clearer: The argument works whenever the model of computation is powerful enough that, for every program candidate, one can express the program spoiler and have the "if-run_forever-else-halt" control flow work correctly.

3.3. A model of computation

To make the above discussion rigorous, we need a mathematical model of computation. Let's brainstorm.

Real computers are powered by central processing units that contain billions of transistors. If reasoning about the capabilities of computers would require a faithful model of a present-day CPU, we'd be in big trouble.

Real programmers don't target these transistors directly. Instead, they write code in programming languages. The reference manual of the popular python language amounts to fewer than 200 pages. That's orders of magnitude better than the schematics of a CPU -- but still way too voluminous for a mathematical model anybody would want to work with.

To make progress, let's turn things around and introduce an extremely spartan computational model. How it relates to the real world will be discussed below.

  while (mem[memPos]) [ ... ]

  ,         // read first input character into memory
  .         // output it
  [         // while first memory cell isn't 0
    ,.      //    read and print the next character
  ]         //
            // halt

3.4. Universality🔗

See Frank's notes.