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.

A Scheme program`is a`

Qquineif and only if(equal?evaluates toQ(evalQ(scheme-report-environment 5)))`#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.

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 functionf: N → N were computed by some Scheme programP. We will use the_{f}Pto define a function_{f}g: N → N that isn't computed by any of theP._{f}

First we assign a unique natural number to each of theP. One way to do this is to represent each_{f}Pby its UTF-8 encoding, and to interpret the bits of that UTF-8 encoding as the binary representation of a natural number_{f}i._{f}

Defineg: N → N as follows. For each natural numberithat is not equal to any of thei, define_{f}g(i) = 0. For eachi, define_{f}g(i) =_{f}f(i) + 1._{f}

gis not computed by any of thePbecause it returns a different result when given_{f}ias an argument. Therefore the_{f}Pdidn't compute all possible functions after all._{f}

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.

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 functionf: N → N that can be computed by a Scheme program, one could write a program in L that also computesf.

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.

Definition.A lambda expression

Hsolves the halting problemfor Scheme if and only if for all expressions`and printable values`

F

V(returnsH'F'V)`#t`

if`(`

terminates and returnsF'V)`#f`

if`(`

does not terminate.F'V)

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.

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

H

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

H`:`

D(letrec ((d (lambda (x) (if (IfHx x) (d x) #t)))) d)`(`

returnsH'D'D)`#t`

, then`(`

does not halt, which meansD'D)`does not solve the halting problem.`

H

If`(`

returnsH'D'D)`#f`

, then`(`

returnsD'D)`#t`

, which means`does not solve the halting problem.`

H

If`(`

returns any value other thanH'D'D)`#t`

or`#f`

, then`does not solve the halting problem.`

H

If`(`

does not return, thenH'D'D)`does not solve the halting problem.`

H

Since`(`

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

H

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

H

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

into a program
`H`

that loops forever if
`D`

says it halts, and halts if
`H`

says it doesn't halt.
`H`

Last updated 27 October 2015.