git @ Cat's Eye Technologies Burro / 1551dc4
Import of Burro version 2.0 revision 2010.0607 sources. Cat's Eye Technologies 8 years ago
13 changed file(s) with 2157 addition(s) and 1536 deletion(s). Raw diff Collapse all Expand all
0 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
1 <html xmlns="http://www.w3.org/1999/xhtml" lang="en">
2 <head>
3 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
4 <title>The Burro Programming Language, version 1.0</title>
5 </head>
6 <body>
7
8 <h1>The Burro Programming Language, version 1.0</h1>
9
10 <p>October 2007, Chris Pressey, Cat's Eye Technologies.</p>
11
12 <p><em>Note: This document describes version 1.0 of the Burro language. For documentation
13 on the latest version of the language, please see <a href="burro.html">burro.html</a>.</em></p>
14
15 <h2>1. Introduction</h2>
16
17 <p><em>Burro</em> is a Brainfuck-like programming language whose programs form an
18 algebraic group under concatenation.</p>
19
20 <p>(At least, that is how I originally would have described it. But that description
21 turns out to be not entirely precise, because the technical meanings of "group" and
22 "program" come into conflict. A more precise statement would be: "Burro is
23 a semi-formal programming language, the set of whose program texts, paired with the operation
24 of concatenation, forms an algebraic group over a semantic equivalence relation."
25 But the first version is close enough for jazz, and rolls off the tongue more easily...)</p>
26
27 <p>Anyway, what does it mean? It means that, among other things, every Burro program has
28 an <em>antiprogram</em> &mdash; a series of instructions that can be appended to it
29 to annihilate its behavior. The resulting catenated program has the
30 same semantics as no program at all &mdash; a "no-op," or a zero-length program.</p>
31
32 <p>Why is this at all remarkable? Well, take the Brainfuck program fragment <code>[-]+[]</code>.
33 What could you append to it to it to make it into a "no-op" program?
34 Evidently <em>nothing</em>, because once the interpreter enters an infinite loop, it's not
35 going to care what instructions you've put after the loop. And a program that loops forever
36 isn't the same as one that does nothing at all.</p>
37
38 <p>So not all Brainfuck programs have antiprograms. Despite that, Brainfuck does embody a lot of
39 symmetry. Group theory, too, is a branch of
40 mathematics particularly suited to the study of symmetry. And as you might imagine,
41 there is a distinct relation between symmetrical programming languages and reversible
42 programming (even though it may not be immediatly clear exactly what that relationship is.)
43 These are some of the factors that encouraged me to design Burro.</p>
44
45 <h2>2. Background</h2>
46
47 <p>Before explaining Burro, a short look of group theory and of the theory of
48 computation would probably be helpful.</p>
49
50 <h3>Group Theory</h3>
51
52 <p>Recall (or go look up in an abstract algebra textbook) that a <em>group</em> is
53 a pair of a set <var>S</var> and a binary operation
54 &middot; : <var>S</var> &times; <var>S</var> &rarr; <var>S</var>
55 that obeys the following three axioms:</p>
56
57 <ul>
58
59 <li>For any three elements <var>a</var>, <var>b</var>, and <var>c</var> of
60 the set <var>S</var>, (<var>a</var> &middot; <var>b</var>) &middot; <var>c</var> =
61 <var>a</var> &middot; (<var>b</var> &middot; <var>c</var>). In other words,
62 the operation is "associative." Parentheses don't matter, and we generally leave them out.</li>
63
64 <li>There exists some element of <var>S</var>, which we call <b>e</b>, such that
65 <var>a</var> &middot; <b>e</b> = <b>e</b> &middot; <var>a</var> = <var>a</var>
66 for every element <var>a</var> of <var>S</var>. Think of
67 <b>e</b> as a "neutral" element that just doesn't contribute anything.</li>
68
69 <li>For every element <var>a</var> of <var>S</var> there is an element
70 <var>a'</var> of <var>S</var> such that <var>a</var> &middot; <var>a'</var> = <b>e</b>.
71 That is, for any element, you can find some element that "annihilates" it.</li>
72
73 </ul>
74
75 <p>There are lots of examples of groups &mdash; the integers under the operation of
76 addition, for example, where <b>e</b> is 0, and the annihilator for any integer
77 is simply its negative (because <var>x</var> + (-<var>x</var>) always equals 0.)</p>
78
79 <p>There are also lots of things you can prove are true about any group
80 (that is, about groups in general.) For instance, that <b>e</b> is unique: if
81 <var>a</var> &middot; <var>x</var> = <var>a</var> and
82 <var>a</var> &middot; <var>y</var> = <var>a</var> then
83 <var>x</var> = <var>y</var> = <b>e</b>. (This particular property will
84 become relevant very soon, so keep it in mind as you read the next section.)</p>
85
86 <p>The set on which a group is based can have any number of elements. Research
87 and literature in group theory often concentrates on finite groups, because these
88 are in some ways more interesting, and they are useful in error-correcting
89 codes and other applications. However, the set of Burro programs is countably
90 infinite, so we will be dealing with infinite groups here.</p>
91
92 <h3>Theory of Computation</h3>
93
94 <p>I don't need to call on a lot of theory of computation here except to point
95 out one fact: for any program, there are an infinite number of equivalent programs.
96 There are formal proofs of this, but they can be messy, and it's something
97 that should be obvious to most programmers. Probably the simplest example, in Brainfuck,
98 is that <code>+-</code>, <code>++--</code>, <code>+++---</code>, <code>++++----</code>,
99 etc., all have the same effect.</p>
100
101 <p>To be specific, by "program" here I mean "program text" in a
102 particular language; if we're talking about "abstract programs" in no particular
103 language, then you could well say that there is only and exactly one program that
104 does any one thing, it's just that there are an infinite number of concrete
105 representations of it.</p>
106
107 <p>This distinction becomes important with respect to treating programs
108 as elements of a group, like we're doing in Burro. Some program will
109 be the neutral element <b>e</b>. But either <em>many</em> programs will
110 be equivalent to this program &mdash; in which case <b>e</b> is not unique, contrary to
111 what group theory tells us &mdash; or we are talking about abstract programs
112 independent of any programming language, in which case our goal of defining a particular
113 language called "Burro" for this purpose seems a bit futile.</p>
114
115 <p>There are a couple of ways this could be resolved. We could foray into
116 domain theory, and try to impose a group structure on the semantics of programs
117 irrespective of the language they are in. Or we could venture into representation
118 theory, and see if the program texts can act as generators of the group elements.
119 Both of these approaches could be interesting, but I chose an approach that I
120 found to be less of a distraction, and possibly more intuitive, at the cost of
121 introducing a slight variation on the notion of a group.</p>
122
123 <h3>Group Theory, revisited</h3>
124
125 <p>To this end, let's examine the idea of a <em>group over an equivalence relation</em>.
126 All this is, really, is being specific about what constitutes "equals" in those
127 group axioms I listed earlier. In mathematics there is a well-established notion of
128 an <em>equivalence relation</em> &mdash; a relationship between elements
129 which paritions a set into
130 disjoint equivalence classes, where every element in a class is considered
131 equivalent to every other element in that same class (and inequivalent to any
132 element in any other class.)</p>
133
134 <p>We can easily define an equivalence relation on programs (that is,
135 program texts.) We simply say that two programs are
136 equivalent if they have the same semantics: they map the same inputs to the
137 same outputs, they compute the same function, they "do the same thing" as
138 far as an external observer can tell, assuming he or she is unconcerned with
139 performance issues. As you can imagine, this relation will be very useful for
140 our purpose.</p>
141
142 <p>We can also reformulate the group axioms using an equivalence relation.
143 At the very least, I can't see why it should be invalid to do so. (Indeed, this seems to
144 be the general idea behind using "quotients" in abstract algebra. In our case, we
145 have a set of program texts and a "semantic" equivalence relation "are equivalent
146 programs", and the quotient set is the set of all computable functions
147 regardless of their concrete representation.)</p>
148
149 <p>So let's go ahead and take that liberty. The resulting algebraic structure
150 should be quite similar to what we had before,
151 but with the equivalence classes becoming the real "members" of the group,
152 and with each class containing many individual elements which are treated
153 interchangably with respect to the group axioms.</p>
154
155 <p>I'll summarize the modified definition here. A <em>group over an equivalence relation</em>
156 is a triple &lang;<var>S</var>,&middot;,&equiv;&rang; where:</p>
157 <ul>
158 <li><var>S</var> is a set</li>
159 <li>&middot; : <var>S</var> &times; <var>S</var> &rarr; <var>S</var> is a binary operation over <var>S</var></li>
160 <li>&equiv; is a reflexive, transitive, and symmetrical binary relation over <var>S</var></li>
161 </ul>
162 <p>where the following axioms are also satisfied:</p>
163 <ul>
164 <li>&forall; <var>a</var>, <var>b</var>, <var>c</var> &isin; <var>S</var>: (<var>a</var> &middot; <var>b</var>) &middot; <var>c</var> &equiv;
165 <var>a</var> &middot; (<var>b</var> &middot; <var>c</var>)</li>
166 <li>&exist; <b>e</b> &isin; <var>S</var>: &forall; <var>a</var> &isin; <var>S</var>: <var>a</var> &middot; <b>e</b> &equiv; <b>e</b> &middot; <var>a</var> &equiv; <var>a</var></li>
167 <li>&forall; <var>a</var> &isin; <var>S</var>: &exist; <var>a'</var> &isin; <var>S</var>: <var>a</var> &middot; <var>a'</var> &equiv; <b>e</b></li>
168 </ul>
169
170 <p>Every theorem that applies to groups should be easy to modify to be applicable
171 to a group over an equivalence relation: just replace = with &equiv;. So what
172 we have, for example, is that while any given <b>e</b> itself might not be unique, the
173 equivalence class <b>E</b> &sube; <var>S</var> that contains it is:
174 <b>E</b> is the only equivalence class that contains
175 elements like <b>e</b> and, for the purposes of the group, all of these elements are
176 interchangeable.</p>
177
178 <h2>3. Syntax and Semantics</h2>
179
180 <h3>Five-instruction Foundation</h3>
181
182 <p>Burro is intended to be Brainfuck-like, so we could start by examining which
183 parts of Brainfuck are already suitable for Burro and which parts will have to
184 be modified or rejected.</p>
185
186 <p>First, note that Brainfuck is traditionally very lenient about what
187 constitutes a "no-op" instruction. Just about any symbol that isn't explicitly
188 mentioned in the instruction set is treated as a no-op (and this behaviour turns
189 out to be useful for inserting comments in programs.) In Burro, however, we'll
190 strive for better clarity by defining an explicit "no-op" instruction. For
191 consistency with the group theory side of things, we'll call it <code>e</code>.
192 (Of course, we won't forget that <code>e</code> lives in an equivalence class
193 with other things like <code>+-</code> and the zero-length program, and all
194 of these things are semantically interchangeable. But <code>e</code> gives
195 us a nice, single-symbol, canonical program form when we want to talk about it.)</p>
196
197 <p>Now let's consider the basic Brainfuck instructions <code>+</code>, <code>-</code>,
198 <code>&lt;</code>, and <code>&gt;</code>. They have a nice, symmetrical
199 organization that is ideally suited to group structure, so we will adopt them
200 in our putative Burro design.</p>
201
202 <p>On the other hand, the instructions <code>.</code> and <code>,</code> will require
203 devising some kind of annihilator for interactive input and output. This seems
204 difficult at least, and not really necessary if we're willing to forego writing
205 "Hunt the Wumpus" in Burro, so we'll leave them out for now. The only input for a
206 Burro program is, instead, the initial state of the tape, and the only output is the
207 final state.</p>
208
209 <p>In addition, <code>[</code> and <code>]</code> will cause problems, because
210 as we saw in the introduction, <code>[-]+[]</code> is an infinite loop, and it's
211 not clear what we could use to annihilate it. We'll defer this question for later
212 and for the meantime leave these instructions out, too.</p>
213
214 <p>What we're left in our "Burro-in-progress" is essentially a very weak subset of
215 Brainfuck, with only the five instructions <code>+-&gt;&lt;e</code>. But this is
216 a starting point that we can use to see if we're on the right track. Do the
217 programs formed from strings of these instructions form a group under concatenation
218 over the semantic equivalence relation? i.e., Does every Burro program so far
219 have an inverse?</p>
220
221 <p>Let's see. For every <i>single-instruction</i> Burro
222 program, we can evidently find another Burro instruction that, when appended to
223 it, "cancels it out" and makes a program with the same semantics as <code>e</code>:</p>
224
225 <table border="1" cellpadding="5">
226 <tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
227 <tr><td align="center"><code>+</code></td><td align="center"><code>-</code></td>
228 <td align="center"><code>+-</code></td><td align="center"><code>e</code></td></tr>
229 <tr><td align="center"><code>-</code></td><td align="center"><code>+</code></td>
230 <td align="center"><code>-+</code></td><td align="center"><code>e</code></td></tr>
231 <tr><td align="center"><code>&gt;</code></td><td align="center"><code>&lt;</code></td>
232 <td align="center"><code>&gt;&lt;</code></td><td align="center"><code>e</code></td></tr>
233 <tr><td align="center"><code>&lt;</code></td><td align="center"><code>&gt;</code></td>
234 <td align="center"><code>&lt;&gt;</code></td><td align="center"><code>e</code></td></tr>
235 <tr><td align="center"><code>e</code></td><td align="center"><code>e</code></td>
236 <td align="center"><code>ee</code></td><td align="center"><code>e</code></td></tr>
237 </table>
238
239 <p>Note that we once again should be more explicit about our requirements than
240 Brainfuck. We need to have a tape which is infinite in both directions, or else
241 <code>&lt;</code> wouldn't always be the inverse of <code>&gt;</code> (because sometimes
242 it'd fail in some way like falling off the edge of the tape.) And, so that we don't have
243 to worry about overflow and all that rot,
244 let's say cells can take on any unbounded negative or positive integer value, too.</p>
245
246 <p>But does this hold for <em>any</em> Burro program? We can use structural
247 induction to determine this.
248 Can we find inverses for every Burro program, concatenated with a given
249 instruction? (In the following table,
250 <i>b</i> indicates any Burro program, and <i>b'</i> its inverse.
251 Also note that <i>bb'</i> is, by definition, <code>e</code>.)</p>
252
253 <table border="1" cellpadding="5">
254 <tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
255 <tr><td align="center"><code><i>b</i>+</code></td><td align="center"><code>-<i>b'</i></code></td>
256 <td align="center"><code><i>b</i>+-<i>b'</i></code> &equiv; <code><i>b</i>e<i>b'</i></code> &equiv; <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
257 <tr><td align="center"><code><i>b</i>-</code></td><td align="center"><code>+<i>b'</i></code></td>
258 <td align="center"><code><i>b</i>-+<i>b'</i></code> &equiv; <code><i>b</i>e<i>b'</i></code> &equiv; <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
259 <tr><td align="center"><code><i>b</i>&gt;</code></td><td align="center"><code>&lt;<i>b'</i></code></td>
260 <td align="center"><code><i>b</i>&gt;&lt;<i>b'</i></code> &equiv; <code><i>b</i>e<i>b'</i></code> &equiv; <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
261 <tr><td align="center"><code><i>b</i>&lt;</code></td><td align="center"><code>&gt;<i>b'</i></code></td>
262 <td align="center"><code><i>b</i>&lt;&gt;<i>b'</i></code> &equiv; <code><i>b</i>e<i>b'</i></code> &equiv; <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
263 <tr><td align="center"><code><i>b</i>e</code> &equiv; <code><i>b</i></code></td><td align="center"><code>e<i>b'</i></code> &equiv; <code><i>b'</i>e</code> &equiv; <code><i>b'</i></code></td>
264 <td align="center"><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
265 </table>
266
267 <p>Looks good. However, this isn't an abelian group, and concatenation is definately not
268 commutative. So, to be complete, we need a table going in the other direction, too: concatenation of a
269 given instruction with any Burro program.</p>
270
271 <table border="1" cellpadding="5">
272 <tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
273 <tr><td align="center"><code>+<i>b</i></code></td><td align="center"><code><i>b'</i>-</code></td>
274 <td align="center"><code>+<i>bb'</i>-</code> &equiv; <code>+e-</code> &equiv; <code>+-</code></td><td align="center"><code>e</code></td></tr>
275 <tr><td align="center"><code>-<i>b</i></code></td><td align="center"><code><i>b'</i>+</code></td>
276 <td align="center"><code>-<i>bb'</i>+</code> &equiv; <code>-e+</code> &equiv; <code>-+</code></td><td align="center"><code>e</code></td></tr>
277 <tr><td align="center"><code>&gt;<i>b</i></code></td><td align="center"><code><i>b'</i>&lt;</code></td>
278 <td align="center"><code>&gt;<i>bb'</i>&lt;</code> &equiv; <code>&gt;e&lt;</code> &equiv; <code>&gt;&lt;</code></td><td align="center"><code>e</code></td></tr>
279 <tr><td align="center"><code>&lt;<i>b</i></code></td><td align="center"><code><i>b'</i>&gt;</code></td>
280 <td align="center"><code>&lt;<i>bb'</i>&gt;</code> &equiv; <code>&lt;e&gt;</code> &equiv; <code>&lt;&gt;</code></td><td align="center"><code>e</code></td></tr>
281 <tr><td align="center"><code>e<i>b</i></code> &equiv; <code><i>b</i></code></td><td align="center"><code><i>b'</i>e</code> &equiv; <code>e<i>b'</i></code> &equiv; <code><i>b'</i></code></td>
282 <td align="center"><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
283 </table>
284
285 <p>So far, so good, I'd say. Now we can address to the problem of how to
286 restrengthen the language so that it remains as powerful as Brainfuck.</p>
287
288 <h3>Loops</h3>
289
290 <p>Obviously, in order for Burro to be as capable as Brainfuck,
291 we would like to see some kind of looping mechanism in it. But, as we've
292 seen, Brainfuck's is insufficient for our purposes, because it allows for
293 the construction of infinite loops that we can't invert by concatenation.</p>
294
295 <p>We could insist that all loops be finite, but that would make
296 Burro less powerful than Brainfuck &mdash; it would only be capable of expressing
297 the primitive recursive functions. The real challenge is in having Burro be Turing-complete,
298 like Brainfuck.</p>
299
300 <p>This situation looks dire, but there turns out to be a way. What we
301 do is borrow the trick used in languages like L00P and Version (and probably
302 many others.) We put a single, implicit loop around the whole program.
303 (There is a classic formal proof that this is sufficient &mdash; the interested
304 reader is referred to the paper "Kleene algebra with tests"<sup><a href="#1">1</a></sup>,
305 which gives a brief history, references, and its own proof.)</p>
306
307 <p>This single implicit loop will be conditional on a special flag, which
308 we'll call the "halt flag", and we'll stipulate is initially set.
309 If this flag is still set when the end of the program is reached, the program halts.
310 But if it is unset when the end of the program is reached, the flag is reset
311 and the program repeats from the beginning. (Note that although the halt flag
312 is reset, all other program state (i.e. the tape) is left alone.)</p>
313
314 <p>To manipulate this flag, we introduce a new instruction:</p>
315
316 <table border="1" cellpadding="5">
317 <tr><th>Instruction</th><th>Semantics</th></tr>
318 <tr><td align="center"><code>!</code></td><td>Toggle halt flag</td></tr>
319 </table>
320
321 <p>Then we check that adding this instruction to Burro's instruction set
322 doesn't change the fact that Burro programs form a group:</p>
323
324 <table border="1" cellpadding="5">
325 <tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
326 <tr><td align="center"><code>!</code></td><td align="center"><code>!</code></td>
327 <td align="center"><code>!!</code></td><td align="center"><code>e</code></td></tr>
328 <tr><td align="center"><code>!<i>b</i></code></td><td align="center"><code><i>b'</i>!</code></td>
329 <td align="center"><code>!<i>bb'</i>!</code> &equiv; <code>!e!</code> &equiv; <code>!!</code></td><td align="center"><code>e</code></td></tr>
330 <tr><td align="center"><code><i>b</i>!</code></td><td align="center"><code>!<i>b'</i></code></td>
331 <td align="center"><code><i>b</i>!!<i>b'</i></code> &equiv; <code><i>beb'</i></code> &equiv; <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
332 </table>
333
334 <p>Seems so. Now we can write Burro programs that halt, and Burro programs that loop
335 forever. What we need next is for the program to be able to decide this behaviour
336 for itself.</p>
337
338 <h3>Conditionals</h3>
339
340 <p>OK, this is the ugly part.</p>
341
342 <p>Let's add a simple control structure to Burro. Since we already have repetition, this
343 will only be for conditional execution. To avoid confusion with Brainfuck, we'll avoid <code>[]</code>
344 entirely; instead, we'll use <code>()</code>
345 to indicate "execute the enclosed code (once) if and only if the current cell is non-zero".</p>
346
347 <p>Actually, let's make it a bit fancier, and allow an "else" clause to be inserted in it,
348 like so: <code>(/)</code> where the code before the <code>/</code> is executed iff the cell
349 is non-zero, and the code after the <code>/</code> is executed iff it is zero.</p>
350
351 <p>(The reasons for this design choice are subtle. They come down to the fact that
352 in order to find an inverse of a conditional, we need to invert the sense of the test.
353 In a higher-level language, we could use a Boolean NOT operation for this. However, in
354 Brainfuck, writing a NOT requires a loop, and thus a conditional. Then we're stuck
355 with deciding how to invert the sense of <em>that</em> conditional, and so forth. By
356 providing NOT-like behaviour as a built-in courtesy of <code>/</code>, we dodge the
357 problem entirely. If you like, you can think of it as meeting the aesthetic demands of
358 a symmetrical language: the conditional structures are symmetrical too.)</p>
359
360 <p>A significant difference here with Brainfuck is that, while Brainfuck is a bit
361 lacksidaisical about matching up <code>[</code>'s with <code>]</code>'s, we explicitly
362 <em>disallow</em> parentheses that do not nest correctly in Burro. A Burro program with mismatched
363 parentheses is an ill-formed Burro program, and thus not really a Burro program at all.
364 We turn up our nose at it; we aren't even interested in whether we can find an
365 inverse of it, because we don't acknowledge it. This applies to the placement of
366 <code>/</code> outside of parentheses, or the absence of <code>/</code> in parentheses,
367 as well.</p>
368
369 <p>(The reasons for this design choice are also somewhat subtle. I originally wanted
370 to deal with this by saying that <code>(</code>, <code>/</code>, and <code>)</code>
371 could come in any order, even a nonsensical one, and still make a valid Burro program,
372 only with the semantics of "no-op" or "loop forever" or something equally representative of
373 "broken." You see this quite often in toy formal languages, and the resulting lack of
374 syntax would seem to allow the set of Burro instructions to be a "free generator" of
375 the group of Burro programs, which sounds like it might have very nice
376 abstract-algebraical properties.
377 The problem is that it potentially interferes with the whole "finding an
378 antiprogram" thing. If a Burro program with mismatched parentheses has the
379 semantics of "no-op", then every Burro program has a trivial annihilator: just
380 tack on an unmatching parenthesis. Similarly, if malformed programs are
381 considered to loop forever, how do you invert them? So, for these reasons,
382 Burro has some small amount of syntax &mdash; a bit more than Brainfuck is usually
383 considered to have, but not much.)</p>
384
385 <p>Now, it turns out we will have to do a fair bit of work on <code>()</code> in order
386 to make it so that we can always find a bit of code that is the inverse of some other
387 bit of code that includes <code>()</code>.</p>
388
389 <p>We can't just make it a "plain old if", because by the time we've finished executing an "if",
390 we don't know which branch was executed &mdash; so we have no idea what the "right"
391 inverse of it would be. For example,</p>
392
393 <ul><li><code>(-/e)</code></li></ul>
394
395 <p>After this has finished executing, the current cell could contain 0 - but is that because it
396 was already 0 before the <code>(</code> was encountered, and nothing happened to it
397 inside the "if"... or is it because it was 1 before
398 the <code>(</code> was encountered, and decremented to 0 by the <code>-</code>
399 instruction inside the "if"?
400 It could be either, and we don't know &mdash; so we can't find an inverse.</p>
401
402 <p>We remedy this in a somewhat disappointingly uninteresting way: we make a copy of
403 the value being tested and squirrel it away for future reference, so that pending code
404 can look at it and tell what decision was made, and in so doing, act appropriately to
405 invert it.</p>
406
407 <p>This information that we squirrel away is, I would say, a kind of <em>continuation</em>.
408 It's not a full-bodied continuation, as the term continuation is often used, in the
409 sense of "function representing the entire remainder of the computation."
410 But, it's a bit of context that is retained during execution that is intended to affect
411 some future control flow decision &mdash; and that's the basic purpose of a continuation.
412 So, I will call it a continuation, although it is perhaps a diminished sort of continuation.
413 (In this sense, the machine stack where arguments and
414 return addresses are stored in a language like C is also a kind of continuation.)</p>
415
416 <p>These continuations that we maintain, these pieces of information that tell us how
417 to undo things in the future, do need to have an orderly relationship with each other.
418 Specifically, we need to remember to undo the more recent conditionals first. So, we
419 retain the continuations in a FIFO discipline, like a stack. Whenever a <code>(</code> is
420 executed, we "push" a continuation into storage, and when we need to invert the effect
421 of a previous conditional, we "pop" a continuation from storage.</p>
422
423 <p>To actually accomplish this latter action we need to define the control structure
424 for undoing conditional tests. We introduce the construct
425 <code>{\}</code>, which works just like <code>(/)</code>, except that the value that it tests
426 doesn't come from the tape &mdash; instead, it comes from the continuation. We establish similar
427 syntactic rules about matching every <code>{</code> with a <code>}</code> and an
428 intervening <code>\</code>, in addition to a rule that says every <code>{\}</code>
429 must be preceded by a <code>(/)</code>.</p>
430
431 <p>With this, we're very close to having an inverse for conditionals. Consider:</p>
432
433 <ul><li><code>(-/e){+\e}</code></li></ul>
434
435 <p>If the current cell contains 0 after <code>(-/e)</code>, the continuation will contain either
436 a 1 or a 0 (the original contents of the cell.) If the continuation contains a 0, the "else" part of
437 <code>{+\e}</code> will be executed &mdash; i.e. nothing will happen. On the other hand, if the
438 continuation contains a 1, the "then" part of <code>{+\e}</code> will be executed.
439 Either way, the tape is correctly restored to its original (pre-<code>(-/e)</code>) state.</p>
440
441 <p>There are still a few details to clean up, though.
442 Specifically, we need to address nesting. What if we're given</p>
443
444 <ul><li><code>(&gt;(&lt;+/e)/e)</code></li></ul>
445
446 <p>How do we form an inverse of this? How would the following work?</p>
447
448 <ul><li><code>(&gt;(&lt;+/e)/e){{-&gt;\e}&lt;\e}</code></li></ul>
449
450 <p>The problem with this, if we collect continuations using only a naive stack arrangement,
451 is that we don't remember how many times a <code>(</code> was encountered before a
452 matching <code>)</code>. The retention of continuations is still FIFO, but we need
453 more control over the relationships between the continuations.</p>
454
455 <p>The nested structure of the <code>(/)</code>'s suggests a nested structure
456 for collecting continuations.
457 Whenever we encounter a <code>(</code> and we "push" a continuation into storage,
458 that continuation becomes the root for a new collection of continuations
459 (those that occur <em>inside</em> the present conditional, up to the matching
460 <code>)</code>.) Since each continuation is both part of some FIFO series of
461 continuations, and has the capacity to act as the root of it's <em>own</em> FIFO series
462 of continuations, the continuations are arranged in a structure that is
463 more a binary tree than a stack.</p>
464
465 <p>This is perhaps a little complicated, so I'll summarize it in this table.
466 Since this is a fairly operational description, I'll use the term "tree node"
467 instead of continuation to help you visualize it. Keep in mind that at any
468 given time there is a "current continuation" and thus a current tree node.</p>
469
470 <table border="1" cellpadding="5">
471 <tr><th>Instruction</th><th>Semantics</th></tr>
472 <tr><td align="center"><code>(</code></td><td>
473 <ul>
474 <li>Create a new tree node with the contents of the current cell</li>
475 <li>Add that new node as a child of the current node</li>
476 <li>Make that new node the new current node</li>
477 <li>If the current cell is zero, skip one instruction past the matching <code>/</code></li>
478 </ul>
479 </td></tr>
480 <tr><td align="center"><code>/</code></td><td>
481 <ul>
482 <li>Skip to the matching <code>)</code></li>
483 </ul>
484 </td></tr>
485 <tr><td align="center"><code>)</code></td><td>
486 <ul>
487 <li>Make the parent of the current node the new current node</li>
488 </ul>
489 </td></tr>
490 <tr><td align="center"><code>{</code></td><td>
491 <ul>
492 <li>Make the most recently added child of the current node the new current node</li>
493 <li>If the value of the current node is zero, skip one instruction past the matching <code>\</code></li>
494 </ul>
495 </td></tr>
496 <tr><td align="center"><code>\</code></td><td>
497 <ul>
498 <li>Skip to the matching <code>}</code></li>
499 </ul>
500 </td></tr>
501 <tr><td align="center"><code>}</code></td><td>
502 <ul>
503 <li>Make the parent of the current node the new current node</li>
504 <li>Remove the old current node and all of its children</li>
505 </ul>
506 </td></tr>
507 </table>
508
509 <p>Now, keeping in mind that the continuation structure
510 remains constant across all Burro programs equivalent to <code>e</code>,
511 we can show that control structures have inverses:</p>
512
513 <table border="1" cellpadding="5">
514 <tr><th>Instruction</th><th>Inverse</th><th>Test result</th><th>Concatenation</th><th>Net effect</th></tr>
515 <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>
516 <td align="center">zero</td><td align="center"><code><i>acdd'c'a'</i></code> &equiv; <code><i>acc'a'</i></code> &equiv; <code><i>aa'</i></code></td><td align="center"><code>e</code></td></tr>
517 <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>
518 <td align="center">non-zero</td><td align="center"><code><i>abdd'b'a'</i></code> &equiv; <code><i>abb'a'</i></code> &equiv; <code><i>aa'</i></code></td><td align="center"><code>e</code></td></tr>
519 </table>
520
521 <p>There you have it: every Burro program has an inverse.</p>
522
523 <h2>4. Implementations</h2>
524
525 <p>There are two reference interpreters for Burro. <code>burro.c</code> is
526 written in ANSI C, and <code>burro.hs</code> is written in Haskell.
527 Both are BSD licensed.
528 Hopefully at least one of them is faithful to the execution model.</p>
529
530 <h3><code>burro.c</code></h3>
531
532 <p>The executable produced by compiling <code>burro.c</code> takes the
533 following command-line arguments:</p>
534
535 <ul><li><code>burro [-d] srcfile.bur</code></li></ul>
536
537 <p>The named file is loaded as Burro source code. All characters in this file except for
538 <code>&gt;&lt;+-(/){\}e!</code> are ignored.</p>
539
540 <p>Before starting the run, the interpreter will read a series of whitespace-separated
541 integers from standard input. These integers
542 are placed on the tape initially, starting from the head-start position, extending right.
543 All unspecified cells are considered to contain 0 initially.</p>
544
545 <p>When the program has halted, all tape cells that were "touched" &mdash; either given initially as
546 part of the input, or passed over by the tape head &mdash; are output to standard output.</p>
547
548 <p>The meanings of the flags are as follows:</p>
549
550 <ul>
551 <li>The <code>-d</code> flag causes debugging information to be sent to standard error.</li>
552 </ul>
553
554 <p>The C implementation performs no syntax-checking. It approximates the unbounded Burro tape
555 with a tape of finite size (defined by <code>TAPE_SIZE</code>, by default 64K) with
556 cells each capable of containing a C language <code>long</code>.</p>
557
558 <h3><code>burro.hs</code></h3>
559
560 <p>The Haskell version of the reference implementation is meant to be executed from
561 within an interactive Haskell environment, such as Hugs. As such, there is no
562 command-line syntax; the user simply invokes the function <code>burro</code>,
563 which has the signature <code>burro :: String -&gt; Tape -&gt; Tape</code>.
564 A convenience constructor <code>tape :: [Integer] -> Tape</code> creates a tape
565 from the given list of integers, with the head positioned over the leftmost cell.</p>
566
567 <p>The Haskell implementation performs no syntax-checking. Because Haskell supports
568 unbounded lists and arbitrary-precision integers, the Burro tape is modelled faithfully.</p>
569
570 <h2>Discussion</h2>
571
572 <p>I hadn't intended to come up with anything in particular when I started
573 designing Burro. I'm hardly a mathematician, and I didn't know anything
574 about abstract algebra except that I found it intriguing. I suppose that algebraic
575 structures have some of the same appeal as programming languages, what with
576 both dealing with primitive operators, equivalent expression forms, and so forth.</p>
577
578 <p>I was basically struck by the variety of objects that could be shown to have
579 this or that algebraic structure, and I wanted to see how well it would
580 hold up if you tried to apply these structures to programs.</p>
581
582 <p>Why groups? Well, the original design goal for Burro was actually to create a Brainfuck-like language
583 where the set of possible programs forms the most <em>restricted</em>
584 possible magma (i.e. the one with the most additional axioms) under concatenation. It can
585 readily been seen that the set of Brainfuck programs forms a semigroup,
586 even a monoid, under concatenation (left as an exercise for the interested
587 reader.) At the other extreme, if the set of programs forms an abelian group under
588 concatenation, the language probably isn't going to be very Brainfuck-like
589 (since insisting that concatenation be commutative is tantamount to saying
590 that the order of instructions in a program doesn't matter.)
591 This leaves a group as the reasonable target to aim for, so that's what I
592 aimed for.</p>
593
594 <p>But the end result turns out to be related to <em>reversible computing</em>.
595 This shouldn't have been a surprise, since groups are one of the simplest
596 foundations for modelling symmetry; it should have been obvious to me that trying to
597 make programs conform to them, would make them (semantically) symmetrical, and
598 thus reversible. But, it wasn't.</p>
599
600 <p>We may ask: in what sense is Burro reversible? And we may compare it
601 to other esolangs in an attempt to understand.</p>
602
603 <p>Well, it's not reversible in the sense that
604 <a href="http://esolangs.org/wiki/Befreak">Befreak</a> is reversible &mdash;
605 you can't pause it at any point, change the direction of execution, and watch it
606 "go backwards". Specifically, you can't "undo" a loop in Burro by executing
607 20 iterations, then turning around and "un-executing" those 20 iterations; instead,
608 you "undo" the loop by neutralizing the toggling of the halt flag. With this approach,
609 inversion is instead <em>like the loop never existed in the first place</em>.</p>
610
611 <p>If one did want to make a Brainfuck-like language which was reversible more in
612 the sense that Befreak is reversible, one approach might be to add rules like
613 "<code>+</code> acts like <code>-</code> if the program counter is incoming from
614 the right". But, I haven't pondered on this approach much at all.</p>
615
616 <p>Conversely, the concatenation concept doesn't have a clear
617 correspondence in a two-dimensional language like Befreak &mdash; how do you put two programs
618 next to each other? Side-by-side, top-to-bottom? You would probably need multiple
619 operators, which would definately complicate things.</p>
620
621 <p>It's also not reversible in the same way that
622 <a href="http://esolangs.org/wiki/Kayak">Kayak</a> is reversible &mdash;
623 Burro programs need not be palindromes, for instance. In fact, I specifically made
624 the "then" and "else" components of both <code>(/)</code> and <code>{\}</code>
625 occur in the same order, so as to break the reflectional symmetry somewhat, and
626 add some translational similarity.</p>
627
628 <p>Conversely, Kayak doesn't cotton to concatenation too well either.
629 In order to preserve the palindrome nature, concatenation would have to
630 occur both at the beginning and the end simultaneously.
631 I haven't given this idea much thought, and I'm not sure where it'd get you.</p>
632
633 <p>Lastly, we could go outside the world of esolangs and use the
634 definition of reversible computing given by Mike Frank<sup><a href="#2">2</a></sup>:</p>
635
636 <blockquote><p>When we say reversible computing, we mean performing computation
637 in such a way that any previous state of the computation can always be reconstructed
638 given a description of the current state.</p></blockquote>
639
640 <p>Burro appears to qualify by this definition &mdash; <em>almost</em>. The requirement
641 that we can reconstruct <em>any</em> previous state is a bit heavy. We can definately
642 reconstruct states up to the start of the last loop iteration, if we want to, due to the mechanism
643 (continuations) that we've defined to remember what the program state was before any given
644 conditional.</p>
645
646 <p>But what about <em>before</em> the last loop iteration? Each time we reach the end
647 of the program text with halt flag unset, we repeat execution from the beginning, and
648 when this happens, there might still be one or more continuations in storage that were the
649 result of executing <code>(/)</code>'s that did not have
650 matching <code>{\}</code>'s.</p>
651
652 <p>We didn't say what happens to these "leftover" continuations. In fact, computationally
653 speaking, it doesn't matter: since syntactically no
654 <code>{\}</code> can precede any <code>(/)</code>, those leftover continuations
655 couldn't actually have any affect during the next iteration. Any <code>{\}</code> that
656 might consume them next time 'round must be preceded by a <code>(/)</code> which will
657 produce one for it to consume instead.</p>
658
659 <p>And indeed, discarding any continuation that remains when a Burro program loops
660 means that continuations need occupy only a bounded amount of space during execution (because there
661 is only a fixed number of conditionals in any given Burro program.) This
662 is a desirable thing in a practical implementation, and
663 both the C and Haskell reference implementations do just this.</p>
664
665 <p>But this is an implementation choice, and it would be equally valid to write an interpreter
666 which retains all these leftover continuations. And such an interpreter would qualify as a
667 reversible computer under Mike Frank's definition, since these continuations would allow one
668 to reconstruct the entire computation history of the program.</p>
669
670 <p>On this last point, it's interesting to note the similarity between Burro's continuations
671 and Kayak's bit bucket. Although Burro continuations record the value tested, they really
672 don't <em>need</em> to; they <em>could</em> just
673 contain bits indicating whether the tests were successes or failures. Both emptying
674 the bit bucket, and discarding continuations, results in a destruction of information that
675 prevents reversibility (and thermodynamically "generates heat") but allows for a limit on the amount of
676 storage required.</p>
677
678 <h2>History</h2>
679
680 <p>I began formulating Burro in the summer of 2005.
681 The basic design of Burro was finished by winter of 2005, as was the C implementation.
682 But its release was delayed for several reasons. Mainly, I was busy with other (ostensibly more
683 important) things, like schoolwork. However, I also had the nagging feeling that certain parts of
684 the language were not quite described correctly. These doubts led me to introduce the
685 concept of a group over an equivalence relation, and to decide that Burro needed
686 real syntax rules (lest inverting a Burro program was "too easy.") So it wasn't until spring of 2007
687 that I had a general description that I was satisfied with.
688 I also wanted a better reference implementation, in something a bit more abstract and
689 rigorous than C. So I wrote the Haskell version over the summer of 2007.</p>
690
691 <p>In addition, part of me wanted to write a publishable paper on Burro.
692 After all, group theory and reversible computing are valid and relatively mainstream
693 research topics, so why not? But in the end, considering doing this was really a
694 waste of my time. Densening my writing style to conform to acceptable academic
695 standards of impermeability, and puffing up my "discovery" to acceptable academic
696 standards of self-importance, really didn't appeal to me. There's no sense pretending,
697 in high-falutin' language, that Burro represents some profound advance in human
698 knowledge. It's just something neat that I built! And in the end it seemed
699 just as valuable, if not moreso, to try to turn esolangers on to group theory than
700 to turn academics on to Brainfuck...</p>
701
702 <p>Happy annihilating!</p>
703
704 <p>-Chris Pressey
705 <br/>Cat's Eye Technologies
706 <br/>October 26, 2007
707 <br/>Windsor, Ontario, Canada</p>
708
709 <h2>Footnotes</h2>
710
711 <ul>
712 <li><a name="1"><sup>1</sup>Dexter Kozen.</a> <a href="http://www.cs.cornell.edu/~kozen/papers/ckat.ps">Kleene algebra with tests</a>. <i>Transactions on Programming Languages and
713 Systems</i>, 19(3):427-443, May 1997.</li>
714 <li><a name="2"><sup>2</sup>Michael Frank.</a> 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></li>
715
716 </ul>
717
718 </body></html>
0 <html><head><title>The Burro programming language</title></head>
0 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
1 <html xmlns="http://www.w3.org/1999/xhtml" lang="en">
2 <head>
3 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
4 <title>The Burro Programming Language, v2.0</title>
5 <link rel="stylesheet" type="text/css" href="markdown-lhs.css" />
6 </head>
17 <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> &mdash; 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 &mdash; 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 &middot; : <var>S</var> &times; <var>S</var> &rarr; <var>S</var>
47 that obeys the following three axioms:</p>
8 <h1>The Burro Programming Language</h1>
9
10 <p>Version 2.0
11 June 2010, Chris Pressey, Cat's Eye Technologies</p>
12
13 <h2>Introduction</h2>
14
15 <p>Burro is a programming language whose programs form an algebraic group under
16 the operation of concatenation and over the equivalence relation of "computes
17 the same function." This means that, for every Burro program, we can
18 construct a corresponding antiprogram that, when appended onto the first
19 program, results in a "no-op" program (a program with no effect &mdash; the
20 identity function.)</p>
21
22 <p>(In fact, for every set of Burro programs that compute the same function,
23 there is a corresponding set of antiprograms, any of which can "cancel out"
24 any program in the first set. From our proof that Burro programs form a
25 group, we obtain a constructive algorithm which, for any given program, will
26 derive only one corresponding antiprogram, a kind of syntactic inverse.)</p>
27
28 <p>This is a kind of reversible computing, but Burro differs from most reversible
29 languages in that it is not the execution trace that is being "undone", but
30 the program itself that is being annihilated.</p>
31
32 <p>This document describes version 2.0 of the Burro language, a reformulation
33 which addresses several issues with Burro 1.0. An update to the language was
34 desired by the author after it was pointed out by Alex Smith that the set of
35 Burro version 1.0 programs do not, in fact, form a proper group (the inverse
36 of (/) is {}, but no inverse of {} is defined; also, the implementations
37 (at least) did not support moving the tape head left past the "start" of the
38 tape, so &lt;> was not a well-defined program.)</p>
39
40 <p>Additionally in this document, we construct a Burro 2.0 program equivalent to
41 a certain Turing machine. While this Turing machine is not universal, the
42 translation method we use demonstrates how it would be possible to map an
43 arbitrary Turing machine to a Burro program, hopefully making uncontroversial
44 the idea that Burro qualifies as universal.</p>
45
46 <p>For further background information on the Burro project, you may also wish
47 to read the <a href="burro-1.0.html">Burro 1.0 article</a>, with the understanding that
48 the language description given there is obsolete.</p>
49
50 <h2>Changes from Burro 1.0</h2>
51
52 <p>The {} construct does not appear in Burro 2.0. Instead, the (/) construct
53 serves as its own inverse. The tree-like structure of decision continuations
54 is not present in Burro 2.0 either. Instead, decision information is kept on
55 a second tape, called the "stack tape".</p>
56
57 <p>Henceforth in this document, the term Burro refers to Burro 2.0.</p>
58
59 <h2>About this Document</h2>
60
61 <p>This document is a reference implementation of Burro in literate Haskell,
62 using Markdown syntax for the textual prose portions (although the version
63 you are reading may have been converted to another format, such as HTML,
64 for presentation.) As such, this document serves as an "executable
65 semantics", both defining the language and providing a ready tool.</p>
66
67 <pre><code> module Main where
68 import System
69 </code></pre>
70
71 <h2>Inductive Definition of a Burro Program</h2>
72
73 <p>The symbol e is a Burro program. <br />
74 The symbol ! is a Burro program. <br />
75 The symbol + is a Burro program. <br />
76 The symbol - is a Burro program. <br />
77 The symbol &lt; is a Burro program. <br />
78 The symbol > is a Burro program. <br />
79 If a and b are Burro programs, then (a/b) is a Burro program. <br />
80 If a and b are Burro programs, then ab is a Burro program. <br />
81 Nothing else is a Burro program. </p>
82
83 <pre><code> data Burro = Null
84 | ToggleHalt
85 | Inc
86 | Dec
87 | GoLeft
88 | GoRight
89 | Test Burro Burro
90 | Seq Burro Burro
91 deriving (Read, Eq)
92 </code></pre>
93
94 <h2>Representation of Burro Programs</h2>
95
96 <p>For a concrete representation, the symbols in the inductive definition
97 given above can be taken to be a subset of a character set; for the
98 purposes of this semantics, we will use the ASCII character set. Parsing
99 a given string of symbols into a Burro program is straightforward; all
100 symbols which are not Burro symbols are simply ignored.</p>
101
102 <pre><code> instance Show Burro where
103 show Null = "e"
104 show ToggleHalt = "!"
105 show Inc = "+"
106 show Dec = "-"
107 show GoLeft = "&lt;"
108 show GoRight = "&gt;"
109 show (Test a b) = "(" ++ (show a) ++ "/" ++ (show b) ++ ")"
110 show (Seq a b) = (show a) ++ (show b)
111
112 parse string =
113 let
114 (rest, acc) = parseProgram string Null
115 in
116 trim acc
117
118 parseProgram [] acc =
119 ([], acc)
120 parseProgram ('e':rest) acc =
121 parseProgram rest (Seq acc Null)
122 parseProgram ('+':rest) acc =
123 parseProgram rest (Seq acc Inc)
124 parseProgram ('-':rest) acc =
125 parseProgram rest (Seq acc Dec)
126 parseProgram ('&lt;':rest) acc =
127 parseProgram rest (Seq acc GoLeft)
128 parseProgram ('&gt;':rest) acc =
129 parseProgram rest (Seq acc GoRight)
130 parseProgram ('!':rest) acc =
131 parseProgram rest (Seq acc ToggleHalt)
132 parseProgram ('(':rest) acc =
133 let
134 (rest', thenprog) = parseProgram rest Null
135 (rest'', elseprog) = parseProgram rest' Null
136 test = Test thenprog elseprog
137 in
138 parseProgram rest'' (Seq acc test)
139 parseProgram ('/':rest) acc =
140 (rest, acc)
141 parseProgram (')':rest) acc =
142 (rest, acc)
143 parseProgram (_:rest) acc =
144 parseProgram rest acc
145
146 trim (Seq Null a) = trim a
147 trim (Seq a Null) = trim a
148 trim (Seq a b) = Seq (trim a) (trim b)
149 trim (Test a b) = Test (trim a) (trim b)
150 trim x = x
151 </code></pre>
152
153 <h2>Group Properties of Burro Programs</h2>
154
155 <p>We assert these first, and when we describe the program semantics we will
156 show that the semantics do not violate them.</p>
157
158 <p>The inverse of e is e: ee = e <br />
159 The inverse of ! is !: !! = e <br />
160 The inverse of + is -: +- = e <br />
161 The inverse of - is +: -+ = e <br />
162 The inverse of &lt; is >: &lt;> = e <br />
163 The inverse of > is &lt;: >&lt; = e <br />
164 If aa' = e and bb' = e, (a/b)(b'/a') = e. <br />
165 If aa' = e and bb' = e, abb'a' = e. </p>
166
167 <pre><code> inverse Null = Null
168 inverse ToggleHalt = ToggleHalt
169 inverse Inc = Dec
170 inverse Dec = Inc
171 inverse GoLeft = GoRight
172 inverse GoRight = GoLeft
173 inverse (Test a b) = Test (inverse b) (inverse a)
174 inverse (Seq a b) = Seq (inverse b) (inverse a)
175 </code></pre>
176
177 <p>For every Burro program x, annihilationOf x is always equivalent
178 computationally to e.</p>
179
180 <pre><code> annihilationOf x = Seq x (inverse x)
181 </code></pre>
182
183 <h2>State Model for Burro Programs</h2>
184
185 <p>Central to the state of a Burro program is an object called a tape.
186 A tape consists of a sequence of cells in a one-dimensional array,
187 unbounded in both directions. Each cell contains an integer of unbounded
188 extent, both positive and negative. The initial value of each cell is
189 zero. One of the cells of the tape is distinguished as the "current cell";
190 this is the cell that we think of as having the "tape head" hovering over it
191 at the moment.</p>
192
193 <p>In this semantics, we represent a tape as two lists, which we treat as
194 stacks. The first list contains the cell under the tape head, and
195 everything to the left of the tape head (in the reverse order from how it
196 appears on the tape.) The second list contains everything to the right of
197 the tape head, in the same order as it appears on the tape.</p>
198
199 <pre><code> data Tape = Tape [Integer] [Integer]
200 deriving (Read)
201
202 instance Show Tape where
203 show t@(Tape l r) =
204 let
205 (Tape l' r') = strip t
206 in
207 show (reverse l') ++ "&lt;" ++ (show r')
208 </code></pre>
209
210 <p>When comparing two tapes for equality, we must disregard any zero cells
211 farther to the left/right than the outermost non-zero cells. Specifically,
212 we strip leading/trailing zeroes from tapes before comparison. We don't
213 strip out a zero that a tape head is currently over, however.</p>
214
215 <p>Also, the current cell must be the same for both tapes (that is, tape heads
216 must be in the same location) for two tapes to be considered equal.</p>
217
218 <pre><code> stripzeroes list = (reverse (sz (reverse list)))
219 where sz [] = []
220 sz (0:rest) = sz rest
221 sz x = x
222
223 ensurecell [] = [0]
224 ensurecell x = x
225
226 strip (Tape l r) = Tape (ensurecell (stripzeroes l)) (stripzeroes r)
227
228 tapeeq :: Tape -&gt; Tape -&gt; Bool
229 tapeeq t1 t2 =
230 let
231 (Tape t1l t1r) = strip t1
232 (Tape t2l t2r) = strip t2
233 in
234 (t1l == t2l) &amp;&amp; (t1r == t2r)
235
236 instance Eq Tape where
237 t1 == t2 = tapeeq t1 t2
238 </code></pre>
239
240 <p>A convenience function for creating an inital tape is also provided.</p>
241
242 <pre><code> tape :: [Integer] -&gt; Tape
243 tape x = Tape [head x] (tail x)
244 </code></pre>
245
246 <p>We now define some operations on tapes that we will use in the semantics.
247 First, operations on tapes that alter or access the cell under the tape head.</p>
248
249 <pre><code> inc (Tape (cell:left) right) = Tape (cell + 1 : left) right
250 dec (Tape (cell:left) right) = Tape (cell - 1 : left) right
251 get (Tape (cell:left) right) = cell
252 set (Tape (_:left) right) value = Tape (value : left) right
253 </code></pre>
254
255 <p>Next, operations on tapes that move the tape head.</p>
256
257 <pre><code> left (Tape (cell:[]) right) = Tape [0] (cell:right)
258 left (Tape (cell:left) right) = Tape left (cell:right)
259 right (Tape left []) = Tape (0:left) []
260 right (Tape left (cell:right)) = Tape (cell:left) right
261 </code></pre>
262
263 <p>Finally, an operation on two tapes that swaps the current cell between
264 them.</p>
265
266 <pre><code> swap t1 t2 = (set t1 (get t2), set t2 (get t1))
267 </code></pre>
268
269 <p>A program state consists of:</p>
48270
49271 <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> &middot; <var>b</var>) &middot; <var>c</var> =
53 <var>a</var> &middot; (<var>b</var> &middot; <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> &middot; <b>e</b> = <b>e</b> &middot; <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> &middot; <var>a'</var> = <b>e</b>.
63 That is, for any element, you can find some element that "annihilates" it.</li>
64
272 <li>A "data tape";</li>
273 <li>A "stack tape"; and</li>
274 <li>A flag called the "halt flag", which may be 0 or 1.</li>
65275 </ul>
66276
67 <p>There are lots of examples of groups &mdash; 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> &middot; <var>x</var> = <var>a</var> and
74 <var>a</var> &middot; <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 &mdash; in which case <b>e</b> is not unique, contrary to
103 what group theory tells us &mdash; 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> &mdash; 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 &lang;<var>S</var>,&middot;,&equiv;&rang; where:</p>
149 <ul>
150 <li><var>S</var> is a set</li>
151 <li>&middot; : <var>S</var> &times; <var>S</var> &rarr; <var>S</var> is a binary operation over <var>S</var></li>
152 <li>&equiv; 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>&forall; <var>a</var>, <var>b</var>, <var>c</var> &isin; <var>S</var>: (<var>a</var> &middot; <var>b</var>) &middot; <var>c</var> &equiv;
157 <var>a</var> &middot; (<var>b</var> &middot; <var>c</var>)</li>
158 <li>&exist; <b>e</b> &isin; <var>S</var>: &forall; <var>a</var> &isin; <var>S</var>: <var>a</var> &middot; <b>e</b> &equiv; <b>e</b> &middot; <var>a</var> &equiv; <var>a</var></li>
159 <li>&forall; <var>a</var> &isin; <var>S</var>: &exist; <var>a'</var> &isin; <var>S</var>: <var>a</var> &middot; <var>a'</var> &equiv; <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 &equiv;. 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> &sube; <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>&lt;</code>, and <code>&gt;</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>+-&gt;&lt;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>&gt;</code></td><td align="center"><code>&lt;</code></td>
224 <td align="center"><code>&gt;&lt;</code></td><td align="center"><code>e</code></td></tr>
225 <tr><td align="center"><code>&lt;</code></td><td align="center"><code>&gt;</code></td>
226 <td align="center"><code>&lt;&gt;</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>&lt;</code> wouldn't always be the inverse of <code>&gt;</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> &equiv; <code><i>b</i>e<i>b'</i></code> &equiv; <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> &equiv; <code><i>b</i>e<i>b'</i></code> &equiv; <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
251 <tr><td align="center"><code><i>b</i>&gt;</code></td><td align="center"><code>&lt;<i>b'</i></code></td>
252 <td align="center"><code><i>b</i>&gt;&lt;<i>b'</i></code> &equiv; <code><i>b</i>e<i>b'</i></code> &equiv; <code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
253 <tr><td align="center"><code><i>b</i>&lt;</code></td><td align="center"><code>&gt;<i>b'</i></code></td>
254 <td align="center"><code><i>b</i>&lt;&gt;<i>b'</i></code> &equiv; <code><i>b</i>e<i>b'</i></code> &equiv; <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> &equiv; <code><i>b</i></code></td><td align="center"><code>e<i>b'</i></code> &equiv; <code><i>b'</i>e</code> &equiv; <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> &equiv; <code>+e-</code> &equiv; <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> &equiv; <code>-e+</code> &equiv; <code>-+</code></td><td align="center"><code>e</code></td></tr>
269 <tr><td align="center"><code>&gt;<i>b</i></code></td><td align="center"><code><i>b'</i>&lt;</code></td>
270 <td align="center"><code>&gt;<i>bb'</i>&lt;</code> &equiv; <code>&gt;e&lt; &equiv; <code>&gt;&lt;</code></td><td align="center"><code>e</code></td></tr>
271 <tr><td align="center"><code>&lt;<i>b</i></code></td><td align="center"><code><i>b'</i>&gt;</code></td>
272 <td align="center"><code>&lt;<i>bb'</i>&gt;</code> &equiv; <code>&lt;e&gt; &equiv; <code>&lt;&gt;</code></td><td align="center"><code>e</code></td></tr>
273 <tr><td align="center"><code>e<i>b</i></code> &equiv; <code><i>b</i></code></td><td align="center"><code><i>b'</i>e</code> &equiv; <code>e<i>b'</i></code> &equiv; <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 &mdash; 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 &mdash; 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> &equiv; <code>!e!</code> &equiv; <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> &equiv; <code><i>beb'</i></code> &equiv; <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 &mdash; 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 &mdash; 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 &mdash; 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 &mdash; 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 &mdash; 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 &mdash; 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>(&gt;(&lt;+/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>(&gt;(&lt;+/e)/e){{-&gt;\e}&lt;\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> &equiv; <code><i>acc'a'</i></code> &equiv; <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> &equiv; <code><i>abb'a'</i></code> &equiv; <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>&gt;&lt;+-(/){\}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" &mdash; either given initially as
538 part of the input, or passed over by the tape head &mdash; 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 -&gt; Tape -&gt; 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 &mdash;
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 &mdash; 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 &mdash;
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 &mdash; <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>
277 <p>The 0 and 1 are represented by False and True boolean values in this
278 semantics.</p>
279
280 <pre><code> data State = State Tape Tape Bool
281 deriving (Show, Read, Eq)
282
283 newstate = State (tape [0]) (tape [0]) True
284 </code></pre>
285
286 <h2>Semantics of Burro Programs</h2>
287
288 <p>Each instruction is defined as a function from program state to program
289 state. Concatenation of instructions is defined as composition of
290 functions, like so:</p>
291
292 <p>If ab is a Burro program, and a maps state S to state S', and b maps
293 state S' to S'', then ab maps state S to state S''.</p>
294
295 <pre><code> exec (Seq a b) t = exec b (exec a t)
296 </code></pre>
297
298 <p>The e instruction is the identity function on states.</p>
299
300 <pre><code> exec Null s = s
301 </code></pre>
302
303 <p>The ! instruction toggles the halt flag. If it is 0 in the input state, it
304 is 1 in the output state, and vice versa.</p>
305
306 <pre><code> exec ToggleHalt (State dat stack halt) = (State dat stack (not halt))
307 </code></pre>
308
309 <p>The + instruction increments the current data cell, while - decrements the
310 current data cell.</p>
311
312 <pre><code> exec Inc (State dat stack halt) = (State (inc dat) stack halt)
313 exec Dec (State dat stack halt) = (State (dec dat) stack halt)
314 </code></pre>
315
316 <p>The instruction &lt; makes the cell to the left of the current data cell, the
317 new current data cell. The instruction > makes the cell to the right of the
318 current data cell, the new current data cell.</p>
319
320 <pre><code> exec GoLeft (State dat stack halt) = (State (left dat) stack halt)
321 exec GoRight (State dat stack halt) = (State (right dat) stack halt)
322 </code></pre>
323
324 <p>(a/b) is the conditional construct, which is quite special.</p>
325
326 <p>First, the current data cell is remembered for the duration of the execution
327 of this construct &mdash; let's call it x.</p>
328
329 <p>Second, the current data cell and the current stack cell are swapped.</p>
330
331 <p>Third, the current stack cell is negated.</p>
332
333 <p>Fourth, the stack cell to the right of the current stack cell is made
334 the new current stack cell.</p>
335
336 <p>Fifth, if x is positive, a is evaluated; if x is negative, b is evaluated;
337 otherwise x = 0 and neither is evaluated. Evaluation occurs in the state
338 established by the preceding four steps.</p>
339
340 <p>Sixth, the stack cell to the left of the current stack cell is made
341 the new current stack cell.</p>
342
343 <p>Seventh, the current data cell and the current stack cell are swapped again.</p>
344
345 <pre><code> exec (Test thn els) (State dat stack halt) =
346 let
347 x = get dat
348 (dat', stack') = swap dat stack
349 stack'' = right (set stack' (0 - (get stack')))
350 f = if x &gt; 0 then thn else if x &lt; 0 then els else Null
351 (State dat''' stack''' halt') = exec f (State dat' stack'' halt)
352 (dat'''', stack'''') = swap dat''' (left stack''')
353 in
354 (State dat'''' stack'''' halt')
355 </code></pre>
356
357 <p>We observe an invariant here: because only the (a/b) construct affects the
358 stack tape, and because it does so in a monotonic way &mdash; that is, both a
359 and b inside (a/b) have access only to the portion of the stack tape to the
360 right of what (a/b) has access to &mdash; the current stack cell in step seven
361 always holds the same value as the current stack cell in step two, except
362 negated.</p>
363
364 <h2>Repetition</h2>
365
366 <p>The repetition model of Burro 2.0 is identical to that of Burro 1.0.
367 The program text is executed, resulting in a final state, S. If, in
368 S, the halt flag is 1, execution terminates with state S. On the other
369 hand, if the halt flag is 0, the program text is executed once more,
370 this time on state S, and the whole procedure repeats. Initially the
371 halt flag is 1, so if ! is never executed, the program never repeats.</p>
372
373 <p>Additionally, each time the program repeats, the stack tape is cleared.</p>
374
375 <pre><code> run program state =
376 let
377 state'@(State dat' stack' halt') = exec program state
378 in
379 if
380 not halt'
381 then
382 run program (State dat' (tape [0]) True)
383 else
384 state'
385 </code></pre>
386
387 <h2>Central theorem of Burro</h2>
388
389 <p>We now have established enough definitions to give a proof of the central
390 theorem of Burro, which is:</p>
391
392 <p><em>Theorem: The set of all Burro programs forms a group over computational
393 equivalence under the operation of concatenation.</em></p>
394
395 <p>As covered in the Burro 1.0 article, a "group over an equivalence relation"
396 captures the notion of replacing the concept of equality in the group
397 axioms with the concept of equivalency. Our particular equivalence relation
398 here is that two programs are equivalent if they compute the same function.</p>
399
400 <p>In order to show that a set G is a group, it is sufficient to show the
401 following four properties hold:</p>
402
403 <ol>
404 <li><p>Closure: For all a, b in G, ab is also in G.</p>
405
406 <p>This follows from the inductive definition of Burro programs.</p></li>
407 <li><p>Associativity: For all a, b and c in G, (ab)c ≡ a(bc).</p>
408
409 <p>This follows from the definition of concatenation (sequential composition);
410 it doesn't matter if we concatenate a with b first, then concatenate that
411 with c, or if we concatenate b with c first, then concatenate a with that.
412 Either way the result is the same string (or in this case, the same Burro
413 program.)</p></li>
414 <li><p>Identity element: There exists an element e in G, such that for every
415 element a in G, ea ≡ ae ≡ a.</p>
416
417 <p>The instruction e in Burro has no effect on the program state. Therefore
418 concatenating it to any existing program, or concatenating any existing
419 program to it, results in a computationally equivalent program.</p></li>
420 <li><p>Inverse element: For each a in G, there exists an element b in G such
421 that ab ≡ ba ≡ e.</p>
422
423 <p>This is the key property. We first show that it holds for each element of
424 the inductive definition of Burro programs. We can then conclude, through
425 structural induction, that all Burro programs have this property.</p>
426
427 <ol>
428 <li><p>Since e is the identity function on states, e is trivially its own
429 inverse.</p></li>
430 <li><p>Since toggling the flag twice is the same as not changing it at all,
431 the inverse of ! is !.</p></li>
432 <li><p>By the definitions of incrementation and decrementation, and because
433 data cells cannot overflow, the inverse of + is -, and the inverse
434 of - is +.</p></li>
435 <li><p>By the definitions of left and right, and because the data tape is
436 unbounded (never reaches an end,) the inverse of > is &lt;, and the inverse
437 of &lt; is >.</p></li>
438 <li><p>The inverse of ab is b'a' where b' is the inverse of b and a' is the
439 inverse of a. This is because abb'a' ≡ aea' ≡ aa' ≡ e.</p></li>
440 <li><p>The inverse of (a/b) is (b'/a'). (This is the key case of the key
441 property.) Going back to the definition of (/), we see there are three
442 sub-cases to consider. Before execution of (a/b)(b'/a'), the data tape
443 may be in one of three possible states:</p>
444
445 <ol>
446 <li><p>The current data cell is zero. So in (a/b), x is 0, which goes on
447 the stack and the current data cell becomes whatever was on the
448 stack (call it k.) The 0 on the stack is negated, thus stays 0
449 (because 0 - 0 = 0). The stack head is moved right. Neither a nor
450 b is evaluated. The stack head is moved back left. The stack and
451 data cells are swapped again, so 0 is back in the current data cell
452 and k is back in the current stack cell. This is the same as the
453 initial configuration, so (a/b) is equivalent to e. By the same
454 reasoning, (b'/a') is equivalent to e, and (a/b)(b'/a') ≡ ee ≡ e.</p></li>
455 <li><p>The current data cell is positive (x > 0). We first evaluate (a/b).
456 The data and stack cells are swapped: the current data cell becomes
457 k, and the current stack cell becomes x > 0. The current stack cell
458 is negated, so becomes -x &lt; 0. The stack head is moved to the right.</p>
459
460 <p>Because x > 0, the first of the sub-programs, a, is now evaluated.
461 The current data cell could be anything &mdash; call it k'.</p>
462
463 <p>The stack head is moved back to the left, so that the current stack
464 cell is once again -x &lt; 0, and it is swapped with the current data
465 cell, making it -x and making the current stack cell k'.</p>
466
467 <p>We are now to evaluate (b'/a'). This time, we know the current data
468 cell is negative (-x &lt; 0). The data and stack cells are swapped:
469 the current data cell becomes k', and the current stack cell becomes
470 -x &lt; 0. The current stack cell is negated, so becomes x > 0. The
471 stack head is moved to the right.</p>
472
473 <p>Because -x &lt; 0, the second of the sub-programs, a', is now evaluated.
474 Because a' is the inverse of a, and it is being applied to a state
475 that is the result of executing a, it will reverse this state to
476 what it was before a was executed (inside (a/b).) This means the
477 current data cell will become k once more.</p>
478
479 <p>The stack head is moved back to the left, so that the current stack
480 cell is once again x > 0, and it is swapped with the current data
481 cell, making it x and making the current stack cell k. This is
482 the state we started from, so (a/b)(b'/a') ≡ e.</p></li>
483 <li><p>Case 3 is an exact mirror image of case 2 &mdash; the only difference
484 is that the first time through, x &lt; 0 and b is evaluated, thus the
485 second time through, -x > 0 and b' is evaluated. Therefore
486 (a/b)(b'/a') ≡ e in this instance as well.</p></li>
487 </ol></li>
488 </ol></li>
489 </ol>
490
491 <p>QED.</p>
492
493 <h2>Driver and Unit Tests</h2>
494
495 <p>We define a few more convenience functions to cater for the execution
496 of Burro programs on an initial state.</p>
497
498 <pre><code> interpret text = run (parse text) newstate
499
500 main = do
501 [fileName] &lt;- getArgs
502 burroText &lt;- readFile fileName
503 putStrLn $ show $ interpret burroText
504 </code></pre>
505
506 <p>Although we have proved that Burro programs form a group, it is not a
507 mechanized proof, and only goes so far in helping us tell if the
508 implementation (which, for an executable semantics, is one and the same
509 as the formal semantic formulation) is correct. Unit tests can't tell us
510 definitively that there are no errors in the formulation, but they can
511 help us catch a class of errors, if there is one present.</p>
512
513 <p>For the first set of test cases, we give a set of pairs of Burro programs.
514 In each of these pairs, both programs should be equivalent in the sense of
515 evaluating to the same tape given an initial blank tape.</p>
516
517 <p>For the second set, we simply give a list of Burro programs. We test
518 each one by applying the annihilationOf function to it and checking that
519 the result of executing it on a blank tape is equivalent to e.</p>
520
521 <pre><code> testCases = [
522 ("+++", "-++-++-++"),
523 ("+(&gt;+++&lt;/---)", "-&gt;+++&lt;"),
524 ("-(+++/&gt;---&lt;)", "+&gt;---&lt;"),
525 ("(!/!)", "e"),
526 ("+(--------!/e)", "+(/)+"),
527 ("+++(/)", "---"),
528 ("---(/)", "+++"),
529 ("+&gt; +++ --(--(--(/&gt;&gt;&gt;&gt;&gt;+)+/&gt;&gt;&gt;+)+/&gt;+)+",
530 "+&gt; &gt;&gt;&gt; +(---(/+)/)+")
531 ]
532
533 annihilationTests = [
534 "e", "+", "-", "&lt;", "&gt;", "!",
535 "++", "--", "&lt;+&lt;-", "--&gt;&gt;--",
536 "(+/-)", "+(+/-)", "-(+/-)",
537 "+(--------!/e)"
538 ]
539
540 allTestCases = testCases ++ map nihil annihilationTests
541 where
542 nihil x = ((show (annihilationOf (parse x))), "e")
543 </code></pre>
544
545 <p>Our unit test harness evaluates to a list of tests which did
546 not pass. If all went well, it will evaluate to the empty list.</p>
547
548 <pre><code> test [] =
549 []
550 test ((a, b):cases) =
551 let
552 resultA = interpret a
553 resultB = interpret b
554 in
555 if
556 resultA == resultB
557 then
558 test cases
559 else
560 ((a, b):(test cases))
561 </code></pre>
562
563 <p>Finally, some miscellaneous functions for helping analyze why the
564 Burro tests you've written aren't working :)</p>
565
566 <pre><code> debug (a, b) = ((a, interpret a), (b, interpret b))
567
568 debugTests = map debug (test allTestCases)
569 </code></pre>
570
571 <h2>Implementing a Turing Machine in Burro</h2>
572
573 <p>First we note a Burro idiom. Assume the current data cell (which
574 we'll call C) contains an odd positive integer (which we'll call x.)
575 We can test if x = 1, write a zero into C, write -x into the cell
576 to the right of C, with the following construct:</p>
577
578 <pre><code>--(F&gt;/T&gt;)&lt;
579 </code></pre>
580
581 <p>T if executed if x = 1 and F is executed otherwise. (Remember,
582 we're assuming x is odd and positive.) To make the idiom hold, we
583 also insist that T and F both leave the data tape head in the
584 position they found it. If you are wonderinf where the zero came
585 from &mdash; it came from the stack.</p>
586
587 <p>We now note that this idiom can be nested to detect larger odd
588 numbers. For example, to determine if x is 1 or 3 or 5:</p>
589
590 <pre><code>--(--(--(F&gt;/T5&gt;)&lt;&gt;/T3&gt;)&lt;&gt;/T1&gt;)&lt;
591 </code></pre>
592
593 <p>We can of course optimize that a bit:</p>
594
595 <pre><code>--(--(--(F&gt;/T5&gt;)/T3&gt;)/T1&gt;)&lt;
596 </code></pre>
597
598 <p>Our basic strategy is to encode the state of the Turing machine's finite
599 control as a positive odd integer, which we will call a "finite control
600 index." We make sure to always keep the current finite control index
601 available in the current data cell at the start of each loop, and we
602 dispatch on its contents using the above idiom to simulate the finite
603 control. We may use odd integers to encode the symbols on the Turing
604 Machine's tape as well.</p>
605
606 <p>We map the Turing machine state onto the Burro data tape in an interleaved
607 fashion, where three adjacent cells are used to represent one TM tape
608 cell. The first (leftmost) cell in the triple contains the finite control
609 index described above. The second cell is a "junk cell" where we can write
610 stuff and never care about it again. The third cell contains our
611 representation of the contents of the TM tape cell. Moving the TM tape
612 head one cell is simulated by moving the Burro data tape head three cells,
613 skipping over the interim finite control cell and junk cell.</p>
614
615 <p>As we always want to be on an up-to-date finite control cell at the start
616 of each iteration, we must make sure to copy it to the new tape cell triple
617 each time we move the TM tape head to a new position. If we are
618 transitioning to a different TM state as well as moving the TM tape head,
619 we can even just write in the new state at the new finite control cell.
620 None of this copying requires intermediate loops, as these value are all
621 fixed constants. The only subtlety is that we must "erase" any finite
622 control cell we move off of (set it back to zero) so that we can get it to
623 the desired value by incrementation and decrementation only. The idiom
624 given above supplies that functionality for us.</p>
625
626 <p>Note that the junk cell is used to store the end result of (/), which
627 we don't care to predict, and don't care to use again. Note also that
628 the junk cell in which the value is stored belongs to the triple of the
629 destination TM tape cell, the one to which the TM tape head is moving
630 on this transition.</p>
631
632 <p>A concrete example follows. We consider the TM tape to be over an
633 alphabet of two symbols, 1 and 3 (or in fact any odd integer greater
634 than 1), and the finite control to have three states, denoted 1, 3,
635 and 5. In addition, state 7 (or in fact any odd integer greater than 5)
636 is a halt state.</p>
637
638 <p>In state 1, <br />
639 - If the symbol is 1, enter state 3; <br />
640 - If the symbol is 3, move head right one square, and remain in state 1. </p>
641
642 <pre><code>&gt;&gt;--(+++&gt;+&gt;/+&lt;&lt;+++&gt;)&lt;
643 </code></pre>
644
645 <p>In state 3, <br />
646 - If the symbol is 1, write 3, move head left one square, and remain in
647 state 3; <br />
648 - If the symbol is 3, move head right one square, and enter state 5. </p>
649
650 <pre><code>&gt;&gt;--(+++&gt;+++++&gt;/+++&lt;&lt;&lt;&lt;&lt;+++&gt;)&lt;
651 </code></pre>
652
653 <p>In state 5, <br />
654 - If the symbol is 1, write 3, move head right one square, and remain in
655 state 5; <br />
656 - If the symbol is 3, write 1 and enter state 7. </p>
657
658 <pre><code>&gt;&gt;--(+&lt;&lt;+++++++&gt;/+++&gt;+++++&gt;)&lt;
659 </code></pre>
660
661 <p>Putting it all together, including toggling the halt flag so that, unless
662 we reach state 7 or higher, we loop through this sequence indefinitely:</p>
663
664 <pre><code>!--(--(--(!&gt;/
665 &gt;&gt;--(+&lt;&lt;+++++++&gt;/+++&gt;+++++&gt;)&lt;
666 &gt;)/
667 &gt;&gt;--(+++&gt;+++++&gt;/+++&lt;&lt;&lt;&lt;&lt;+++&gt;)&lt;
668 &gt;)/
669 &gt;&gt;--(+++&gt;+&gt;/+&lt;&lt;+++&gt;)&lt;
670 &gt;)&lt;
671 </code></pre>
672
673 <p>It is not a very interesting Turing machine, but by following this
674 construction, it should be apparent how any arbitrary Turing machine
675 could be mapped to a Burro program in the same way.</p>
676
677 <p>Happy annihilating (for reals this time)!</p>
678
679 <p>-Chris Pressey <br />
680 Cat's Eye Technologies <br />
681 June 7, 2010 <br />
682 Evanston, Illinois, USA</p>
683 </body>
684 </html>
0 #!/usr/bin/perl -w
1
2 $title = "The Burro Programming Language, v2.0";
3 $lhs_input = "../src/Burro.lhs";
4 $lhs_temp = "lhs.tmp";
5 $html_temp = "html.tmp";
6 $html_output = "burro.html";
7
8 open INFILE, "<$lhs_input";
9 open OUTFILE, ">$lhs_temp";
10
11 while (defined ($line = <INFILE>)) {
12 chomp $line;
13 if ($line =~ /^\>(.*?)coding\:(.*?)$/) {
14 # pass
15 } elsif ($line =~ /^\>(.*?)$/) {
16 print OUTFILE " $1\n";
17 } else {
18 $line =~ s/\s\-\-\s/ \&mdash\; /g;
19 print OUTFILE "$line\n";
20 }
21 }
22
23 close INFILE;
24 close OUTFILE;
25
26 system "Markdown.pl <$lhs_temp >$html_temp";
27
28 open INFILE, "<$html_temp";
29 open OUTFILE, ">$html_output";
30
31 print OUTFILE <<"EOH";
32 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
33 <html xmlns="http://www.w3.org/1999/xhtml" lang="en">
34 <head>
35 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
36 <title>$title</title>
37 <link rel="stylesheet" type="text/css" href="markdown-lhs.css" />
38 </head>
39 <body>
40 EOH
41
42 while (defined ($line = <INFILE>)) {
43 print OUTFILE $line;
44 }
45
46 print OUTFILE <<"EOF";
47 </body>
48 </html>
49 EOF
50
51 close INFILE;
52 close OUTFILE;
53
54 system "rm *.tmp";
0 blockquote {
1 font-family: monospace;
2 white-space: pre;
3 border-style: solid;
4 border-width: 1px;
5 border-color: black;
6 padding-left: 3em;
7 }
8
9 pre {
10 border-style: solid;
11 border-width: 1px;
12 border-color: black;
13 padding-left: 3em;
14 padding-top: 1em;
15 padding-bottom: 1em;
16 }
+0
-3
eg/countdown-nullified.bur less more
0 (-!/e){!+/e}
1
2
+0
-1
eg/countdown.bur less more
0 (-!/e)
+0
-1
eg/test.bur less more
0 (->(->(-/e)</e)</e)>(-/e)>(-/e)
0 > -- coding: UTF-8
1
2 The Burro Programming Language
3 ==============================
4 Version 2.0
5 June 2010, Chris Pressey, Cat's Eye Technologies
6
7
8 Introduction
9 ------------
10
11 Burro is a programming language whose programs form an algebraic group under
12 the operation of concatenation and over the equivalence relation of "computes
13 the same function." This means that, for every Burro program, we can
14 construct a corresponding antiprogram that, when appended onto the first
15 program, results in a "no-op" program (a program with no effect -- the
16 identity function.)
17
18 (In fact, for every set of Burro programs that compute the same function,
19 there is a corresponding set of antiprograms, any of which can "cancel out"
20 any program in the first set. From our proof that Burro programs form a
21 group, we obtain a constructive algorithm which, for any given program, will
22 derive only one corresponding antiprogram, a kind of syntactic inverse.)
23
24 This is a kind of reversible computing, but Burro differs from most reversible
25 languages in that it is not the execution trace that is being "undone", but
26 the program itself that is being annihilated.
27
28 This document describes version 2.0 of the Burro language, a reformulation
29 which addresses several issues with Burro 1.0. An update to the language was
30 desired by the author after it was pointed out by Alex Smith that the set of
31 Burro version 1.0 programs do not, in fact, form a proper group (the inverse
32 of (/) is {\}, but no inverse of {\} is defined; also, the implementations
33 (at least) did not support moving the tape head left past the "start" of the
34 tape, so <> was not a well-defined program.)
35
36 Additionally in this document, we construct a Burro 2.0 program equivalent to
37 a certain Turing machine. While this Turing machine is not universal, the
38 translation method we use demonstrates how it would be possible to map an
39 arbitrary Turing machine to a Burro program, hopefully making uncontroversial
40 the idea that Burro qualifies as universal.
41
42 For further background information on the Burro project, you may also wish
43 to read the [Burro 1.0 article](burro-1.0.html), with the understanding that
44 the language description given there is obsolete.
45
46
47 Changes from Burro 1.0
48 ----------------------
49
50 The {\} construct does not appear in Burro 2.0. Instead, the (/) construct
51 serves as its own inverse. The tree-like structure of decision continuations
52 is not present in Burro 2.0 either. Instead, decision information is kept on
53 a second tape, called the "stack tape".
54
55 Henceforth in this document, the term Burro refers to Burro 2.0.
56
57
58 About this Document
59 -------------------
60
61 This document is a reference implementation of Burro in literate Haskell,
62 using Markdown syntax for the textual prose portions (although the version
63 you are reading may have been converted to another format, such as HTML,
64 for presentation.) As such, this document serves as an "executable
65 semantics", both defining the language and providing a ready tool.
66
67 > module Main where
68 > import System
69
70
71 Inductive Definition of a Burro Program
72 ---------------------------------------
73
74 The symbol e is a Burro program.
75 The symbol ! is a Burro program.
76 The symbol + is a Burro program.
77 The symbol - is a Burro program.
78 The symbol < is a Burro program.
79 The symbol > is a Burro program.
80 If a and b are Burro programs, then (a/b) is a Burro program.
81 If a and b are Burro programs, then ab is a Burro program.
82 Nothing else is a Burro program.
83
84 > data Burro = Null
85 > | ToggleHalt
86 > | Inc
87 > | Dec
88 > | GoLeft
89 > | GoRight
90 > | Test Burro Burro
91 > | Seq Burro Burro
92 > deriving (Read, Eq)
93
94
95 Representation of Burro Programs
96 --------------------------------
97
98 For a concrete representation, the symbols in the inductive definition
99 given above can be taken to be a subset of a character set; for the
100 purposes of this semantics, we will use the ASCII character set. Parsing
101 a given string of symbols into a Burro program is straightforward; all
102 symbols which are not Burro symbols are simply ignored.
103
104 > instance Show Burro where
105 > show Null = "e"
106 > show ToggleHalt = "!"
107 > show Inc = "+"
108 > show Dec = "-"
109 > show GoLeft = "<"
110 > show GoRight = ">"
111 > show (Test a b) = "(" ++ (show a) ++ "/" ++ (show b) ++ ")"
112 > show (Seq a b) = (show a) ++ (show b)
113 >
114 > parse string =
115 > let
116 > (rest, acc) = parseProgram string Null
117 > in
118 > trim acc
119 >
120 > parseProgram [] acc =
121 > ([], acc)
122 > parseProgram ('e':rest) acc =
123 > parseProgram rest (Seq acc Null)
124 > parseProgram ('+':rest) acc =
125 > parseProgram rest (Seq acc Inc)
126 > parseProgram ('-':rest) acc =
127 > parseProgram rest (Seq acc Dec)
128 > parseProgram ('<':rest) acc =
129 > parseProgram rest (Seq acc GoLeft)
130 > parseProgram ('>':rest) acc =
131 > parseProgram rest (Seq acc GoRight)
132 > parseProgram ('!':rest) acc =
133 > parseProgram rest (Seq acc ToggleHalt)
134 > parseProgram ('(':rest) acc =
135 > let
136 > (rest', thenprog) = parseProgram rest Null
137 > (rest'', elseprog) = parseProgram rest' Null
138 > test = Test thenprog elseprog
139 > in
140 > parseProgram rest'' (Seq acc test)
141 > parseProgram ('/':rest) acc =
142 > (rest, acc)
143 > parseProgram (')':rest) acc =
144 > (rest, acc)
145 > parseProgram (_:rest) acc =
146 > parseProgram rest acc
147 >
148 > trim (Seq Null a) = trim a
149 > trim (Seq a Null) = trim a
150 > trim (Seq a b) = Seq (trim a) (trim b)
151 > trim (Test a b) = Test (trim a) (trim b)
152 > trim x = x
153
154
155 Group Properties of Burro Programs
156 ----------------------------------
157
158 We assert these first, and when we describe the program semantics we will
159 show that the semantics do not violate them.
160
161 The inverse of e is e: ee = e
162 The inverse of ! is !: !! = e
163 The inverse of + is -: +- = e
164 The inverse of - is +: -+ = e
165 The inverse of < is >: <> = e
166 The inverse of > is <: >< = e
167 If aa' = e and bb' = e, (a/b)(b'/a') = e.
168 If aa' = e and bb' = e, abb'a' = e.
169
170 > inverse Null = Null
171 > inverse ToggleHalt = ToggleHalt
172 > inverse Inc = Dec
173 > inverse Dec = Inc
174 > inverse GoLeft = GoRight
175 > inverse GoRight = GoLeft
176 > inverse (Test a b) = Test (inverse b) (inverse a)
177 > inverse (Seq a b) = Seq (inverse b) (inverse a)
178
179 For every Burro program x, annihilationOf x is always equivalent
180 computationally to e.
181
182 > annihilationOf x = Seq x (inverse x)
183
184
185 State Model for Burro Programs
186 ------------------------------
187
188 Central to the state of a Burro program is an object called a tape.
189 A tape consists of a sequence of cells in a one-dimensional array,
190 unbounded in both directions. Each cell contains an integer of unbounded
191 extent, both positive and negative. The initial value of each cell is
192 zero. One of the cells of the tape is distinguished as the "current cell";
193 this is the cell that we think of as having the "tape head" hovering over it
194 at the moment.
195
196 In this semantics, we represent a tape as two lists, which we treat as
197 stacks. The first list contains the cell under the tape head, and
198 everything to the left of the tape head (in the reverse order from how it
199 appears on the tape.) The second list contains everything to the right of
200 the tape head, in the same order as it appears on the tape.
201
202 > data Tape = Tape [Integer] [Integer]
203 > deriving (Read)
204 >
205 > instance Show Tape where
206 > show t@(Tape l r) =
207 > let
208 > (Tape l' r') = strip t
209 > in
210 > show (reverse l') ++ "<" ++ (show r')
211
212 When comparing two tapes for equality, we must disregard any zero cells
213 farther to the left/right than the outermost non-zero cells. Specifically,
214 we strip leading/trailing zeroes from tapes before comparison. We don't
215 strip out a zero that a tape head is currently over, however.
216
217 Also, the current cell must be the same for both tapes (that is, tape heads
218 must be in the same location) for two tapes to be considered equal.
219
220 > stripzeroes list = (reverse (sz (reverse list)))
221 > where sz [] = []
222 > sz (0:rest) = sz rest
223 > sz x = x
224 >
225 > ensurecell [] = [0]
226 > ensurecell x = x
227 >
228 > strip (Tape l r) = Tape (ensurecell (stripzeroes l)) (stripzeroes r)
229 >
230 > tapeeq :: Tape -> Tape -> Bool
231 > tapeeq t1 t2 =
232 > let
233 > (Tape t1l t1r) = strip t1
234 > (Tape t2l t2r) = strip t2
235 > in
236 > (t1l == t2l) && (t1r == t2r)
237 >
238 > instance Eq Tape where
239 > t1 == t2 = tapeeq t1 t2
240
241 A convenience function for creating an inital tape is also provided.
242
243 > tape :: [Integer] -> Tape
244 > tape x = Tape [head x] (tail x)
245
246 We now define some operations on tapes that we will use in the semantics.
247 First, operations on tapes that alter or access the cell under the tape head.
248
249 > inc (Tape (cell:left) right) = Tape (cell + 1 : left) right
250 > dec (Tape (cell:left) right) = Tape (cell - 1 : left) right
251 > get (Tape (cell:left) right) = cell
252 > set (Tape (_:left) right) value = Tape (value : left) right
253
254 Next, operations on tapes that move the tape head.
255
256 > left (Tape (cell:[]) right) = Tape [0] (cell:right)
257 > left (Tape (cell:left) right) = Tape left (cell:right)
258 > right (Tape left []) = Tape (0:left) []
259 > right (Tape left (cell:right)) = Tape (cell:left) right
260
261 Finally, an operation on two tapes that swaps the current cell between
262 them.
263
264 > swap t1 t2 = (set t1 (get t2), set t2 (get t1))
265
266 A program state consists of:
267
268 - A "data tape";
269 - A "stack tape"; and
270 - A flag called the "halt flag", which may be 0 or 1.
271
272 The 0 and 1 are represented by False and True boolean values in this
273 semantics.
274
275 > data State = State Tape Tape Bool
276 > deriving (Show, Read, Eq)
277 >
278 > newstate = State (tape [0]) (tape [0]) True
279
280
281 Semantics of Burro Programs
282 ---------------------------
283
284 Each instruction is defined as a function from program state to program
285 state. Concatenation of instructions is defined as composition of
286 functions, like so:
287
288 If ab is a Burro program, and a maps state S to state S', and b maps
289 state S' to S'', then ab maps state S to state S''.
290
291 > exec (Seq a b) t = exec b (exec a t)
292
293 The e instruction is the identity function on states.
294
295 > exec Null s = s
296
297 The ! instruction toggles the halt flag. If it is 0 in the input state, it
298 is 1 in the output state, and vice versa.
299
300 > exec ToggleHalt (State dat stack halt) = (State dat stack (not halt))
301
302 The + instruction increments the current data cell, while - decrements the
303 current data cell.
304
305 > exec Inc (State dat stack halt) = (State (inc dat) stack halt)
306 > exec Dec (State dat stack halt) = (State (dec dat) stack halt)
307
308 The instruction < makes the cell to the left of the current data cell, the
309 new current data cell. The instruction > makes the cell to the right of the
310 current data cell, the new current data cell.
311
312 > exec GoLeft (State dat stack halt) = (State (left dat) stack halt)
313 > exec GoRight (State dat stack halt) = (State (right dat) stack halt)
314
315 (a/b) is the conditional construct, which is quite special.
316
317 First, the current data cell is remembered for the duration of the execution
318 of this construct -- let's call it x.
319
320 Second, the current data cell and the current stack cell are swapped.
321
322 Third, the current stack cell is negated.
323
324 Fourth, the stack cell to the right of the current stack cell is made
325 the new current stack cell.
326
327 Fifth, if x is positive, a is evaluated; if x is negative, b is evaluated;
328 otherwise x = 0 and neither is evaluated. Evaluation occurs in the state
329 established by the preceding four steps.
330
331 Sixth, the stack cell to the left of the current stack cell is made
332 the new current stack cell.
333
334 Seventh, the current data cell and the current stack cell are swapped again.
335
336 > exec (Test thn els) (State dat stack halt) =
337 > let
338 > x = get dat
339 > (dat', stack') = swap dat stack
340 > stack'' = right (set stack' (0 - (get stack')))
341 > f = if x > 0 then thn else if x < 0 then els else Null
342 > (State dat''' stack''' halt') = exec f (State dat' stack'' halt)
343 > (dat'''', stack'''') = swap dat''' (left stack''')
344 > in
345 > (State dat'''' stack'''' halt')
346
347 We observe an invariant here: because only the (a/b) construct affects the
348 stack tape, and because it does so in a monotonic way -- that is, both a
349 and b inside (a/b) have access only to the portion of the stack tape to the
350 right of what (a/b) has access to -- the current stack cell in step seven
351 always holds the same value as the current stack cell in step two, except
352 negated.
353
354
355 Repetition
356 ----------
357
358 The repetition model of Burro 2.0 is identical to that of Burro 1.0.
359 The program text is executed, resulting in a final state, S. If, in
360 S, the halt flag is 1, execution terminates with state S. On the other
361 hand, if the halt flag is 0, the program text is executed once more,
362 this time on state S, and the whole procedure repeats. Initially the
363 halt flag is 1, so if ! is never executed, the program never repeats.
364
365 Additionally, each time the program repeats, the stack tape is cleared.
366
367 > run program state =
368 > let
369 > state'@(State dat' stack' halt') = exec program state
370 > in
371 > if
372 > not halt'
373 > then
374 > run program (State dat' (tape [0]) True)
375 > else
376 > state'
377
378
379 Central theorem of Burro
380 ------------------------
381
382 We now have established enough definitions to give a proof of the central
383 theorem of Burro, which is:
384
385 *Theorem: The set of all Burro programs forms a group over computational
386 equivalence under the operation of concatenation.*
387
388 As covered in the Burro 1.0 article, a "group over an equivalence relation"
389 captures the notion of replacing the concept of equality in the group
390 axioms with the concept of equivalency. Our particular equivalence relation
391 here is that two programs are equivalent if they compute the same function.
392
393 In order to show that a set G is a group, it is sufficient to show the
394 following four properties hold:
395
396 1. Closure: For all a, b in G, ab is also in G.
397
398 This follows from the inductive definition of Burro programs.
399
400 2. Associativity: For all a, b and c in G, (ab)c ≡ a(bc).
401
402 This follows from the definition of concatenation (sequential composition);
403 it doesn't matter if we concatenate a with b first, then concatenate that
404 with c, or if we concatenate b with c first, then concatenate a with that.
405 Either way the result is the same string (or in this case, the same Burro
406 program.)
407
408 3. Identity element: There exists an element e in G, such that for every
409 element a in G, ea ≡ ae ≡ a.
410
411 The instruction e in Burro has no effect on the program state. Therefore
412 concatenating it to any existing program, or concatenating any existing
413 program to it, results in a computationally equivalent program.
414
415 4. Inverse element: For each a in G, there exists an element b in G such
416 that ab ≡ ba ≡ e.
417
418 This is the key property. We first show that it holds for each element of
419 the inductive definition of Burro programs. We can then conclude, through
420 structural induction, that all Burro programs have this property.
421
422 1. Since e is the identity function on states, e is trivially its own
423 inverse.
424
425 2. Since toggling the flag twice is the same as not changing it at all,
426 the inverse of ! is !.
427
428 3. By the definitions of incrementation and decrementation, and because
429 data cells cannot overflow, the inverse of + is -, and the inverse
430 of - is +.
431
432 4. By the definitions of left and right, and because the data tape is
433 unbounded (never reaches an end,) the inverse of > is <, and the inverse
434 of < is >.
435
436 5. The inverse of ab is b'a' where b' is the inverse of b and a' is the
437 inverse of a. This is because abb'a' ≡ aea' ≡ aa' ≡ e.
438
439 6. The inverse of (a/b) is (b'/a'). (This is the key case of the key
440 property.) Going back to the definition of (/), we see there are three
441 sub-cases to consider. Before execution of (a/b)(b'/a'), the data tape
442 may be in one of three possible states:
443
444 1. The current data cell is zero. So in (a/b), x is 0, which goes on
445 the stack and the current data cell becomes whatever was on the
446 stack (call it k.) The 0 on the stack is negated, thus stays 0
447 (because 0 - 0 = 0). The stack head is moved right. Neither a nor
448 b is evaluated. The stack head is moved back left. The stack and
449 data cells are swapped again, so 0 is back in the current data cell
450 and k is back in the current stack cell. This is the same as the
451 initial configuration, so (a/b) is equivalent to e. By the same
452 reasoning, (b'/a') is equivalent to e, and (a/b)(b'/a') ≡ ee ≡ e.
453
454 2. The current data cell is positive (x > 0). We first evaluate (a/b).
455 The data and stack cells are swapped: the current data cell becomes
456 k, and the current stack cell becomes x > 0. The current stack cell
457 is negated, so becomes -x < 0. The stack head is moved to the right.
458
459 Because x > 0, the first of the sub-programs, a, is now evaluated.
460 The current data cell could be anything -- call it k'.
461
462 The stack head is moved back to the left, so that the current stack
463 cell is once again -x < 0, and it is swapped with the current data
464 cell, making it -x and making the current stack cell k'.
465
466 We are now to evaluate (b'/a'). This time, we know the current data
467 cell is negative (-x < 0). The data and stack cells are swapped:
468 the current data cell becomes k', and the current stack cell becomes
469 -x < 0. The current stack cell is negated, so becomes x > 0. The
470 stack head is moved to the right.
471
472 Because -x < 0, the second of the sub-programs, a', is now evaluated.
473 Because a' is the inverse of a, and it is being applied to a state
474 that is the result of executing a, it will reverse this state to
475 what it was before a was executed (inside (a/b).) This means the
476 current data cell will become k once more.
477
478 The stack head is moved back to the left, so that the current stack
479 cell is once again x > 0, and it is swapped with the current data
480 cell, making it x and making the current stack cell k. This is
481 the state we started from, so (a/b)(b'/a') ≡ e.
482
483 3. Case 3 is an exact mirror image of case 2 -- the only difference
484 is that the first time through, x < 0 and b is evaluated, thus the
485 second time through, -x > 0 and b' is evaluated. Therefore
486 (a/b)(b'/a') ≡ e in this instance as well.
487
488 QED.
489
490
491 Driver and Unit Tests
492 ---------------------
493
494 We define a few more convenience functions to cater for the execution
495 of Burro programs on an initial state.
496
497 > interpret text = run (parse text) newstate
498
499 > main = do
500 > [fileName] <- getArgs
501 > burroText <- readFile fileName
502 > putStrLn $ show $ interpret burroText
503
504 Although we have proved that Burro programs form a group, it is not a
505 mechanized proof, and only goes so far in helping us tell if the
506 implementation (which, for an executable semantics, is one and the same
507 as the formal semantic formulation) is correct. Unit tests can't tell us
508 definitively that there are no errors in the formulation, but they can
509 help us catch a class of errors, if there is one present.
510
511 For the first set of test cases, we give a set of pairs of Burro programs.
512 In each of these pairs, both programs should be equivalent in the sense of
513 evaluating to the same tape given an initial blank tape.
514
515 For the second set, we simply give a list of Burro programs. We test
516 each one by applying the annihilationOf function to it and checking that
517 the result of executing it on a blank tape is equivalent to e.
518
519 > testCases = [
520 > ("+++", "-++-++-++"),
521 > ("+(>+++</---)", "->+++<"),
522 > ("-(+++/>---<)", "+>---<"),
523 > ("(!/!)", "e"),
524 > ("+(--------!/e)", "+(/)+"),
525 > ("+++(/)", "---"),
526 > ("---(/)", "+++"),
527 > ("+> +++ --(--(--(/>>>>>+)+/>>>+)+/>+)+",
528 > "+> >>> +(---(/+)/)+")
529 > ]
530
531 > annihilationTests = [
532 > "e", "+", "-", "<", ">", "!",
533 > "++", "--", "<+<-", "-->>--",
534 > "(+/-)", "+(+/-)", "-(+/-)",
535 > "+(--------!/e)"
536 > ]
537
538 > allTestCases = testCases ++ map nihil annihilationTests
539 > where
540 > nihil x = ((show (annihilationOf (parse x))), "e")
541
542 Our unit test harness evaluates to a list of tests which did
543 not pass. If all went well, it will evaluate to the empty list.
544
545 > test [] =
546 > []
547 > test ((a, b):cases) =
548 > let
549 > resultA = interpret a
550 > resultB = interpret b
551 > in
552 > if
553 > resultA == resultB
554 > then
555 > test cases
556 > else
557 > ((a, b):(test cases))
558
559 Finally, some miscellaneous functions for helping analyze why the
560 Burro tests you've written aren't working :)
561
562 > debug (a, b) = ((a, interpret a), (b, interpret b))
563
564 > debugTests = map debug (test allTestCases)
565
566
567 Implementing a Turing Machine in Burro
568 --------------------------------------
569
570 First we note a Burro idiom. Assume the current data cell (which
571 we'll call C) contains an odd positive integer (which we'll call x.)
572 We can test if x = 1, write a zero into C, write -x into the cell
573 to the right of C, with the following construct:
574
575 --(F>/T>)<
576
577 T if executed if x = 1 and F is executed otherwise. (Remember,
578 we're assuming x is odd and positive.) To make the idiom hold, we
579 also insist that T and F both leave the data tape head in the
580 position they found it. If you are wonderinf where the zero came
581 from -- it came from the stack.
582
583 We now note that this idiom can be nested to detect larger odd
584 numbers. For example, to determine if x is 1 or 3 or 5:
585
586 --(--(--(F>/T5>)<>/T3>)<>/T1>)<
587
588 We can of course optimize that a bit:
589
590 --(--(--(F>/T5>)/T3>)/T1>)<
591
592 Our basic strategy is to encode the state of the Turing machine's finite
593 control as a positive odd integer, which we will call a "finite control
594 index." We make sure to always keep the current finite control index
595 available in the current data cell at the start of each loop, and we
596 dispatch on its contents using the above idiom to simulate the finite
597 control. We may use odd integers to encode the symbols on the Turing
598 Machine's tape as well.
599
600 We map the Turing machine state onto the Burro data tape in an interleaved
601 fashion, where three adjacent cells are used to represent one TM tape
602 cell. The first (leftmost) cell in the triple contains the finite control
603 index described above. The second cell is a "junk cell" where we can write
604 stuff and never care about it again. The third cell contains our
605 representation of the contents of the TM tape cell. Moving the TM tape
606 head one cell is simulated by moving the Burro data tape head three cells,
607 skipping over the interim finite control cell and junk cell.
608
609 As we always want to be on an up-to-date finite control cell at the start
610 of each iteration, we must make sure to copy it to the new tape cell triple
611 each time we move the TM tape head to a new position. If we are
612 transitioning to a different TM state as well as moving the TM tape head,
613 we can even just write in the new state at the new finite control cell.
614 None of this copying requires intermediate loops, as these value are all
615 fixed constants. The only subtlety is that we must "erase" any finite
616 control cell we move off of (set it back to zero) so that we can get it to
617 the desired value by incrementation and decrementation only. The idiom
618 given above supplies that functionality for us.
619
620 Note that the junk cell is used to store the end result of (/), which
621 we don't care to predict, and don't care to use again. Note also that
622 the junk cell in which the value is stored belongs to the triple of the
623 destination TM tape cell, the one to which the TM tape head is moving
624 on this transition.
625
626 A concrete example follows. We consider the TM tape to be over an
627 alphabet of two symbols, 1 and 3 (or in fact any odd integer greater
628 than 1), and the finite control to have three states, denoted 1, 3,
629 and 5. In addition, state 7 (or in fact any odd integer greater than 5)
630 is a halt state.
631
632 In state 1,
633 - If the symbol is 1, enter state 3;
634 - If the symbol is 3, move head right one square, and remain in state 1.
635
636 >>--(+++>+>/+<<+++>)<
637
638 In state 3,
639 - If the symbol is 1, write 3, move head left one square, and remain in
640 state 3;
641 - If the symbol is 3, move head right one square, and enter state 5.
642
643 >>--(+++>+++++>/+++<<<<<+++>)<
644
645 In state 5,
646 - If the symbol is 1, write 3, move head right one square, and remain in
647 state 5;
648 - If the symbol is 3, write 1 and enter state 7.
649
650 >>--(+<<+++++++>/+++>+++++>)<
651
652 Putting it all together, including toggling the halt flag so that, unless
653 we reach state 7 or higher, we loop through this sequence indefinitely:
654
655 !--(--(--(!>/
656 >>--(+<<+++++++>/+++>+++++>)<
657 >)/
658 >>--(+++>+++++>/+++<<<<<+++>)<
659 >)/
660 >>--(+++>+>/+<<+++>)<
661 >)<
662
663 It is not a very interesting Turing machine, but by following this
664 construction, it should be apparent how any arbitrary Turing machine
665 could be mapped to a Burro program in the same way.
666
667 Happy annihilating (for reals this time)!
668
669 -Chris Pressey
670 Cat's Eye Technologies
671 June 7, 2010
672 Evanston, Illinois, USA
0 # Makefile for burro.
0 # Makefile for Burro.
11
2 CC?=gcc
3 OBJS=burro.o tree.o
4 PROG=burro
2 HC=ghc
3 HCFLAGS=-O
4 O=.o
5 PROG=Burro
56
6 all: $(PROG)
7 OBJS=Burro${O}
78
8 $(PROG): $(OBJS)
9 $(CC) $(OBJS) -o $(PROG)
9 all: ${PROG}
1010
11 burro.o: burro.c tree.h
12 $(CC) -Wall -c burro.c -o burro.o
11 Burro${O}: Burro.lhs
12 ${HC} ${HCFLAGS} -c $*.lhs
1313
14 tree.o: tree.c tree.h
15 $(CC) -Wall -c tree.c -o tree.o
14 ${PROG}: ${OBJS}
15 ${HC} -o ${PROG} -O ${OBJS}
16 strip ${PROG}
1617
1718 clean:
18 rm -rf $(OBJS) $(PROG)
19 rm -rf *${O} *.hi ${PROG}
+0
-327
src/burro.c less more
0 /*
1 * Copyright (c)2005-2007 Cat's Eye Technologies. All rights reserved.
2 *
3 * Redistribution and use in source and binary forms, with or without
4 * modification, are permitted provided that the following conditions
5 * are met:
6 *
7 * Redistributions of source code must retain the above copyright
8 * notices, this list of conditions and the following disclaimer.
9 *
10 * Redistributions in binary form must reproduce the above copyright
11 * notices, this list of conditions, and the following disclaimer in
12 * the documentation and/or other materials provided with the
13 * distribution.
14 *
15 * Neither the names of the copyright holders nor the names of their
16 * contributors may be used to endorse or promote products derived
17 * from this software without specific prior written permission.
18 *
19 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
20 * ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
21 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
22 * FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
23 * COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
24 * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
25 * BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
26 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
27 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
28 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
29 * ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
30 * POSSIBILITY OF SUCH DAMAGE.
31 */
32
33 /*
34 * burro.c
35 *
36 * A quick-and-dirty interpreter for the Burro programming language,
37 * where the set of possible programs is a group under concatenation
38 * (roughly speaking; see burro.html for the full story.)
39 *
40 * $Id: burro.c 10 2007-10-10 01:17:52Z catseye $
41 */
42
43 #include <stdio.h>
44 #include <stdlib.h>
45 #include <string.h>
46 #include <unistd.h> /* for getopt() */
47
48 #include "tree.h"
49
50 /* constants */
51
52 #ifndef TAPE_SIZE
53 #define TAPE_SIZE 65536
54 #endif
55
56 #define TAPE_START (TAPE_SIZE / 2) /* for entry and dump */
57 #define TAPE_END (TAPE_START + 100) /* for dumps only */
58
59 #ifndef PROG_SIZE
60 #define PROG_SIZE 65536
61 #endif
62
63 /* globals */
64
65 char prog[PROG_SIZE];
66 int pc;
67
68 long tape[TAPE_SIZE];
69 int th;
70
71 int halt_flag;
72
73 int debug_flag = 0;
74
75 FILE *f;
76
77 struct tree *root; /* structure into which we save test results */
78
79 /********* debugging *********/
80
81 void
82 debug_state(void)
83 {
84 if (!debug_flag)
85 return;
86
87 fprintf(stderr,
88 "OP='%c' PC=%3d TH=%3d TC=%4ld HF=%1d ",
89 prog[pc], pc, th - TAPE_START, tape[th], halt_flag);
90 }
91
92 void
93 debug_tree(struct tree *t, struct tree *s)
94 {
95 if (!debug_flag)
96 return;
97 tree_dump(stderr, t, s);
98 }
99
100 void
101 debug_newline(void)
102 {
103 if (debug_flag)
104 fprintf(stderr, "\n");
105 }
106
107 /**** usage info ****/
108
109 void
110 usage(void)
111 {
112 fprintf(stderr, "Usage: burro [-d] filename\n");
113 exit(1);
114 }
115
116 /**** MAIN ****/
117
118 int
119 main(int argc, char **argv)
120 {
121 int ch; /* getopt character */
122 struct tree *save;
123 int i;
124
125 /* get cmdline args */
126 while ((ch = getopt(argc, argv, "d")) != -1) {
127 switch ((char)ch) {
128 case 'd':
129 debug_flag++;
130 break;
131 case '?':
132 default:
133 usage();
134 }
135 }
136 argv += optind;
137 argc -= optind;
138
139 if (argc < 1)
140 usage();
141
142 /* load */
143
144 f = fopen(argv[0], "r");
145 if (f == NULL) {
146 fprintf(stderr, "Couldn't open '%s'\n", argv[0]);
147 exit(1);
148 }
149 pc = 0;
150 for (;;) {
151 if (pc >= PROG_SIZE) break;
152 prog[pc] = fgetc(f);
153 if (feof(f)) break;
154 if (strchr("+-<>(/){\\}!e", prog[pc]) == NULL) continue;
155 pc++;
156 }
157 prog[pc] = '\0';
158 fclose(f);
159
160 /* initialize tape */
161
162 for (th = 0; th < TAPE_SIZE; th++)
163 tape[th] = 0;
164
165 /* read tape from input */
166
167 th = TAPE_START;
168 for (;;) {
169 scanf("%ld", &tape[th]);
170 if (feof(stdin)) {
171 tape[th] = 0;
172 break;
173 }
174 if (debug_flag) {
175 fprintf(stderr,
176 "Writing %ld into position %d\n",
177 tape[th], th);