Reflective \(\onehash\)

One sometimes hears the claim that the Recursion Theorem allows one to write programs that “have access to their own source code.” This section makes this precise by formulating an an extension of \(\onett\hash\) called Reflective \(\onesharp\) (\(\Ronesharp\)). In \(\Ronesharp\) one can write programs which directly can output themselves without calling on the Recursion Theorem or tricks which we have seen. Then we give a new proof of the Recursion Theorem for \(\Ronesharp\), one which is perhaps simpler conceptually than the proofs which we have seen. As a bonus, we will use \(\Ronesharp\) to directly implement recursive definitions, as mentioned in the previous section. Along the way, we will be interested in the relation between \(\onesharp\) and \(\Ronesharp\).

The language \(\Ronesharp\) extends \(\onett\hash\) by adding one extra programming construct, the instruction \(\onett\hash^6\). This instruction may be used anywhere in a program (\(p\)), and when it is used, we take \(p\) itself and write them to R1, after whatever happens to be in R1.

The main equation about this construct is

\[ \semantics{\onett\hash^6 + x }( \ ) \simeq \semantics{x}(\onett\hash^6 + x) \]

Please keep in mind that \(\Ronesharp\) extends \(\onett\hash\). So if \(x\) is a program of \(\onehash\), then viewing it as a program of \(\Ronesharp\) should not change any how it works. That is, \(\semantics{x}(\ybar)\) as a program of \(\Ronesharp\) has the same value as \(\semantics{x}(\ybar)\) as a program of \(\onesharp\).

Theorem 11

For each natural number \(n\), the following hold:

1. There is a universal program \(\uprog_n\) for \(\Ronesharp\). Indeed, there is a \(\onesharp\)-program \(\uprog_n\) such that for all words \(x\) and all \(n\)-tuples \(\ybar\), \(\semantics{\uprog_n}(x,\ybar) \simeq \semantics{x}(\ybar)\), where the latter program is in \(\Ronesharp\).

2. For each program \(p\) of \(\Ronesharp\) there is a program \(\widehat{p}\) of \(\onesharp\) such that \(\semantics{p}\) and \(\semantics{\widehat{p}}\) agree as \(n\)-place partial functions.

3. The Recursion Theorem for \(\Ronesharp\): for all \(p\) there is some \(q^*\) so that for all \(n\)-tuples \(\ybar\), \([\![ q^* ]\!](\ybar) \simeq [\![p]\!] (q^*,\ybar)\), with these computations being in \(\Ronesharp\).

Proof. For (1), we need only change the universal program of \(\onesharp\) in a minor way.

Part (2) follows immediately from part (1) and the observation that \(\uprog_n\) is a program of \(\onesharp\).

Here is the proof of (3). We are given a program \(p\). Let \(q^*\) be the following program of \(\Ronesharp\):

\[ \moveprog_{n,n+2} + \moveprog_{n-1, n+1} + \cdots + \moveprog_{1,3} + \onett\hash^6 + \moveprog_{1,2} + \semantics{\writeprog}(p) + \uprog_{n+1} \]

We are using part (1) to get \(\uprog_{n+1}\). In words, \(q^*\) takes a tuple \(\ybar = y_1, \ldots, y_n\) and moves each down two registers, so as to free up R1 and R2. Then \(q^*\) “spits itself out” into R1, moves this to R2, and then writes \(p\) to R1. Finally it applies \(\uprog_{n+1}\) to what is in the registers. To review and then go on:

\[\begin{split} \begin{array}{cl} & \semantics{q^*}( \ybar ) \\ %\simeq & \semantics{ %\moveprog_{n,n+3} + \cdots + % \moveprog_{1,3} + \semantics{\writeprog}(p) + \moveprog_{1,2} + \uprog_{n+1} }(q^*,\ybar)\\ \simeq & \semantics{ \onett\hash^6 +\moveprog_{1,2} + \semantics{\writeprog}(p) + \uprog_{n+1}}(\eps,\eps, y_1, \ldots, y_n) \\ \simeq & \semantics{ \moveprog_{1,2} + \semantics{\writeprog}(p) + \uprog_{n+1}}(q^*,\eps, y_1, \ldots, y_n) \\ \simeq & \semantics{ \semantics{\writeprog}(p) + \uprog_{n+1}}(\eps,q^*, y_1, \ldots, y_n) \\ \simeq &\semantics{\uprog_{n+1}}(p,q^*,\ybar) \\ \simeq & \semantics{p}(q^*,\ybar) \end{array} \end{split}\]

Exercise 86

What happens when we run the programs below on all empty registers?

1. \(\onett\hash^6 + \onett\hash^6 \)

2. \(\onett\hash^6 + \clearprog_1 + \onett\hash^6\)

3. \(\onett\hash^6 + \reverseprog\), where \(\reverseprog\) reverses what is in R1.

Exercise 87

This problem has to do with Theorem 11

1. Prove part (2) of using the Recursion Theorem of \(\onehash\) directly. In fact, the Recursion Theorem for \(\onesharp\) implies that there is a translation of programs of \(\Ronesharp\) to programs of \(\onesharp\) that preserves strong equivalence. Find this (short) translation.

2. Can part (3) be proved by simply repeating the proof of Theorem 9?

Exercise 88

Assume that \(\uprog_0\) has the property that whenever \(\semantics{x}(\ )\!\!\downarrow\), the computation of \(\uprog_0\) on \(x\) takes at least as many steps as the run of \(x\) on empty registers. Let \(p\) be the program \(\onett \hash^6 + \uprog_0\). Show that \(\semantics{p}(\ )\!\!\uparrow\).