Kleene's recursion theorem

Kleene's recursion theorem is a result in computability theory first proved by Stephen Kleene; it allows to construct programs, Turing machines and recursive functions that refer back to their own description.

The theorem can be formulated for any of the equivalent models of computation listed in the computability theory article. Here we will use Pascal programs.

If p is a string that describes a Pascal program which reads a single input string and produces a single output string, then we will denote the corresponding partial function from input strings to output strings by f_p. (This is a partial function because for some input strings the program described by p may run into an infinite loop and never produce an output.)

The statement of the theorem is as follows: If Q is a Pascal program which takes two input strings x and y and produces a single output string Q(x,y) (which again may be undefined if Q runs into an infinite loop), then there always exists a string p describing some Pascal program such that for all input strings y:

Q(p,y) = f_p(y).

This latter equality is to be read as an equality of partial functions: Q(p,y) is defined if and only if f_p(y) is defined, and in this case the two values are the same.

As an application, we can show that there must exist a Pascal program which takes a single input, ignores that input and prints itself as output: Define Q(x,y) = x, then the theorem yields a Pascal program p such that for all y: f_p(y) = Q(p,y) = p. It is an amusing exercise to actually write such a program p.