|
0 |
<html><head><title>The Burro programming language</title></head>
|
|
1 |
<body>
|
|
2 |
|
|
3 |
<h1>Burro</h1>
|
|
4 |
|
|
5 |
<p>October 2007, Chris Pressey, Cat's Eye Technologies.</p>
|
|
6 |
|
|
7 |
<h2>1. Introduction</h2>
|
|
8 |
|
|
9 |
<p><em>Burro</em> is a Brainfuck-like programming language whose programs form an
|
|
10 |
algebraic group under concatenation.</p>
|
|
11 |
|
|
12 |
<p>(At least, that is how I originally would have described it. But that description
|
|
13 |
turns out to be not entirely precise, because the technical meanings of "group" and
|
|
14 |
"program" come into conflict. A more precise statement would be: "Burro is
|
|
15 |
a semi-formal programming language, the set of whose program texts, paired with the operation
|
|
16 |
of concatenation, forms an algebraic group over a semantic equivalence relation."
|
|
17 |
But the first version is close enough for jazz, and rolls off the tongue more easily...)</p>
|
|
18 |
|
|
19 |
<p>Anyway, what does it mean? It means that, among other things, every Burro program has
|
|
20 |
an <em>antiprogram</em> — a series of instructions that can be appended to it
|
|
21 |
to annihilate its behavior. The resulting catenated program has the
|
|
22 |
same semantics as no program at all — a "no-op," or a zero-length program.</p>
|
|
23 |
|
|
24 |
<p>Why is this at all remarkable? Well, take the Brainfuck program fragment <code>[-]+[]</code>.
|
|
25 |
What could you append to it to it to make it into a "no-op" program?
|
|
26 |
Evidently <em>nothing</em>, because once the interpreter enters an infinite loop, it's not
|
|
27 |
going to care what instructions you've put after the loop. And a program that loops forever
|
|
28 |
isn't the same as one that does nothing at all.</p>
|
|
29 |
|
|
30 |
<p>So not all Brainfuck programs have antiprograms. Despite that, Brainfuck does embody a lot of
|
|
31 |
symmetry. Group theory, too, is a branch of
|
|
32 |
mathematics particularly suited to the study of symmetry. And as you might imagine,
|
|
33 |
there is a distinct relation between symmetrical programming languages and reversible
|
|
34 |
programming (even though it may not be immediatly clear exactly what that relationship is.)
|
|
35 |
These are some of the factors that encouraged me to design Burro.</p>
|
|
36 |
|
|
37 |
<h2>2. Background</h2>
|
|
38 |
|
|
39 |
<p>Before explaining Burro, a short look of group theory and of the theory of
|
|
40 |
computation would probably be helpful.</p>
|
|
41 |
|
|
42 |
<h3>Group Theory</h3>
|
|
43 |
|
|
44 |
<p>Recall (or go look up in an abstract algebra textbook) that a <em>group</em> is
|
|
45 |
a pair of a set <var>S</var> and a binary operation
|
|
46 |
· : <var>S</var> × <var>S</var> → <var>S</var>
|
|
47 |
that obeys the following three axioms:</p>
|
|
48 |
|
|
49 |
<ul>
|
|
50 |
|
|
51 |
<li>For any three elements <var>a</var>, <var>b</var>, and <var>c</var> of
|
|
52 |
the set <var>S</var>, (<var>a</var> · <var>b</var>) · <var>c</var> =
|
|
53 |
<var>a</var> · (<var>b</var> · <var>c</var>). In other words,
|
|
54 |
the operation is "associative." Parentheses don't matter, and we generally leave them out.</li>
|
|
55 |
|
|
56 |
<li>There exists some element of <var>S</var>, which we call <b>e</b>, such that
|
|
57 |
<var>a</var> · <b>e</b> = <b>e</b> · <var>a</var> = <var>a</var>
|
|
58 |
for every element <var>a</var> of <var>S</var>. Think of
|
|
59 |
<b>e</b> as a "neutral" element that just doesn't contribute anything.</li>
|
|
60 |
|
|
61 |
<li>For every element <var>a</var> of <var>S</var> there is an element
|
|
62 |
<var>a'</var> of <var>S</var> such that <var>a</var> · <var>a'</var> = <b>e</b>.
|
|
63 |
That is, for any element, you can find some element that "annihilates" it.</li>
|
|
64 |
|
|
65 |
</ul>
|
|
66 |
|
|
67 |
<p>There are lots of examples of groups — the integers under the operation of
|
|
68 |
addition, for example, where <b>e</b> is 0, and the annihilator for any integer
|
|
69 |
is simply its negative (because <var>x</var> + (-<var>x</var>) always equals 0.)</p>
|
|
70 |
|
|
71 |
<p>There are also lots of things you can prove are true about any group
|
|
72 |
(that is, about groups in general.) For instance, that <b>e</b> is unique: if
|
|
73 |
<var>a</var> · <var>x</var> = <var>a</var> and
|
|
74 |
<var>a</var> · <var>y</var> = <var>a</var> then
|
|
75 |
<var>x</var> = <var>y</var> = <b>e</b>. (This particular property will
|
|
76 |
become relevant very soon, so keep it in mind as you read the next section.)</p>
|
|
77 |
|
|
78 |
<p>The set on which a group is based can have any number of elements. Research
|
|
79 |
and literature in group theory often concentrates on finite groups, because these
|
|
80 |
are in some ways more interesting, and they are useful in error-correcting
|
|
81 |
codes and other applications. However, the set of Burro programs is countably
|
|
82 |
infinite, so we will be dealing with infinite groups here.</p>
|
|
83 |
|
|
84 |
<h3>Theory of Computation</h3>
|
|
85 |
|
|
86 |
<p>I don't need to call on a lot of theory of computation here except to point
|
|
87 |
out one fact: for any program, there are an infinite number of equivalent programs.
|
|
88 |
There are formal proofs of this, but they can be messy, and it's something
|
|
89 |
that should be obvious to most programmers. Probably the simplest example, in Brainfuck,
|
|
90 |
is that <code>+-</code>, <code>++--</code>, <code>+++---</code>, <code>++++----</code>,
|
|
91 |
etc., all have the same effect.</p>
|
|
92 |
|
|
93 |
<p>To be specific, by "program" here I mean "program text" in a
|
|
94 |
particular language; if we're talking about "abstract programs" in no particular
|
|
95 |
language, then you could well say that there is only and exactly one program that
|
|
96 |
does any one thing, it's just that there are an infinite number of concrete
|
|
97 |
representations of it.</p>
|
|
98 |
|
|
99 |
<p>This distinction becomes important with respect to treating programs
|
|
100 |
as elements of a group, like we're doing in Burro. Some program will
|
|
101 |
be the neutral element <b>e</b>. But either <em>many</em> programs will
|
|
102 |
be equivalent to this program — in which case <b>e</b> is not unique, contrary to
|
|
103 |
what group theory tells us — or we are talking about abstract programs
|
|
104 |
independent of any programming language, in which case our goal of defining a particular
|
|
105 |
language called "Burro" for this purpose seems a bit futile.</p>
|
|
106 |
|
|
107 |
<p>There are a couple of ways this could be resolved. We could foray into
|
|
108 |
domain theory, and try to impose a group structure on the semantics of programs
|
|
109 |
irrespective of the language they are in. Or we could venture into representation
|
|
110 |
theory, and see if the program texts can act as generators of the group elements.
|
|
111 |
Both of these approaches could be interesting, but I chose an approach that I
|
|
112 |
found to be less of a distraction, and possibly more intuitive, at the cost of
|
|
113 |
introducing a slight variation on the notion of a group.</p>
|
|
114 |
|
|
115 |
<h3>Group Theory, revisited</h3>
|
|
116 |
|
|
117 |
<p>To this end, let's examine the idea of a <em>group over an equivalence relation</em>.
|
|
118 |
All this is, really, is being specific about what constitutes "equals" in those
|
|
119 |
group axioms I listed earlier. In mathematics there is a well-established notion of
|
|
120 |
an <em>equivalence relation</em> — a relationship between elements
|
|
121 |
which paritions a set into
|
|
122 |
disjoint equivalence classes, where every element in a class is considered
|
|
123 |
equivalent to every other element in that same class (and inequivalent to any
|
|
124 |
element in any other class.)</p>
|
|
125 |
|
|
126 |
<p>We can easily define an equivalence relation on programs (that is,
|
|
127 |
program texts.) We simply say that two programs are
|
|
128 |
equivalent if they have the same semantics: they map the same inputs to the
|
|
129 |
same outputs, they compute the same function, they "do the same thing" as
|
|
130 |
far as an external observer can tell, assuming he or she is unconcerned with
|
|
131 |
performance issues. As you can imagine, this relation will be very useful for
|
|
132 |
our purpose.</p>
|
|
133 |
|
|
134 |
<p>We can also reformulate the group axioms using an equivalence relation.
|
|
135 |
At the very least, I can't see why it should be invalid to do so. (Indeed, this seems to
|
|
136 |
be the general idea behind using "quotients" in abstract algebra. In our case, we
|
|
137 |
have a set of program texts and a "semantic" equivalence relation "are equivalent
|
|
138 |
programs", and the quotient set is the set of all computable functions
|
|
139 |
regardless of their concrete representation.)</p>
|
|
140 |
|
|
141 |
<p>So let's go ahead and take that liberty. The resulting algebraic structure
|
|
142 |
should be quite similar to what we had before,
|
|
143 |
but with the equivalence classes becoming the real "members" of the group,
|
|
144 |
and with each class containing many individual elements which are treated
|
|
145 |
interchangably with respect to the group axioms.</p>
|
|
146 |
|
|
147 |
<p>I'll summarize the modified definition here. A <em>group over an equivalence relation</em>
|
|
148 |
is a triple ⟨<var>S</var>,·,≡⟩ where:</p>
|
|
149 |
<ul>
|
|
150 |
<li><var>S</var> is a set</li>
|
|
151 |
<li>· : <var>S</var> × <var>S</var> → <var>S</var> is a binary operation over <var>S</var></li>
|
|
152 |
<li>≡ is a reflexive, transitive, and symmetrical binary relation over <var>S</var></li>
|
|
153 |
</ul>
|
|
154 |
<p>where the following axioms are also satisfied:</p>
|
|
155 |
<ul>
|
|
156 |
<li>∀ <var>a</var>, <var>b</var>, <var>c</var> ∈ <var>S</var>: (<var>a</var> · <var>b</var>) · <var>c</var> ≡
|
|
157 |
<var>a</var> · (<var>b</var> · <var>c</var>)</li>
|
|
158 |
<li>∃ <b>e</b> ∈ <var>S</var>: ∀ <var>a</var> ∈ <var>S</var>: <var>a</var> · <b>e</b> ≡ <b>e</b> · <var>a</var> ≡ <var>a</var></li>
|
|
159 |
<li>∀ <var>a</var> ∈ <var>S</var>: ∃ <var>a'</var> ∈ <var>S</var>: <var>a</var> · <var>a'</var> ≡ <b>e</b></li>
|
|
160 |
</ul>
|
|
161 |
|
|
162 |
<p>Every theorem that applies to groups should be easy to modify to be applicable
|
|
163 |
to a group over an equivalence relation: just replace = with ≡. So what
|
|
164 |
we have, for example, is that while any given <b>e</b> itself might not be unique, the
|
|
165 |
equivalence class <b>E</b> ⊆ <var>S</var> that contains it is:
|
|
166 |
<b>E</b> is the only equivalence class that contains
|
|
167 |
elements like <b>e</b> and, for the purposes of the group, all of these elements are
|
|
168 |
interchangeable.</p>
|
|
169 |
|
|
170 |
<h2>3. Syntax and Semantics</h2>
|
|
171 |
|
|
172 |
<h3>Five-instruction Foundation</h3>
|
|
173 |
|
|
174 |
<p>Burro is intended to be Brainfuck-like, so we could start by examining which
|
|
175 |
parts of Brainfuck are already suitable for Burro and which parts will have to
|
|
176 |
be modified or rejected.</p>
|
|
177 |
|
|
178 |
<p>First, note that Brainfuck is traditionally very lenient about what
|
|
179 |
constitutes a "no-op" instruction. Just about any symbol that isn't explicitly
|
|
180 |
mentioned in the instruction set is treated as a no-op (and this behaviour turns
|
|
181 |
out to be useful for inserting comments in programs.) In Burro, however, we'll
|
|
182 |
strive for better clarity by defining an explicit "no-op" instruction. For
|
|
183 |
consistency with the group theory side of things, we'll call it <code>e</code>.
|
|
184 |
(Of course, we won't forget that <code>e</code> lives in an equivalence class
|
|
185 |
with other things like <code>+-</code> and the zero-length program, and all
|
|
186 |
of these things are semantically interchangeable. But <code>e</code> gives
|
|
187 |
us a nice, single-symbol, canonical program form when we want to talk about it.)</p>
|
|
188 |
|
|
189 |
<p>Now let's consider the basic Brainfuck instructions <code>+</code>, <code>-</code>,
|
|
190 |
<code><</code>, and <code>></code>. They have a nice, symmetrical
|
|
191 |
organization that is ideally suited to group structure, so we will adopt them
|
|
192 |
in our putative Burro design.</p>
|
|
193 |
|
|
194 |
<p>On the other hand, the instructions <code>.</code> and <code>,</code> will require
|
|
195 |
devising some kind of annihilator for interactive input and output. This seems
|
|
196 |
difficult at least, and not really necessary if we're willing to forego writing
|
|
197 |
"Hunt the Wumpus" in Burro, so we'll leave them out for now. The only input for a
|
|
198 |
Burro program is, instead, the initial state of the tape, and the only output is the
|
|
199 |
final state.</p>
|
|
200 |
|
|
201 |
<p>In addition, <code>[</code> and <code>]</code> will cause problems, because
|
|
202 |
as we saw in the introduction, <code>[-]+[]</code> is an infinite loop, and it's
|
|
203 |
not clear what we could use to annihilate it. We'll defer this question for later
|
|
204 |
and for the meantime leave these instructions out, too.</p>
|
|
205 |
|
|
206 |
<p>What we're left in our "Burro-in-progress" is essentially a very weak subset of
|
|
207 |
Brainfuck, with only the five instructions <code>+-><e</code>. But this is
|
|
208 |
a starting point that we can use to see if we're on the right track. Do the
|
|
209 |
programs formed from strings of these instructions form a group under concatenation
|
|
210 |
over the semantic equivalence relation? i.e., Does every Burro program so far
|
|
211 |
have an inverse?</p>
|
|
212 |
|
|
213 |
<p>Let's see. For every <i>single-instruction</i> Burro
|
|
214 |
program, we can evidently find another Burro instruction that, when appended to
|
|
215 |
it, "cancels it out" and makes a program with the same semantics as <code>e</code>:</p>
|
|
216 |
|
|
217 |
<table border=1 cellpadding=5>
|
|
218 |
<tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
|
|
219 |
<tr><td align="center"><code>+</code></td><td align="center"><code>-</code></td>
|
|
220 |
<td align="center"><code>+-</code></td><td align="center"><code>e</code></td></tr>
|
|
221 |
<tr><td align="center"><code>-</code></td><td align="center"><code>+</code></td>
|
|
222 |
<td align="center"><code>-+</code></td><td align="center"><code>e</code></td></tr>
|
|
223 |
<tr><td align="center"><code>></code></td><td align="center"><code><</code></td>
|
|
224 |
<td align="center"><code>><</code></td><td align="center"><code>e</code></td></tr>
|
|
225 |
<tr><td align="center"><code><</code></td><td align="center"><code>></code></td>
|
|
226 |
<td align="center"><code><></code></td><td align="center"><code>e</code></td></tr>
|
|
227 |
<tr><td align="center"><code>e</code></td><td align="center"><code>e</code></td>
|
|
228 |
<td align="center"><code>ee</code></td><td align="center"><code>e</code></td></tr>
|
|
229 |
</table>
|
|
230 |
|
|
231 |
<p>Note that we once again should be more explicit about our requirements than
|
|
232 |
Brainfuck. We need to have a tape which is infinite in both directions, or else
|
|
233 |
<code><</code> wouldn't always be the inverse of <code>></code> (because sometimes
|
|
234 |
it'd fail in some way like falling off the edge of the tape.) And, so that we don't have
|
|
235 |
to worry about overflow and all that rot,
|
|
236 |
let's say cells can take on any unbounded negative or positive integer value, too.</p>
|
|
237 |
|
|
238 |
<p>But does this hold for <em>any</em> Burro program? We can use structural
|
|
239 |
induction to determine this.
|
|
240 |
Can we find inverses for every Burro program, concatenated with a given
|
|
241 |
instruction? (In the following table,
|
|
242 |
<i>b</i> indicates any Burro program, and <i>b'</i> its inverse.
|
|
243 |
Also note that <i>bb'</i> is, by definition, <code>e</code>.)</p>
|
|
244 |
|
|
245 |
<table border=1 cellpadding=5>
|
|
246 |
<tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
|
|
247 |
<tr><td align="center"><code><i>b</i>+</code></td><td align="center"><code>-<i>b'</i></code></td>
|
|
248 |
<td align="center"><code><i>b</i>+-<i>b'</i></code> ≡ <code><i>b</i>e<i>b'</i></code> ≡ <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
249 |
<tr><td align="center"><code><i>b</i>-</code></td><td align="center"><code>+<i>b'</i></code></td>
|
|
250 |
<td align="center"><code><i>b</i>-+<i>b'</i></code> ≡ <code><i>b</i>e<i>b'</i></code> ≡ <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
251 |
<tr><td align="center"><code><i>b</i>></code></td><td align="center"><code><<i>b'</i></code></td>
|
|
252 |
<td align="center"><code><i>b</i>><<i>b'</i></code> ≡ <code><i>b</i>e<i>b'</i></code> ≡ <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
253 |
<tr><td align="center"><code><i>b</i><</code></td><td align="center"><code>><i>b'</i></code></td>
|
|
254 |
<td align="center"><code><i>b</i><><i>b'</i></code> ≡ <code><i>b</i>e<i>b'</i></code> ≡ <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
255 |
<tr><td align="center"><code><i>b</i>e</code> ≡ <code><i>b</i></code></td><td align="center"><code>e<i>b'</i></code> ≡ <code><i>b'</i>e</code> ≡ <code><i>b'</i></code></td>
|
|
256 |
<td align="center"><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
257 |
</table>
|
|
258 |
|
|
259 |
<p>Looks good. However, this isn't an abelian group, and concatenation is definately not
|
|
260 |
commutative. So, to be complete, we need a table going in the other direction, too: concatenation of a
|
|
261 |
given instruction with any Burro program.</p>
|
|
262 |
|
|
263 |
<table border=1 cellpadding=5>
|
|
264 |
<tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
|
|
265 |
<tr><td align="center"><code>+<i>b</i></code></td><td align="center"><code><i>b'</i>-</code></td>
|
|
266 |
<td align="center"><code>+<i>bb'</i>-</code> ≡ <code>+e-</code> ≡ <code>+-</code></td><td align="center"><code>e</code></td></tr>
|
|
267 |
<tr><td align="center"><code>-<i>b</i></code></td><td align="center"><code><i>b'</i>+</code></td>
|
|
268 |
<td align="center"><code>-<i>bb'</i>+</code> ≡ <code>-e+</code> ≡ <code>-+</code></td><td align="center"><code>e</code></td></tr>
|
|
269 |
<tr><td align="center"><code>><i>b</i></code></td><td align="center"><code><i>b'</i><</code></td>
|
|
270 |
<td align="center"><code>><i>bb'</i><</code> ≡ <code>>e< ≡ <code>><</code></td><td align="center"><code>e</code></td></tr>
|
|
271 |
<tr><td align="center"><code><<i>b</i></code></td><td align="center"><code><i>b'</i>></code></td>
|
|
272 |
<td align="center"><code><<i>bb'</i>></code> ≡ <code><e> ≡ <code><></code></td><td align="center"><code>e</code></td></tr>
|
|
273 |
<tr><td align="center"><code>e<i>b</i></code> ≡ <code><i>b</i></code></td><td align="center"><code><i>b'</i>e</code> ≡ <code>e<i>b'</i></code> ≡ <code><i>b'</i></code></td>
|
|
274 |
<td align="center"><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
275 |
</table>
|
|
276 |
|
|
277 |
<p>So far, so good, I'd say. Now we can address to the problem of how to
|
|
278 |
restrengthen the language so that it remains as powerful as Brainfuck.</p>
|
|
279 |
|
|
280 |
<h3>Loops</h3>
|
|
281 |
|
|
282 |
<p>Obviously, in order for Burro to be as capable as Brainfuck,
|
|
283 |
we would like to see some kind of looping mechanism in it. But, as we've
|
|
284 |
seen, Brainfuck's is insufficient for our purposes, because it allows for
|
|
285 |
the construction of infinite loops that we can't invert by concatenation.</p>
|
|
286 |
|
|
287 |
<p>We could insist that all loops be finite, but that would make
|
|
288 |
Burro less powerful than Brainfuck — it would only be capable of expressing
|
|
289 |
the primitive recursive functions. The real challenge is in having Burro be Turing-complete,
|
|
290 |
like Brainfuck.</p>
|
|
291 |
|
|
292 |
<p>This situation looks dire, but there turns out to be a way. What we
|
|
293 |
do is borrow the trick used in languages like L00P and Version (and probably
|
|
294 |
many others.) We put a single, implicit loop around the whole program.
|
|
295 |
(There is a classic formal proof that this is sufficient — the interested
|
|
296 |
reader is referred to the paper "Kleene algebra with tests"<sup><a href="#1">1</a></sup>,
|
|
297 |
which gives a brief history, references, and its own proof.)</p>
|
|
298 |
|
|
299 |
<p>This single implicit loop will be conditional on a special flag, which
|
|
300 |
we'll call the "halt flag", and we'll stipulate is initially set.
|
|
301 |
If this flag is still set when the end of the program is reached, the program halts.
|
|
302 |
But if it is unset when the end of the program is reached, the flag is reset
|
|
303 |
and the program repeats from the beginning. (Note that although the halt flag
|
|
304 |
is reset, all other program state (i.e. the tape) is left alone.)</p>
|
|
305 |
|
|
306 |
<p>To manipulate this flag, we introduce a new instruction:</p>
|
|
307 |
|
|
308 |
<table border=1 cellpadding=5>
|
|
309 |
<tr><th>Instruction</th><th>Semantics</th></tr>
|
|
310 |
<tr><td align="center"><code>!</code></td><td>Toggle halt flag</td></tr>
|
|
311 |
</table>
|
|
312 |
|
|
313 |
<p>Then we check that adding this instruction to Burro's instruction set
|
|
314 |
doesn't change the fact that Burro programs form a group:</p>
|
|
315 |
|
|
316 |
<table border=1 cellpadding=5>
|
|
317 |
<tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
|
|
318 |
<tr><td align="center"><code>!</code></td><td align="center"><code>!</code></td>
|
|
319 |
<td align="center"><code>!!</code></td><td align="center"><code>e</code></td></tr>
|
|
320 |
<tr><td align="center"><code>!<i>b</i></code></td><td align="center"><code><i>b'</i>!</code></td>
|
|
321 |
<td align="center"><code>!<i>bb'</i>!</code> ≡ <code>!e!</code> ≡ <code>!!</code></td><td align="center"><code>e</code></td></tr>
|
|
322 |
<tr><td align="center"><code><i>b</i>!</code></td><td align="center"><code>!<i>b'</i></code></td>
|
|
323 |
<td align="center"><code><i>b</i>!!<i>b'</i></code> ≡ <code><i>beb'</i></code> ≡ <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
324 |
</table>
|
|
325 |
|
|
326 |
<p>Seems so. Now we can write Burro programs that halt, and Burro programs that loop
|
|
327 |
forever. What we need next is for the program to be able to decide this behaviour
|
|
328 |
for itself.</p>
|
|
329 |
|
|
330 |
<h3>Conditionals</h3>
|
|
331 |
|
|
332 |
<p>OK, this is the ugly part.</p>
|
|
333 |
|
|
334 |
<p>Let's add a simple control structure to Burro. Since we already have repetition, this
|
|
335 |
will only be for conditional execution. To avoid confusion with Brainfuck, we'll avoid <code>[]</code>
|
|
336 |
entirely; instead, we'll use <code>()</code>
|
|
337 |
to indicate "execute the enclosed code (once) if and only if the current cell is non-zero".</p>
|
|
338 |
|
|
339 |
<p>Actually, let's make it a bit fancier, and allow an "else" clause to be inserted in it,
|
|
340 |
like so: <code>(/)</code> where the code before the <code>/</code> is executed iff the cell
|
|
341 |
is non-zero, and the code after the <code>/</code> is executed iff it is zero.</p>
|
|
342 |
|
|
343 |
<p>(The reasons for this design choice are subtle. They come down to the fact that
|
|
344 |
in order to find an inverse of a conditional, we need to invert the sense of the test.
|
|
345 |
In a higher-level language, we could use a Boolean NOT operation for this. However, in
|
|
346 |
Brainfuck, writing a NOT requires a loop, and thus a conditional. Then we're stuck
|
|
347 |
with deciding how to invert the sense of <em>that</em> conditional, and so forth. By
|
|
348 |
providing NOT-like behaviour as a built-in courtesy of <code>/</code>, we dodge the
|
|
349 |
problem entirely. If you like, you can think of it as meeting the aesthetic demands of
|
|
350 |
a symmetrical language: the conditional structures are symmetrical too.)</p>
|
|
351 |
|
|
352 |
<p>A significant difference here with Brainfuck is that, while Brainfuck is a bit
|
|
353 |
lacksidaisical about matching up <code>[</code>'s with <code>]</code>'s, we explicitly
|
|
354 |
<em>disallow</em> parentheses that do not nest correctly in Burro. A Burro program with mismatched
|
|
355 |
parentheses is an ill-formed Burro program, and thus not really a Burro program at all.
|
|
356 |
We turn up our nose at it; we aren't even interested in whether we can find an
|
|
357 |
inverse of it, because we don't acknowledge it. This applies to the placement of
|
|
358 |
<code>/</code> outside of parentheses, or the absence of <code>/</code> in parentheses,
|
|
359 |
as well.</p>
|
|
360 |
|
|
361 |
<p>(The reasons for this design choice are also somewhat subtle. I originally wanted
|
|
362 |
to deal with this by saying that <code>(</code>, <code>/</code>, and <code>)</code>
|
|
363 |
could come in any order, even a nonsensical one, and still make a valid Burro program,
|
|
364 |
only with the semantics of "no-op" or "loop forever" or something equally representative of
|
|
365 |
"broken." You see this quite often in toy formal languages, and the resulting lack of
|
|
366 |
syntax would seem to allow the set of Burro instructions to be a "free generator" of
|
|
367 |
the group of Burro programs, which sounds like it might have very nice
|
|
368 |
abstract-algebraical properties.
|
|
369 |
The problem is that it potentially interferes with the whole "finding an
|
|
370 |
antiprogram" thing. If a Burro program with mismatched parentheses has the
|
|
371 |
semantics of "no-op", then every Burro program has a trivial annihilator: just
|
|
372 |
tack on an unmatching parenthesis. Similarly, if malformed programs are
|
|
373 |
considered to loop forever, how do you invert them? So, for these reasons,
|
|
374 |
Burro has some small amount of syntax — a bit more than Brainfuck is usually
|
|
375 |
considered to have, but not much.)</p>
|
|
376 |
|
|
377 |
<p>Now, it turns out we will have to do a fair bit of work on <code>()</code> in order
|
|
378 |
to make it so that we can always find a bit of code that is the inverse of some other
|
|
379 |
bit of code that includes <code>()</code>.</p>
|
|
380 |
|
|
381 |
<p>We can't just make it a "plain old if", because by the time we've finished executing an "if",
|
|
382 |
we don't know which branch was executed — so we have no idea what the "right"
|
|
383 |
inverse of it would be. For example,</p>
|
|
384 |
|
|
385 |
<ul><code>(-/e)</code></ul>
|
|
386 |
|
|
387 |
<p>After this has finished executing, the current cell could contain 0 - but is that because it
|
|
388 |
was already 0 before the <code>(</code> was encountered, and nothing happened to it
|
|
389 |
inside the "if"... or is it because it was 1 before
|
|
390 |
the <code>(</code> was encountered, and decremented to 0 by the <code>-</code>
|
|
391 |
instruction inside the "if"?
|
|
392 |
It could be either, and we don't know — so we can't find an inverse.</p>
|
|
393 |
|
|
394 |
<p>We remedy this in a somewhat disappointingly uninteresting way: we make a copy of
|
|
395 |
the value being tested and squirrel it away for future reference, so that pending code
|
|
396 |
can look at it and tell what decision was made, and in so doing, act appropriately to
|
|
397 |
invert it.</p>
|
|
398 |
|
|
399 |
<p>This information that we squirrel away is, I would say, a kind of <em>continuation</em>.
|
|
400 |
It's not a full-bodied continuation, as the term continuation is often used, in the
|
|
401 |
sense of "function representing the entire remainder of the computation."
|
|
402 |
But, it's a bit of context that is retained during execution that is intended to affect
|
|
403 |
some future control flow decision — and that's the basic purpose of a continuation.
|
|
404 |
So, I will call it a continuation, although it is perhaps a diminished sort of continuation.
|
|
405 |
(In this sense, the machine stack where arguments and
|
|
406 |
return addresses are stored in a language like C is also a kind of continuation.)</p>
|
|
407 |
|
|
408 |
<p>These continuations that we maintain, these pieces of information that tell us how
|
|
409 |
to undo things in the future, do need to have an orderly relationship with each other.
|
|
410 |
Specifically, we need to remember to undo the more recent conditionals first. So, we
|
|
411 |
retain the continuations in a FIFO discipline, like a stack. Whenever a <code>(</code> is
|
|
412 |
executed, we "push" a continuation into storage, and when we need to invert the effect
|
|
413 |
of a previous conditional, we "pop" a continuation from storage.</p>
|
|
414 |
|
|
415 |
<p>To actually accomplish this latter action we need to define the control structure
|
|
416 |
for undoing conditional tests. We introduce the construct
|
|
417 |
<code>{\}</code>, which works just like <code>(/)</code>, except that the value that it tests
|
|
418 |
doesn't come from the tape — instead, it comes from the continuation. We establish similar
|
|
419 |
syntactic rules about matching every <code>{</code> with a <code>}</code> and an
|
|
420 |
intervening <code>\</code>, in addition to a rule that says every <code>{\}</code>
|
|
421 |
must be preceded by a <code>(/)</code>.</p>
|
|
422 |
|
|
423 |
<p>With this, we're very close to having an inverse for conditionals. Consider:</p>
|
|
424 |
|
|
425 |
<ul><code>(-/e){+\e}</code></ul>
|
|
426 |
|
|
427 |
<p>If the current cell contains 0 after <code>(-/e)</code>, the continuation will contain either
|
|
428 |
a 1 or a 0 (the original contents of the cell.) If the continuation contains a 0, the "else" part of
|
|
429 |
<code>{+\e}</code> will be executed — i.e. nothing will happen. On the other hand, if the
|
|
430 |
continuation contains a 1, the "then" part of <code>{+\e}</code> will be executed.
|
|
431 |
Either way, the tape is correctly restored to its original (pre-<code>(-/e)</code>) state.</p>
|
|
432 |
|
|
433 |
<p>There are still a few details to clean up, though.
|
|
434 |
Specifically, we need to address nesting. What if we're given</p>
|
|
435 |
|
|
436 |
<ul><code>(>(<+/e)/e)</code></ul>
|
|
437 |
|
|
438 |
<p>How do we form an inverse of this? How would the following work?</p>
|
|
439 |
|
|
440 |
<ul><code>(>(<+/e)/e){{->\e}<\e}</code></ul>
|
|
441 |
|
|
442 |
<p>The problem with this, if we collect continuations using only a naive stack arrangement,
|
|
443 |
is that we don't remember how many times a <code>(</code> was encountered before a
|
|
444 |
matching <code>)</code>. The retention of continuations is still FIFO, but we need
|
|
445 |
more control over the relationships between the continuations.</p>
|
|
446 |
|
|
447 |
<p>The nested structure of the <code>(/)</code>'s suggests a nested structure
|
|
448 |
for collecting continuations.
|
|
449 |
Whenever we encounter a <code>(</code> and we "push" a continuation into storage,
|
|
450 |
that continuation becomes the root for a new collection of continuations
|
|
451 |
(those that occur <em>inside</em> the present conditional, up to the matching
|
|
452 |
<code>)</code>.) Since each continuation is both part of some FIFO series of
|
|
453 |
continuations, and has the capacity to act as the root of it's <em>own</em> FIFO series
|
|
454 |
of continuations, the continuations are arranged in a structure that is
|
|
455 |
more a binary tree than a stack.</p>
|
|
456 |
|
|
457 |
<p>This is perhaps a little complicated, so I'll summarize it in this table.
|
|
458 |
Since this is a fairly operational description, I'll use the term "tree node"
|
|
459 |
instead of continuation to help you visualize it. Keep in mind that at any
|
|
460 |
given time there is a "current continuation" and thus a current tree node.</p>
|
|
461 |
|
|
462 |
<table border=1 cellpadding=5>
|
|
463 |
<tr><th>Instruction</th><th>Semantics</th></tr>
|
|
464 |
<tr><td align="center"><code>(</code></td><td>
|
|
465 |
<ul>
|
|
466 |
<li>Create a new tree node with the contents of the current cell</li>
|
|
467 |
<li>Add that new node as a child of the current node</li>
|
|
468 |
<li>Make that new node the new current node</li>
|
|
469 |
<li>If the current cell is zero, skip one instruction past the matching <code>/</code></li>
|
|
470 |
</ul>
|
|
471 |
</td></tr>
|
|
472 |
<tr><td align="center"><code>/</code></td><td>
|
|
473 |
<ul>
|
|
474 |
<li>Skip to the matching <code>)</code></li>
|
|
475 |
</ul>
|
|
476 |
</td></tr>
|
|
477 |
<tr><td align="center"><code>)</code></td><td>
|
|
478 |
<ul>
|
|
479 |
<li>Make the parent of the current node the new current node</li>
|
|
480 |
</ul>
|
|
481 |
</td></tr>
|
|
482 |
<tr><td align="center"><code>{</code></td><td>
|
|
483 |
<ul>
|
|
484 |
<li>Make the most recently added child of the current node the new current node</li>
|
|
485 |
<li>If the value of the current node is zero, skip one instruction past the matching <code>\</code></li>
|
|
486 |
</ul>
|
|
487 |
</td></tr>
|
|
488 |
<tr><td align="center"><code>\</code></td><td>
|
|
489 |
<ul>
|
|
490 |
<li>Skip to the matching <code>}</code></li>
|
|
491 |
</ul>
|
|
492 |
</td></tr>
|
|
493 |
<tr><td align="center"><code>}</code></td><td>
|
|
494 |
<ul>
|
|
495 |
<li>Make the parent of the current node the new current node</li>
|
|
496 |
<li>Remove the old current node and all of its children</li>
|
|
497 |
</ul>
|
|
498 |
</td></tr>
|
|
499 |
</table>
|
|
500 |
|
|
501 |
<p>Now, keeping in mind that the continuation structure
|
|
502 |
remains constant across all Burro programs equivalent to <code>e</code>,
|
|
503 |
we can show that control structures have inverses:</p>
|
|
504 |
|
|
505 |
<table border=1 cellpadding=5>
|
|
506 |
<tr><th>Instruction</th><th>Inverse</th><th>Test result</th><th>Concatenation</th><th>Net effect</th></tr>
|
|
507 |
<tr><td align="center"><code><i>a</i>(<i>b</i>/<i>c</i>)<i>d</i></code></td><td align="center"><code><i>d'</i>{<i>b'</i>\<i>c'</i>}<i>a'</i></code></td>
|
|
508 |
<td align="center">zero</td><td align="center"><code><i>acdd'c'a'</i></code> ≡ <code><i>acc'a'</i></code> ≡ <code><i>aa'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
509 |
<tr><td align="center"><code><i>a</i>(<i>b</i>/<i>c</i>)<i>d</i></code></td><td align="center"><code><i>d'</i>{<i>b'</i>\<i>c'</i>}<i>a'</i></code></td>
|
|
510 |
<td align="center">non-zero</td><td align="center"><code><i>abdd'b'a'</i></code> ≡ <code><i>abb'a'</i></code> ≡ <code><i>aa'</i></code></td><td align="center"><code>e</code></td></tr>
|
|
511 |
</table>
|
|
512 |
|
|
513 |
<p>There you have it: every Burro program has an inverse.</p>
|
|
514 |
|
|
515 |
<h2>4. Implementations</h2>
|
|
516 |
|
|
517 |
<p>There are two reference interpreters for Burro. <code>burro.c</code> is
|
|
518 |
written in ANSI C, and <code>burro.hs</code> is written in Haskell.
|
|
519 |
Both are BSD licensed.
|
|
520 |
Hopefully at least one of them is faithful to the execution model.</p>
|
|
521 |
|
|
522 |
<h3><code>burro.c</code></h3>
|
|
523 |
|
|
524 |
<p>The executable produced by compiling <code>burro.c</code> takes the
|
|
525 |
following command-line arguments:</p>
|
|
526 |
|
|
527 |
<ul><code>burro [-d] srcfile.bur</code></ul>
|
|
528 |
|
|
529 |
<p>The named file is loaded as Burro source code. All characters in this file except for
|
|
530 |
<code>><+-(/){\}e!</code> are ignored.</p>
|
|
531 |
|
|
532 |
<p>Before starting the run, the interpreter will read a series of whitespace-separated
|
|
533 |
integers from standard input. These integers
|
|
534 |
are placed on the tape initially, starting from the head-start position, extending right.
|
|
535 |
All unspecified cells are considered to contain 0 initially.</p>
|
|
536 |
|
|
537 |
<p>When the program has halted, all tape cells that were "touched" — either given initially as
|
|
538 |
part of the input, or passed over by the tape head — are output to standard output.</p>
|
|
539 |
|
|
540 |
<p>The meanings of the flags are as follows:</p>
|
|
541 |
|
|
542 |
<ul>
|
|
543 |
<li>The <code>-d</code> flag causes debugging information to be sent to standard error.</li>
|
|
544 |
</ul>
|
|
545 |
|
|
546 |
<p>The C implementation performs no syntax-checking. It approximates the unbounded Burro tape
|
|
547 |
with a tape of finite size (defined by <code>TAPE_SIZE</code>, by default 64K) with
|
|
548 |
cells each capable of containing a C language <code>long</code>.</p>
|
|
549 |
|
|
550 |
<h3><code>burro.hs</code></h3>
|
|
551 |
|
|
552 |
<p>The Haskell version of the reference implementation is meant to be executed from
|
|
553 |
within an interactive Haskell environment, such as Hugs. As such, there is no
|
|
554 |
command-line syntax; the user simply invokes the function <code>burro</code>,
|
|
555 |
which has the signature <code>burro :: String -> Tape -> Tape</code>.
|
|
556 |
A convenience constructor <code>tape :: [Integer] -> Tape</code> creates a tape
|
|
557 |
from the given list of integers, with the head positioned over the leftmost cell.</p>
|
|
558 |
|
|
559 |
<p>The Haskell implementation performs no syntax-checking. Because Haskell supports
|
|
560 |
unbounded lists and arbitrary-precision integers, the Burro tape is modelled faithfully.</p>
|
|
561 |
|
|
562 |
<h2>Discussion</h2>
|
|
563 |
|
|
564 |
<p>I hadn't intended to come up with anything in particular when I started
|
|
565 |
designing Burro. I'm hardly a mathematician, and I didn't know anything
|
|
566 |
about abstract algebra except that I found it intriguing. I suppose that algebraic
|
|
567 |
structures have some of the same appeal as programming languages, what with
|
|
568 |
both dealing with primitive operators, equivalent expression forms, and so forth.</p>
|
|
569 |
|
|
570 |
<p>I was basically struck by the variety of objects that could be shown to have
|
|
571 |
this or that algebraic structure, and I wanted to see how well it would
|
|
572 |
hold up if you tried to apply these structures to programs.</p>
|
|
573 |
|
|
574 |
<p>Why groups? Well, the original design goal for Burro was actually to create a Brainfuck-like language
|
|
575 |
where the set of possible programs forms the most <em>restricted</em>
|
|
576 |
possible magma (i.e. the one with the most additional axioms) under concatenation. It can
|
|
577 |
readily been seen that the set of Brainfuck programs forms a semigroup,
|
|
578 |
even a monoid, under concatenation (left as an exercise for the interested
|
|
579 |
reader.) At the other extreme, if the set of programs forms an abelian group under
|
|
580 |
concatenation, the language probably isn't going to be very Brainfuck-like
|
|
581 |
(since insisting that concatenation be commutative is tantamount to saying
|
|
582 |
that the order of instructions in a program doesn't matter.)
|
|
583 |
This leaves a group as the reasonable target to aim for, so that's what I
|
|
584 |
aimed for.</p>
|
|
585 |
|
|
586 |
<p>But the end result turns out to be related to <em>reversible computing</em>.
|
|
587 |
This shouldn't have been a surprise, since groups are one of the simplest
|
|
588 |
foundations for modelling symmetry; it should have been obvious to me that trying to
|
|
589 |
make programs conform to them, would make them (semantically) symmetrical, and
|
|
590 |
thus reversible. But, it wasn't.</p>
|
|
591 |
|
|
592 |
<p>We may ask: in what sense is Burro reversible? And we may compare it
|
|
593 |
to other esolangs in an attempt to understand.</p>
|
|
594 |
|
|
595 |
<p>Well, it's not reversible in the sense that
|
|
596 |
<a href="http://esolangs.org/wiki/Befreak">Befreak</a> is reversible —
|
|
597 |
you can't pause it at any point, change the direction of execution, and watch it
|
|
598 |
"go backwards". Specifically, you can't "undo" a loop in Burro by executing
|
|
599 |
20 iterations, then turning around and "un-executing" those 20 iterations; instead,
|
|
600 |
you "undo" the loop by neutralizing the toggling of the halt flag. With this approach,
|
|
601 |
inversion is instead <em>like the loop never existed in the first place</em>.</p>
|
|
602 |
|
|
603 |
<p>If one did want to make a Brainfuck-like language which was reversible more in
|
|
604 |
the sense that Befreak is reversible, one approach might be to add rules like
|
|
605 |
"<code>+</code> acts like <code>-</code> if the program counter is incoming from
|
|
606 |
the right". But, I haven't pondered on this approach much at all.</p>
|
|
607 |
|
|
608 |
<p>Conversely, the concatenation concept doesn't have a clear
|
|
609 |
correspondence in a two-dimensional language like Befreak — how do you put two programs
|
|
610 |
next to each other? Side-by-side, top-to-bottom? You would probably need multiple
|
|
611 |
operators, which would definately complicate things.</p>
|
|
612 |
|
|
613 |
<p>It's also not reversible in the same way that
|
|
614 |
<a href="http://esolangs.org/wiki/Kayak">Kayak</a> is reversible —
|
|
615 |
Burro programs need not be palindromes, for instance. In fact, I specifically made
|
|
616 |
the "then" and "else" components of both <code>(/)</code> and <code>{\}</code>
|
|
617 |
occur in the same order, so as to break the reflectional symmetry somewhat, and
|
|
618 |
add some translational similarity.</p>
|
|
619 |
|
|
620 |
<p>Conversely, Kayak doesn't cotton to concatenation too well either.
|
|
621 |
In order to preserve the palindrome nature, concatenation would have to
|
|
622 |
occur both at the beginning and the end simultaneously.
|
|
623 |
I haven't given this idea much thought, and I'm not sure where it'd get you.</p>
|
|
624 |
|
|
625 |
<p>Lastly, we could go outside the world of esolangs and use the
|
|
626 |
definition of reversible computing given by Mike Frank<sup><a href="#2">2</a></sup>:</p>
|
|
627 |
|
|
628 |
<blockquote>When we say reversible computing, we mean performing computation
|
|
629 |
in such a way that any previous state of the computation can always be reconstructed
|
|
630 |
given a description of the current state.</blockquote>
|
|
631 |
|
|
632 |
<p>Burro appears to qualify by this definition — <em>almost</em>. The requirement
|
|
633 |
that we can reconstruct <em>any</em> previous state is a bit heavy. We can definately
|
|
634 |
reconstruct states up to the start of the last loop iteration, if we want to, due to the mechanism
|
|
635 |
(continuations) that we've defined to remember what the program state was before any given
|
|
636 |
conditional.</p>
|
|
637 |
|
|
638 |
<p>But what about <em>before</em> the last loop iteration? Each time we reach the end
|
|
639 |
of the program text with halt flag unset, we repeat execution from the beginning, and
|
|
640 |
when this happens, there might still be one or more continuations in storage that were the
|
|
641 |
result of executing <code>(/)</code>'s that did not have
|
|
642 |
matching <code>{\}</code>'s.</p>
|
|
643 |
|
|
644 |
<p>We didn't say what happens to these "leftover" continuations. In fact, computationally
|
|
645 |
speaking, it doesn't matter: since syntactically no
|
|
646 |
<code>{\}</code> can precede any <code>(/)</code>, those leftover continuations
|
|
647 |
couldn't actually have any affect during the next iteration. Any <code>{\}</code> that
|
|
648 |
might consume them next time 'round must be preceded by a <code>(/)</code> which will
|
|
649 |
produce one for it to consume instead.</p>
|
|
650 |
|
|
651 |
<p>And indeed, discarding any continuation that remains when a Burro program loops
|
|
652 |
means that continuations need occupy only a bounded amount of space during execution (because there
|
|
653 |
is only a fixed number of conditionals in any given Burro program.) This
|
|
654 |
is a desirable thing in a practical implementation, and
|
|
655 |
both the C and Haskell reference implementations do just this.</p>
|
|
656 |
|
|
657 |
<p>But this is an implementation choice, and it would be equally valid to write an interpreter
|
|
658 |
which retains all these leftover continuations. And such an interpreter would qualify as a
|
|
659 |
reversible computer under Mike Frank's definition, since these continuations would allow one
|
|
660 |
to reconstruct the entire computation history of the program.</p>
|
|
661 |
|
|
662 |
<p>On this last point, it's interesting to note the similarity between Burro's continuations
|
|
663 |
and Kayak's bit bucket. Although Burro continuations record the value tested, they really
|
|
664 |
don't <em>need</em> to; they <em>could</em> just
|
|
665 |
contain bits indicating whether the tests were successes or failures. Both emptying
|
|
666 |
the bit bucket, and discarding continuations, results in a destruction of information that
|
|
667 |
prevents reversibility (and thermodynamically "generates heat") but allows for a limit on the amount of
|
|
668 |
storage required.</p>
|
|
669 |
|
|
670 |
<h2>History</h2>
|
|
671 |
|
|
672 |
<p>I began formulating Burro in the summer of 2005.
|
|
673 |
The basic design of Burro was finished by winter of 2005, as was the C implementation.
|
|
674 |
But its release was delayed for several reasons. Mainly, I was busy with other (ostensibly more
|
|
675 |
important) things, like schoolwork. However, I also had the nagging feeling that certain parts of
|
|
676 |
the language were not quite described correctly. These doubts led me to introduce the
|
|
677 |
concept of a group over an equivalence relation, and to decide that Burro needed
|
|
678 |
real syntax rules (lest inverting a Burro program was "too easy.") So it wasn't until spring of 2007
|
|
679 |
that I had a general description that I was satisfied with.
|
|
680 |
I also wanted a better reference implementation, in something a bit more abstract and
|
|
681 |
rigorous than C. So I wrote the Haskell version over the summer of 2007.</p>
|
|
682 |
|
|
683 |
<p>In addition, part of me wanted to write a publishable paper on Burro.
|
|
684 |
After all, group theory and reversible computing are valid and relatively mainstream
|
|
685 |
research topics, so why not? But in the end, considering doing this was really a
|
|
686 |
waste of my time. Densening my writing style to conform to acceptable academic
|
|
687 |
standards of impermeability, and puffing up my "discovery" to acceptable academic
|
|
688 |
standards of self-importance, really didn't appeal to me. There's no sense pretending,
|
|
689 |
in high-falutin' language, that Burro represents some profound advance in human
|
|
690 |
knowledge. It's just something neat that I built! And in the end it seemed
|
|
691 |
just as valuable, if not moreso, to try to turn esolangers on to group theory than
|
|
692 |
to turn academics on to Brainfuck...</p>
|
|
693 |
|
|
694 |
<p>Happy annihilating!</p>
|
|
695 |
|
|
696 |
<p>-Chris Pressey
|
|
697 |
<br>Cat's Eye Technologies
|
|
698 |
<br>October 26, 2007
|
|
699 |
<br>Windsor, Ontario, Canada</p>
|
|
700 |
|
|
701 |
<h2>Footnotes</h2>
|
|
702 |
|
|
703 |
<ul>
|
|
704 |
<li><a name="1"><sup>1</sup>Dexter Kozen. <a href="http://www.cs.cornell.edu/~kozen/papers/ckat.ps">Kleene algebra with tests</a>. <i>Transactions on Programming Languages and
|
|
705 |
Systems</i>, 19(3):427-443, May 1997.</a></li>
|
|
706 |
<li><a name="2"><sup>2</sup>Michael Frank. What's Reversible Computing? <code><a href="http://www.cise.ufl.edu/~mpf/rc/what.html">http://www.cise.ufl.edu/~mpf/rc/what.html</a></code></a></li>
|
|
707 |
|
|
708 |
</ul>
|
|
709 |
|
|
710 |
</body></html>
|