Undecidability of the Halting Problem

The undecidability of the halting problem is one of the most interesting and important topics in computer science. Indeed, it is one of the most important philosophical and scientific discoveries made during the twentieth century.

The Scheme programming language, with its natural representation of programs as structured data, allows an especially simple yet rigorous treatment of this topic. We could use any other Turing-complete language instead, but the definitions and proofs would become more complex.

We begin with some introductory material concerning quines and Turing completeness.

Quines

Definition of Quines

A Scheme program Q is a quine if and only if

    (equal? Q
            (eval Q (scheme-report-environment 5)))

evaluates to #t.

0 is a quine.

((lambda (x) (x x))
 (lambda (x) (x x)))

is not a quine.

((lambda (x) (list x (list 'quote x)))
 '(lambda (x) (list x (list 'quote x))))

is a quine.

If you don't understand why we are using Scheme instead of some other language such as Java, then you should write a Java program that prints itself to System.out.

Quines are named after Willard Van Orman Quine, who used to teach philosophy at Harvard.

Turing Completeness

Let N be the set of natural numbers (starting with zero).

Theorem. Not all mathematical functions from N to N are computable by a Scheme program.

The proof of that theorem uses a technique called diagonalization, which we will also use when we prove the undecidability of the halting problem.

Proof. Suppose every mathematical function f: N → N were computed by some Scheme program P_f. We will use the P_f to define a function g: N → N that isn't computed by any of the P_f.

First we assign a unique natural number to each of the P_f. One way to do this is to represent each P_f by its UTF-8 encoding, and to interpret the bits of that UTF-8 encoding as the binary representation of a natural number i_f.

Define g: N → N as follows. For each natural number i that is not equal to any of the i_f, define g(i) = 0. For each i_f, define g(i_f) = f(i_f) + 1.

g is not computed by any of the P_f because it returns a different result when given i_f as an argument. Therefore the P_f didn't compute all possible functions after all.

Nothing in the proof depends upon any special properties of Scheme. We could prove the theorem for any other programming language by substituting that language for Scheme.

Some mathematical functions are computable, but not all mathematical functions are computable. It turns out that all sufficiently powerful programming languages compute exactly the same set of functions from N to N. To make it easier to talk about the programming languages that are sufficiently powerful to compute this standard set of functions from N to N, we call them the Turing-complete languages.

Definition of Turing Completness

A programming language L is Turing-complete if and only if L is at least as powerful as Scheme in the following sense: For every mathematical function f: N → N that can be computed by a Scheme program, one could write a program in L that also computes f.

That definition could use any sufficiently powerful programming language instead of Scheme, but Scheme is convenient because it supports arbitrarily large exact integers. The original definition of Turing completeness used Turing machines, which are much less convenient.

Halting Problem for Scheme

Definition. A lambda expression H solves the halting problem for Scheme if and only if for all expressions F and printable values V

    (H 'F 'V)

returns #t if (F 'V) terminates and returns #f if (F 'V) does not terminate.

The restriction to printable values might make the halting problem easier, but it doesn't make the problem any harder. If the halting problem is undecidable when restricted to printable values, then it is also undecidable when all values are allowed.

Undecidability of the Halting Problem for Scheme

Theorem. No lambda expression H solves the halting problem for Scheme.

Proof. Suppose H is a lambda expression, and consider the following expression, which we'll call D:

    (letrec ((d (lambda (x) (if (H x x) (d x) #t))))
      d)

If (H 'D 'D) returns #t, then (D 'D) does not halt, which means H does not solve the halting problem.

If (H 'D 'D) returns #f, then (D 'D) returns #t, which means H does not solve the halting problem.

If (H 'D 'D) returns any value other than #t or #f, then H does not solve the halting problem.

If (H 'D 'D) does not return, then H does not solve the halting problem.

Since (H 'D 'D) must do one of the four things above, H does not solve the halting problem.

Since H is an arbitrary lambda expression, we conclude that no lambda expression solves the halting problem for Scheme.

It's a lot easier to prove the undecidability of the halting problem for Scheme than for most other languages, but the theorem above and its proof can be stated and proved for any Turing-complete programming language by encoding programs and values as numbers (or by using the quine tricks) to turn any program H into a program D that loops forever if H says it halts, and halts if H says it doesn't halt.

Last updated 23 March 2008.