The recursion theorem and you

  • user warning: Got error 28 from storage engine query: SELECT DISTINCT t.* FROM drupal_term_node r INNER JOIN drupal_term_data t ON r.tid = t.tid INNER JOIN drupal_vocabulary v ON t.vid = v.vid LEFT JOIN drupal_forum_access fa ON t.tid = fa.tid LEFT JOIN drupal_acl acl_fa ON acl_fa.name = t.tid AND acl_fa.module = 'forum_access' LEFT JOIN drupal_acl_user aclu_fa ON aclu_fa.acl_id = acl_fa.acl_id AND aclu_fa.uid = 0 WHERE ((fa.grant_view >= 1 AND fa.rid IN (1)) OR fa.tid IS NULL OR aclu_fa.uid = 0) AND ( r.vid = 69914 )ORDER BY v.weight, t.weight, t.name in /var/www/dikutal.dk/modules/taxonomy/taxonomy.module on line 632.
  • user warning: Got error 28 from storage engine query: SELECT DISTINCT node.nid AS nid, node.title AS node_title, node.language AS node_language, node.type AS node_type, node.vid AS node_vid, node_revisions.teaser AS node_revisions_teaser, node_revisions.format AS node_revisions_format, node_data_field_date.field_date_value AS node_data_field_date_field_date_value FROM drupal_node node LEFT JOIN drupal_content_field_date node_data_field_date ON node.vid = node_data_field_date.vid LEFT JOIN drupal_term_node term_node ON node.vid = term_node.vid AND (term_node.tid = 9 OR term_node.tid = 10 OR term_node.tid = 12 OR term_node.tid = 19 OR term_node.tid = 18 OR term_node.tid = 13 OR term_node.tid = 16 OR term_node.tid = 17 OR term_node.tid = 11 OR term_node.tid = 14 OR term_node.tid = 15) LEFT JOIN drupal_node_revisions node_revisions ON node.vid = node_revisions.vid INNER JOIN drupal_node_access na ON na.nid = node.nid WHERE (na.grant_view >= 1 AND ((na.gid = 0 AND na.realm = 'all') OR (na.gid = 1 AND na.realm = 'book_page_access_view') OR (na.gid = 1 AND na.realm = 'forum_access'))) AND ( ((node.status <> 0) AND (node.type in ('event')) AND (term_node.tid IS NULL)) AND (DATE_FORMAT(ADDTIME(node_data_field_date.field_date_value, SEC_TO_TIME(7200)), '%Y-%m-%d') >= '2014-10-22') )ORDER BY node_data_field_date_field_date_value ASC LIMIT 0, 3 in /var/www/dikutal.dk/sites/all/modules/views/includes/view.inc on line 771.
Skrevet af Sebbe, 8. januar 2012 - 6:10

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:

fun A () = B "fun B x = ... and F x = ..."

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

fun B x = F ("fun A x = B \"" ^ x ^ "\"\n" ^ x)

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:

fun B x = let fun esc (#"\""::xs) = #"\\" :: #"\"" :: esc xs
| esc (#"\\"::xs) = #"\\" :: #"\\" :: esc xs
| esc (x::xs) = x :: esc xs
| esc [] = []
in F ("fun A x = B \"" ^ (implode o esc o explode) x ^ "\"\n" ^ x) end

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:

(* With B and F neatly formatted *)
fun A () = B "and B x = let fun esc (#\"\\\"\"::xs) = #\"\\\\\" :: #\"\\\"\" :: esc xs | esc (#\"\\\\\"::xs) = #\"\\\\\" :: #\"\\\\\" :: esc xs | esc (x::xs) = x :: esc xs | esc [] = [] in F (\"fun A () = B \\\"\" ^ (implode o esc o explode) x ^ \"\\\"\\n\" ^ x) end and F x = (print o implode o rev o explode) x"

and B x = let fun esc (#"\""::xs) = #"\\" :: #"\"" :: esc xs
| esc (#"\\"::xs) = #"\\" :: #"\\" :: esc xs
| esc (x::xs) = x :: esc xs
| esc [] = []
in F ("fun A () = B \"" ^ (implode o esc o explode) x ^ "\"\n" ^ x) end

and F x = (print o implode o rev o explode) x

(* And with B and F collapsed *)
fun A () = B "and B x = let fun esc (#\"\\\"\"::xs) = #\"\\\\\" :: #\"\\\"\" :: esc xs | esc (#\"\\\\\"::xs) = #\"\\\\\" :: #\"\\\\\" :: esc xs | esc (x::xs) = x :: esc xs | esc [] = [] in F (\"fun A () = B \\\"\" ^ (implode o esc o explode) x ^ \"\\\"\\n\" ^ x) end and F x = (print o implode o rev o explode) x"
and B x = let fun esc (#"\""::xs) = #"\\" :: #"\"" :: esc xs | esc (#"\\"::xs) = #"\\" :: #"\\" :: esc xs | esc (x::xs) = x :: esc xs | esc [] = [] in F ("fun A () = B \"" ^ (implode o esc o explode) x ^ "\"\n" ^ x) end and F x = (print o implode o rev o explode) x

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. ↩

Handlinger