I've taken this from a letter by Christopher Strachey to the *Computer Journal* for January 1965, volume 7, number 4. There's a copy
as AI photocopy S170. He used a programming language called CPL which is
now extinct, but the basic idea works in any programming language where
functions (procedures, subroutines) can take other functions as
arguments. I've written the proof using Pascal-like notation, but
without the types.

Assume we have written a function called `T`

(T for
``terminates''). `T`

takes another function as argument, and
returns 1 if that function will eventually stop, and 0 if it will go on
for ever. For example, suppose we have these two functions `f`

and
`g`

:

function f; begin f := 1; end; function g; begin next: goto next; end;Then

`T(f)`

is 1; `T(g)`

is 0.
Now we write another function `P`

:

function P; begin l: if T(P) = 1 then goto l; end;

Now, what's `T(P)`

? It has to be either 0 or 1, so start by
assuming it's 0. Look at the definition of `P`

. If `T(P)`

is
0, `P`

won't goto `l`

, but will just return. So `P`

terminates. But that's a contradiction, because `T(P) = 0`

means
that `T`

is saying that `P`

won't terminate.

So assume instead that `T(P)`

is 1. Look again at the definition of
`P`

. Now, `P`

will goto `l`

and will loop forever. So
`P`

does not terminate. But that's also a contradiction, because
`T(P) = 1`

means that `T`

is saying that `P`

will
terminate.

So either way, we hit a contradiction. Our initial assumption - that
we could write a function `T`

- must therefore be false.

Note: strictly speaking, this only works in a language where a function
can take *any* other function as an argument. If you know Pascal,
you'll know that's not the case there, because of type-checking (though
I think it is in C). In such cases, you need to make a more indirect
proof. This involves encoding the text of the procedure as a number, and
using that number as an index into a catalogue of all possible
functions. But the basic structure is still the same.

Wed Feb 14 23:47:23 GMT 1996