Image 01 Image 02

The recursion theorem and you

Posted on 8th January 2012 by Sebastian

Quines are a wonderful thing. A quine is a program, that when run produces its own code as output. Now, in most interpreted languages you can read your own code through means of I/O — I’d consider that cheating: We can do much better than that. We’ll do it without anything but a clever theoretical result. (And maybe a little bit of code to make it work in practice.)

You can make a quine in any Turing-complete language, and the reason for this is a thorem called the recursion theorem. The theorem (informally[1]) states, that for any computable function f of two inputs, it is possible to create a program R that computes the function r defined by r(w) = f(w, \langle R \rangle), where \langle R \rangle is the description — or source code, if you will — of R. In essence this means, that it is possible to write a program which obtains its own source code, and then uses it for further computation.

Now, in order for this post to make sense, we’ll have to look a bit into the proof of the theorem. The idea behind the proof is as follows: We divide our program into three program fragments, A, B and F, each of which we can think of as a function in our programming language of choice. A is called first, and has the task of getting \langle BF \rangle, the source code of the functions B and F, and passing this on to B. B computes \langle A \rangle, and uses this to compute \langle ABF \rangle and pass it on to F. F is then the program fragment computing the function f, now with the source code of the entirety of the program in hand.

The interaction between A, B and F

Now that we have an idea of how the different fragments are to interact with each other, we need to get down to the specifics, and actually construct the fragments A and B[2].

We will start by constructing A. Let us for a moment assume that we actually have B and F already constructed. In that case, \langle BF \rangle is a fixed string. This means, we can have A simply call B(w, \langle BF \rangle) and be done with it.

For constructing B we will need to be a bit more tricksy. We know, based on how we constructed A, exactly what A looks like if we know what \langle BF \rangle is[3]. This means, given \langle BF \rangle, we can construct \langle A \rangle — and we’re in luck: Remember, when A calls B, it passes along the extra information of \langle BF \rangle. So, we now have both \langle A \rangle and \langle BF \rangle, and if we compose these two we get \langle ABF \rangle. We now call F(w, \langle ABF \rangle), and B does what we want it to.

This concludes the proof of the theorem, and it is now time to look a bit at how we can use it. A particularily interesting thing about this proof is, that we can use this construct directly to create a quine. To try this out, let us create a SML program, which prints its own source code in reverse.

We can start by creating F. All that F needs to do is simply to reverse and then print its input. This can be achieved pretty easily like so:

val F = print o implode o rev o explode

Next up is B, but before we can construct that, we need to figure out what we want A to look like. The simplest option is to have A take on the following form:

Now we can begin constructing B. If we just naïvely do this, we get something to the tune of:

This, however, suffers from the fact, that we’ll need to escape the quotes in the definition of B when writing them inside of the string in A. Were we to do this, we’d find that we’d need to escape the escape characters as well. A fixed version looks as follows:

Finally, we need to create A, but that is fairly simple, as we already have determined what format it should have. Since SML doesn’t support multiline strings, however, I collapse B and F onto one line, giving us a final result of:

And there we have it, we’ve created a lovely[4] reverse quine in SML using the recursion theorem. Not only that, we could repeat the process and do the exact same thing in most any other language — or change out F to whatever we wish. There is nothing special about the language or F we chose — and that I find quite spectacular.

  1. [1]The actual formal statement and proof of the theorem can be found in Introduction to the Theory of Computation by Michael Sipser. If you like the content of this article, I urge you to read it — it is quite a good book.
  2. [2]Why do we not need to construct F?
  3. [3]After all, we constructed A based on this ourselves.
  4. [4]Okay, not the prettiest, but lovely in concept.

Leave a reply...