A short proof

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;

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.