git @ Cat's Eye Technologies Burro / master doc / burro-1.0.html
master

Tree @master (Download .tar.gz)

burro-1.0.html @masterraw · history · blame

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<!-- encoding: UTF-8 -->
<html xmlns="http://www.w3.org/1999/xhtml" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<title>The Burro Programming Language, version 1.0</title>
</head>
<body>

<h1>The Burro Programming Language, version 1.0</h1>

<p>October 2007, Chris Pressey, Cat's Eye Technologies.</p>

<p><em>Note: This document describes version 1.0 of the Burro language.  For documentation
on the latest version of the language, please see <a href="../src/_Burro.lhs.html">Burro.lhs</a>.</em></p>

<h2>1. Introduction</h2>

<p><em>Burro</em> is a Brainfuck-like programming language whose programs form an
algebraic group under concatenation.</p>

<p>(At least, that is how I originally would have described it.  But that description
turns out to be not entirely precise, because the technical meanings of "group" and
"program" come into conflict.  A more precise statement would be: "Burro is
a semi-formal programming language, the set of whose program texts, paired with the operation
of concatenation, forms an algebraic group over a semantic equivalence relation."
But the first version is close enough for jazz, and rolls off the tongue more easily...)</p>

<p>Anyway, what does it mean?  It means that, among other things, every Burro program has
an <em>antiprogram</em> — a series of instructions that can be appended to it
to annihilate its behavior.  The resulting catenated program has the
same semantics as no program at all — a "no-op," or a zero-length program.</p>

<p>Why is this at all remarkable?  Well, take the Brainfuck program fragment <code>[-]+[]</code>.
What could you append to it to it to make it into a "no-op" program?
Evidently <em>nothing</em>, because once the interpreter enters an infinite loop, it's not
going to care what instructions you've put after the loop.  And a program that loops forever
isn't the same as one that does nothing at all.</p>

<p>So not all Brainfuck programs have antiprograms.  Despite that, Brainfuck does embody a lot of
symmetry. Group theory, too, is a branch of
mathematics particularly suited to the study of symmetry.  And as you might imagine,
there is a distinct relation between symmetrical programming languages and reversible
programming (even though it may not be immediatly clear exactly what that relationship is.) 
These are some of the factors that encouraged me to design Burro.</p>

<h2>2. Background</h2>

<p>Before explaining Burro, a short look of group theory and of the theory of
computation would probably be helpful.</p>

<h3>Group Theory</h3>

<p>Recall (or go look up in an abstract algebra textbook) that a <em>group</em> is
a pair of a set <var>S</var> and a binary operation
· : <var>S</var> × <var>S</var><var>S</var>
that obeys the following three axioms:</p>

<ul>

<li>For any three elements <var>a</var>, <var>b</var>, and <var>c</var> of
the set <var>S</var>, (<var>a</var> · <var>b</var>) · <var>c</var> =
<var>a</var> · (<var>b</var> · <var>c</var>).  In other words,
the operation is "associative."  Parentheses don't matter, and we generally leave them out.</li>

<li>There exists some element of <var>S</var>, which we call <b>e</b>, such that
<var>a</var> · <b>e</b> = <b>e</b> · <var>a</var> = <var>a</var>
for every element <var>a</var> of <var>S</var>.  Think of
<b>e</b> as a "neutral" element that just doesn't contribute anything.</li>

<li>For every element <var>a</var> of <var>S</var> there is an element
<var>a'</var> of <var>S</var> such that <var>a</var> · <var>a'</var> = <b>e</b>.
That is, for any element, you can find some element that "annihilates" it.</li>

</ul>

<p>There are lots of examples of groups — the integers under the operation of
addition, for example, where <b>e</b> is 0, and the annihilator for any integer
is simply its negative (because <var>x</var> + (-<var>x</var>) always equals 0.)</p>

<p>There are also lots of things you can prove are true about any group
(that is, about groups in general.) For instance, that <b>e</b> is unique: if
<var>a</var> · <var>x</var> = <var>a</var> and
<var>a</var> · <var>y</var> = <var>a</var> then
<var>x</var> = <var>y</var> = <b>e</b>.  (This particular property will
become relevant very soon, so keep it in mind as you read the next section.)</p>

<p>The set on which a group is based can have any number of elements.  Research
and literature in group theory often concentrates on finite groups, because these
are in some ways more interesting, and they are useful in error-correcting
codes and other applications.  However, the set of Burro programs is countably
infinite, so we will be dealing with infinite groups here.</p>

<h3>Theory of Computation</h3>

<p>I don't need to call on a lot of theory of computation here except to point
out one fact: for any program, there are an infinite number of equivalent programs.
There are formal proofs of this, but they can be messy, and it's something
that should be obvious to most programmers.  Probably the simplest example, in Brainfuck,
is that <code>+-</code>, <code>++--</code>, <code>+++---</code>, <code>++++----</code>,
etc., all have the same effect.</p>

<p>To be specific, by "program" here I mean "program text" in a
particular language; if we're talking about "abstract programs" in no particular
language, then you could well say that there is only and exactly one program that
does any one thing, it's just that there are an infinite number of concrete
representations of it.</p>

<p>This distinction becomes important with respect to treating programs
as elements of a group, like we're doing in Burro.  Some program will
be the neutral element <b>e</b>.  But either <em>many</em> programs will
be equivalent to this program — in which case <b>e</b> is not unique, contrary to
what group theory tells us — or we are talking about abstract programs
independent of any programming language, in which case our goal of defining a particular
language called "Burro" for this purpose seems a bit futile.</p>

<p>There are a couple of ways this could be resolved.  We could foray into
domain theory, and try to impose a group structure on the semantics of programs
irrespective of the language they are in.  Or we could venture into representation
theory, and see if the program texts can act as generators of the group elements.
Both of these approaches could be interesting, but I chose an approach that I
found to be less of a distraction, and possibly more intuitive, at the cost of
introducing a slight variation on the notion of a group.</p>

<h3>Group Theory, revisited</h3>

<p>To this end, let's examine the idea of a <em>group over an equivalence relation</em>.
All this is, really, is being specific about what constitutes "equals" in those
group axioms I listed earlier.  In mathematics there is a well-established notion of
an <em>equivalence relation</em> — a relationship between elements
which paritions a set into
disjoint equivalence classes, where every element in a class is considered
equivalent to every other element in that same class (and inequivalent to any
element in any other class.)</p>

<p>We can easily define an equivalence relation on programs (that is,
program texts.)  We simply say that two programs are
equivalent if they have the same semantics: they map the same inputs to the
same outputs, they compute the same function, they "do the same thing" as
far as an external observer can tell, assuming he or she is unconcerned with
performance issues. As you can imagine, this relation will be very useful for
our purpose.</p>

<p>We can also reformulate the group axioms using an equivalence relation.
At the very least, I can't see why it should be invalid to do so.  (Indeed, this seems to
be the general idea behind using "quotients" in abstract algebra.  In our case, we
have a set of program texts and a "semantic" equivalence relation "are equivalent
programs", and the quotient set is the set of all computable functions
regardless of their concrete representation.)</p>

<p>So let's go ahead and take that liberty.  The resulting algebraic structure
should be quite similar to what we had before,
but with the equivalence classes becoming the real "members" of the group,
and with each class containing many individual elements which are treated
interchangably with respect to the group axioms.</p>

<p>I'll summarize the modified definition here.  A <em>group over an equivalence relation</em>
is a triple 〈<var>S</var>,·,≡〉 where:</p>
<ul>
<li><var>S</var> is a set</li>
<li>· : <var>S</var> × <var>S</var><var>S</var> is a binary operation over <var>S</var></li>
<li>≡ is a reflexive, transitive, and symmetrical binary relation over <var>S</var></li>
</ul>
<p>where the following axioms are also satisfied:</p>
<ul>
<li><var>a</var>, <var>b</var>, <var>c</var><var>S</var>: (<var>a</var> · <var>b</var>) · <var>c</var><var>a</var> · (<var>b</var> · <var>c</var>)</li>
<li><b>e</b><var>S</var>: ∀ <var>a</var><var>S</var>: <var>a</var> · <b>e</b><b>e</b> · <var>a</var><var>a</var></li>
<li><var>a</var><var>S</var>: ∃ <var>a'</var><var>S</var>: <var>a</var> · <var>a'</var><b>e</b></li>
</ul>

<p>Every theorem that applies to groups should be easy to modify to be applicable
to a group over an equivalence relation: just replace = with ≡.  So what
we have, for example, is that while any given <b>e</b> itself might not be unique, the
equivalence class <b>E</b><var>S</var> that contains it is:
<b>E</b> is the only equivalence class that contains
elements like <b>e</b> and, for the purposes of the group, all of these elements are
interchangeable.</p>

<h2>3. Syntax and Semantics</h2>

<h3>Five-instruction Foundation</h3>

<p>Burro is intended to be Brainfuck-like, so we could start by examining which
parts of Brainfuck are already suitable for Burro and which parts will have to
be modified or rejected.</p>

<p>First, note that Brainfuck is traditionally very lenient about what
constitutes a "no-op" instruction.  Just about any symbol that isn't explicitly
mentioned in the instruction set is treated as a no-op (and this behaviour turns
out to be useful for inserting comments in programs.)  In Burro, however, we'll
strive for better clarity by defining an explicit "no-op" instruction.  For
consistency with the group theory side of things, we'll call it <code>e</code>.
(Of course, we won't forget that <code>e</code> lives in an equivalence class
with other things like <code>+-</code> and the zero-length program, and all
of these things are semantically interchangeable.  But <code>e</code> gives
us a nice, single-symbol, canonical program form when we want to talk about it.)</p>

<p>Now let's consider the basic Brainfuck instructions <code>+</code>, <code>-</code>,
<code>&lt;</code>, and <code>&gt;</code>.  They have a nice, symmetrical
organization that is ideally suited to group structure, so we will adopt them
in our putative Burro design.</p>

<p>On the other hand, the instructions <code>.</code> and <code>,</code> will require
devising some kind of annihilator for interactive input and output.  This seems
difficult at least, and not really necessary if we're willing to forego writing
"Hunt the Wumpus" in Burro, so we'll leave them out for now.  The only input for a
Burro program is, instead, the initial state of the tape, and the only output is the
final state.</p>

<p>In addition, <code>[</code> and <code>]</code> will cause problems, because
as we saw in the introduction, <code>[-]+[]</code> is an infinite loop, and it's
not clear what we could use to annihilate it.  We'll defer this question for later
and for the meantime leave these instructions out, too.</p>

<p>What we're left in our "Burro-in-progress" is essentially a very weak subset of
Brainfuck, with only the five instructions <code>+-&gt;&lt;e</code>.  But this is
a starting point that we can use to see if we're on the right track.  Do the
programs formed from strings of these instructions form a group under concatenation
over the semantic equivalence relation?  i.e.,  Does every Burro program so far
have an inverse?</p>

<p>Let's see.  For every <i>single-instruction</i> Burro
program, we can evidently find another Burro instruction that, when appended to
it, "cancels it out" and makes a program with the same semantics as <code>e</code>:</p>

<table border="1" cellpadding="5">
<tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
<tr><td align="center"><code>+</code></td><td align="center"><code>-</code></td>
    <td align="center"><code>+-</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>-</code></td><td align="center"><code>+</code></td>
    <td align="center"><code>-+</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>&gt;</code></td><td align="center"><code>&lt;</code></td>
    <td align="center"><code>&gt;&lt;</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>&lt;</code></td><td align="center"><code>&gt;</code></td>
    <td align="center"><code>&lt;&gt;</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>e</code></td><td align="center"><code>e</code></td>
    <td align="center"><code>ee</code></td><td align="center"><code>e</code></td></tr>
</table>

<p>Note that we once again should be more explicit about our requirements than
Brainfuck.  We need to have a tape which is infinite in both directions, or else
<code>&lt;</code> wouldn't always be the inverse of <code>&gt;</code> (because sometimes
it'd fail in some way like falling off the edge of the tape.)  And, so that we don't have
to worry about overflow and all that rot,
let's say cells can take on any unbounded negative or positive integer value, too.</p>

<p>But does this hold for <em>any</em> Burro program?  We can use structural
induction to determine this.
Can we find inverses for every Burro program, concatenated with a given
instruction?  (In the following table,
<i>b</i> indicates any Burro program, and <i>b'</i> its inverse.
Also note that <i>bb'</i> is, by definition, <code>e</code>.)</p>

<table border="1" cellpadding="5">
<tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
<tr><td align="center"><code><i>b</i>+</code></td><td align="center"><code>-<i>b'</i></code></td>
    <td align="center"><code><i>b</i>+-<i>b'</i></code><code><i>b</i>e<i>b'</i></code><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code><i>b</i>-</code></td><td align="center"><code>+<i>b'</i></code></td>
    <td align="center"><code><i>b</i>-+<i>b'</i></code><code><i>b</i>e<i>b'</i></code><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code><i>b</i>&gt;</code></td><td align="center"><code>&lt;<i>b'</i></code></td>
    <td align="center"><code><i>b</i>&gt;&lt;<i>b'</i></code><code><i>b</i>e<i>b'</i></code><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code><i>b</i>&lt;</code></td><td align="center"><code>&gt;<i>b'</i></code></td>
    <td align="center"><code><i>b</i>&lt;&gt;<i>b'</i></code><code><i>b</i>e<i>b'</i></code><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code><i>b</i>e</code><code><i>b</i></code></td><td align="center"><code>e<i>b'</i></code><code><i>b'</i>e</code><code><i>b'</i></code></td>
    <td align="center"><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
</table>

<p>Looks good.  However, this isn't an abelian group, and concatenation is definately not
commutative.  So, to be complete, we need a table going in the other direction, too: concatenation of a
given instruction with any Burro program.</p>

<table border="1" cellpadding="5">
<tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
<tr><td align="center"><code>+<i>b</i></code></td><td align="center"><code><i>b'</i>-</code></td>
    <td align="center"><code>+<i>bb'</i>-</code><code>+e-</code><code>+-</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>-<i>b</i></code></td><td align="center"><code><i>b'</i>+</code></td>
    <td align="center"><code>-<i>bb'</i>+</code><code>-e+</code><code>-+</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>&gt;<i>b</i></code></td><td align="center"><code><i>b'</i>&lt;</code></td>
    <td align="center"><code>&gt;<i>bb'</i>&lt;</code><code>&gt;e&lt;</code><code>&gt;&lt;</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>&lt;<i>b</i></code></td><td align="center"><code><i>b'</i>&gt;</code></td>
    <td align="center"><code>&lt;<i>bb'</i>&gt;</code><code>&lt;e&gt;</code><code>&lt;&gt;</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>e<i>b</i></code><code><i>b</i></code></td><td align="center"><code><i>b'</i>e</code><code>e<i>b'</i></code><code><i>b'</i></code></td>
   <td align="center"><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
</table>

<p>So far, so good, I'd say.  Now we can address to the problem of how to
restrengthen the language so that it remains as powerful as Brainfuck.</p>

<h3>Loops</h3>

<p>Obviously, in order for Burro to be as capable as Brainfuck,
we would like to see some kind of looping mechanism in it. But, as we've
seen, Brainfuck's is insufficient for our purposes, because it allows for
the construction of infinite loops that we can't invert by concatenation.</p>

<p>We could insist that all loops be finite, but that would make
Burro less powerful than Brainfuck — it would only be capable of expressing
the primitive recursive functions.  The real challenge is in having Burro be Turing-complete,
like Brainfuck.</p>

<p>This situation looks dire, but there turns out to be a way.  What we
do is borrow the trick used in languages like L00P and Version (and probably
many others.)  We put a single, implicit loop around the whole program.
(There is a classic formal proof that this is sufficient — the interested
reader is referred to the paper "Kleene algebra with tests"<sup><a href="#1">1</a></sup>,
which gives a brief history, references, and its own proof.)</p>

<p>This single implicit loop will be conditional on a special flag, which
we'll call the "halt flag", and we'll stipulate is initially set.
If this flag is still set when the end of the program is reached, the program halts.
But if it is unset when the end of the program is reached, the flag is reset
and the program repeats from the beginning.  (Note that although the halt flag
is reset, all other program state (i.e. the tape) is left alone.)</p>

<p>To manipulate this flag, we introduce a new instruction:</p>

<table border="1" cellpadding="5">
<tr><th>Instruction</th><th>Semantics</th></tr>
<tr><td align="center"><code>!</code></td><td>Toggle halt flag</td></tr>
</table>

<p>Then we check that adding this instruction to Burro's instruction set
doesn't change the fact that Burro programs form a group:</p>

<table border="1" cellpadding="5">
<tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
<tr><td align="center"><code>!</code></td><td align="center"><code>!</code></td>
    <td align="center"><code>!!</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code>!<i>b</i></code></td><td align="center"><code><i>b'</i>!</code></td>
    <td align="center"><code>!<i>bb'</i>!</code><code>!e!</code><code>!!</code></td><td align="center"><code>e</code></td></tr>
<tr><td align="center"><code><i>b</i>!</code></td><td align="center"><code>!<i>b'</i></code></td>
    <td align="center"><code><i>b</i>!!<i>b'</i></code><code><i>beb'</i></code><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
</table>

<p>Seems so.  Now we can write Burro programs that halt, and Burro programs that loop
forever.  What we need next is for the program to be able to decide this behaviour
for itself.</p>

<h3>Conditionals</h3>

<p>OK, this is the ugly part.</p>

<p>Let's add a simple control structure to Burro.  Since we already have repetition, this
will only be for conditional execution.  To avoid confusion with Brainfuck, we'll avoid <code>[]</code>
entirely; instead, we'll use <code>()</code>
to indicate "execute the enclosed code (once) if and only if the current cell is non-zero".</p>

<p>Actually, let's make it a bit fancier, and allow an "else" clause to be inserted in it,
like so: <code>(/)</code> where the code before the <code>/</code> is executed iff the cell
is non-zero, and the code after the <code>/</code> is executed iff it is zero.</p>

<p>(The reasons for this design choice are subtle.  They come down to the fact that
in order to find an inverse of a conditional, we need to invert the sense of the test.
In a higher-level language, we could use a Boolean NOT operation for this.  However, in
Brainfuck, writing a NOT requires a loop, and thus a conditional.  Then we're stuck
with deciding how to invert the sense of <em>that</em> conditional, and so forth.  By
providing NOT-like behaviour as a built-in courtesy of <code>/</code>, we dodge the
problem entirely.  If you like, you can think of it as meeting the aesthetic demands of
a symmetrical language: the conditional structures are symmetrical too.)</p>

<p>A significant difference here with Brainfuck is that, while Brainfuck is a bit
lacksidaisical about matching up <code>[</code>'s with <code>]</code>'s, we explicitly
<em>disallow</em> parentheses that do not nest correctly in Burro.  A Burro program with mismatched
parentheses is an ill-formed Burro program, and thus not really a Burro program at all.
We turn up our nose at it; we aren't even interested in whether we can find an
inverse of it, because we don't acknowledge it.  This applies to the placement of
<code>/</code> outside of parentheses, or the absence of <code>/</code> in parentheses,
as well.</p>

<p>(The reasons for this design choice are also somewhat subtle.  I originally wanted
to deal with this by saying that <code>(</code>, <code>/</code>, and <code>)</code>
could come in any order, even a nonsensical one, and still make a valid Burro program,
only with the semantics of "no-op" or "loop forever" or something equally representative of
"broken."  You see this quite often in toy formal languages, and the resulting lack of
syntax would seem to allow the set of Burro instructions to be a "free generator" of
the group of Burro programs, which sounds like it might have very nice
abstract-algebraical properties.
The problem is that it potentially interferes with the whole "finding an
antiprogram" thing.  If a Burro program with mismatched parentheses has the
semantics of "no-op", then every Burro program has a trivial annihilator: just
tack on an unmatching parenthesis.  Similarly, if malformed programs are
considered to loop forever, how do you invert them?  So, for these reasons,
Burro has some small amount of syntax — a bit more than Brainfuck is usually
considered to have, but not much.)</p>

<p>Now, it turns out we will have to do a fair bit of work on <code>()</code> in order
to make it so that we can always find a bit of code that is the inverse of some other
bit of code that includes <code>()</code>.</p>

<p>We can't just make it a "plain old if", because by the time we've finished executing an "if",
we don't know which branch was executed — so we have no idea what the "right"
inverse of it would be.  For example,</p>

<ul><li><code>(-/e)</code></li></ul>

<p>After this has finished executing, the current cell could contain 0 - but is that because it
was already 0 before the <code>(</code> was encountered, and nothing happened to it
inside the "if"... or is it because it was 1 before
the <code>(</code> was encountered, and decremented to 0 by the <code>-</code>
instruction inside the "if"?
It could be either, and we don't know — so we can't find an inverse.</p>

<p>We remedy this in a somewhat disappointingly uninteresting way: we make a copy of
the value being tested and squirrel it away for future reference, so that pending code
can look at it and tell what decision was made, and in so doing, act appropriately to
invert it.</p>

<p>This information that we squirrel away is, I would say, a kind of <em>continuation</em>.
It's not a full-bodied continuation, as the term continuation is often used, in the
sense of "function representing the entire remainder of the computation."
But, it's a bit of context that is retained during execution that is intended to affect
some future control flow decision — and that's the basic purpose of a continuation.
So, I will call it a continuation, although it is perhaps a diminished sort of continuation.
(In this sense, the machine stack where arguments and
return addresses are stored in a language like C is also a kind of continuation.)</p>

<p>These continuations that we maintain, these pieces of information that tell us how
to undo things in the future, do need to have an orderly relationship with each other.
Specifically, we need to remember to undo the more recent conditionals first.  So, we
retain the continuations in a FIFO discipline, like a stack.  Whenever a <code>(</code> is
executed, we "push" a continuation into storage, and when we need to invert the effect
of a previous conditional, we "pop" a continuation from storage.</p>

<p>To actually accomplish this latter action we need to define the control structure
for undoing conditional tests.  We introduce the construct
<code>{\}</code>, which works just like <code>(/)</code>, except that the value that it tests
doesn't come from the tape — instead, it comes from the continuation.  We establish similar
syntactic rules about matching every <code>{</code> with a <code>}</code> and an
intervening <code>\</code>, in addition to a rule that says every <code>{\}</code>
must be preceded by a <code>(/)</code>.</p>

<p>With this, we're very close to having an inverse for conditionals.  Consider:</p>

<ul><li><code>(-/e){+\e}</code></li></ul>

<p>If the current cell contains 0 after <code>(-/e)</code>, the continuation will contain either
a 1 or a 0 (the original contents of the cell.)  If the continuation contains a 0, the "else" part of
<code>{+\e}</code> will be executed — i.e. nothing will happen.  On the other hand, if the
continuation contains a 1, the "then" part of <code>{+\e}</code> will be executed.
Either way, the tape is correctly restored to its original (pre-<code>(-/e)</code>) state.</p>

<p>There are still a few details to clean up, though.
Specifically, we need to address nesting.  What if we're given</p>

<ul><li><code>(&gt;(&lt;+/e)/e)</code></li></ul>

<p>How do we form an inverse of this?  How would the following work?</p>

<ul><li><code>(&gt;(&lt;+/e)/e){{-&gt;\e}&lt;\e}</code></li></ul>

<p>The problem with this, if we collect continuations using only a naive stack arrangement,
is that we don't remember how many times a <code>(</code> was encountered before a
matching <code>)</code>.  The retention of continuations is still FIFO, but we need
more control over the relationships between the continuations.</p>

<p>The nested structure of the <code>(/)</code>'s suggests a nested structure
for collecting continuations.  
Whenever we encounter a <code>(</code> and we "push" a continuation into storage,
that continuation becomes the root for a new collection of continuations
(those that occur <em>inside</em> the present conditional, up to the matching
<code>)</code>.)  Since each continuation is both part of some FIFO series of
continuations, and has the capacity to act as the root of it's <em>own</em> FIFO series
of continuations, the continuations are arranged in a structure that is
more a binary tree than a stack.</p>

<p>This is perhaps a little complicated, so I'll summarize it in this table.
Since this is a fairly operational description, I'll use the term "tree node"
instead of continuation to help you visualize it.  Keep in mind that at any
given time there is a "current continuation" and thus a current tree node.</p>

<table border="1" cellpadding="5">
<tr><th>Instruction</th><th>Semantics</th></tr>
<tr><td align="center"><code>(</code></td><td>
<ul>
<li>Create a new tree node with the contents of the current cell</li>
<li>Add that new node as a child of the current node</li>
<li>Make that new node the new current node</li>
<li>If the current cell is zero, skip one instruction past the matching <code>/</code></li>
</ul>
</td></tr>
<tr><td align="center"><code>/</code></td><td>
<ul>
<li>Skip to the matching <code>)</code></li>
</ul>
</td></tr>
<tr><td align="center"><code>)</code></td><td>
<ul>
<li>Make the parent of the current node the new current node</li>
</ul>
</td></tr>
<tr><td align="center"><code>{</code></td><td>
<ul>
<li>Make the most recently added child of the current node the new current node</li>
<li>If the value of the current node is zero, skip one instruction past the matching <code>\</code></li>
</ul>
</td></tr>
<tr><td align="center"><code>\</code></td><td>
<ul>
<li>Skip to the matching <code>}</code></li>
</ul>
</td></tr>
<tr><td align="center"><code>}</code></td><td>
<ul>
<li>Make the parent of the current node the new current node</li>
<li>Remove the old current node and all of its children</li>
</ul>
</td></tr>
</table>

<p>Now, keeping in mind that the continuation structure
remains constant across all Burro programs equivalent to <code>e</code>,
we can show that control structures have inverses:</p>

<table border="1" cellpadding="5">
<tr><th>Instruction</th><th>Inverse</th><th>Test result</th><th>Concatenation</th><th>Net effect</th></tr>
<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>
    <td align="center">zero</td><td align="center"><code><i>acdd'c'a'</i></code><code><i>acc'a'</i></code><code><i>aa'</i></code></td><td align="center"><code>e</code></td></tr>
<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>
    <td align="center">non-zero</td><td align="center"><code><i>abdd'b'a'</i></code><code><i>abb'a'</i></code><code><i>aa'</i></code></td><td align="center"><code>e</code></td></tr>
</table>

<p>There you have it: every Burro program has an inverse.</p>

<h2>4. Implementations</h2>

<p>There are two reference interpreters for Burro.  <code>burro.c</code> is
written in ANSI C, and <code>burro.hs</code> is written in Haskell.
Both are BSD licensed.
Hopefully at least one of them is faithful to the execution model.</p>

<h3><code>burro.c</code></h3>

<p>The executable produced by compiling <code>burro.c</code> takes the
following command-line arguments:</p>

<ul><li><code>burro [-d] srcfile.bur</code></li></ul>

<p>The named file is loaded as Burro source code.  All characters in this file except for
<code>&gt;&lt;+-(/){\}e!</code> are ignored.</p>

<p>Before starting the run, the interpreter will read a series of whitespace-separated
integers from standard input.  These integers
are placed on the tape initially, starting from the head-start position, extending right.
All unspecified cells are considered to contain 0 initially.</p>

<p>When the program has halted, all tape cells that were "touched" — either given initially as
part of the input, or passed over by the tape head — are output to standard output.</p>

<p>The meanings of the flags are as follows:</p>

<ul>
<li>The <code>-d</code> flag causes debugging information to be sent to standard error.</li>
</ul>

<p>The C implementation performs no syntax-checking.  It approximates the unbounded Burro tape
with a tape of finite size (defined by <code>TAPE_SIZE</code>, by default 64K) with
cells each capable of containing a C language <code>long</code>.</p>

<h3><code>burro.hs</code></h3>

<p>The Haskell version of the reference implementation is meant to be executed from
within an interactive Haskell environment, such as Hugs.  As such, there is no
command-line syntax; the user simply invokes the function <code>burro</code>,
which has the signature <code>burro :: String -&gt; Tape -&gt; Tape</code>.
A convenience constructor <code>tape :: [Integer] -> Tape</code> creates a tape
from the given list of integers, with the head positioned over the leftmost cell.</p>

<p>The Haskell implementation performs no syntax-checking. Because Haskell supports
unbounded lists and arbitrary-precision integers, the Burro tape is modelled faithfully.</p>

<h2>Discussion</h2>

<p>I hadn't intended to come up with anything in particular when I started
designing Burro.  I'm hardly a mathematician, and I didn't know anything
about abstract algebra except that I found it intriguing.  I suppose that algebraic
structures have some of the same appeal as programming languages, what with
both dealing with primitive operators, equivalent expression forms, and so forth.</p>

<p>I was basically struck by the variety of objects that could be shown to have
this or that algebraic structure, and I wanted to see how well it would
hold up if you tried to apply these structures to programs.</p>

<p>Why groups?  Well, the original design goal for Burro was actually to create a Brainfuck-like language 
where the set of possible programs forms the most <em>restricted</em>
possible magma (i.e. the one with the most additional axioms) under concatenation.  It can
readily been seen that the set of Brainfuck programs forms a semigroup,
even a monoid, under concatenation (left as an exercise for the interested
reader.)  At the other extreme, if the set of programs forms an abelian group under
concatenation, the language probably isn't going to be very Brainfuck-like
(since insisting that concatenation be commutative is tantamount to saying
that the order of instructions in a program doesn't matter.)
This leaves a group as the reasonable target to aim for, so that's what I
aimed for.</p>

<p>But the end result turns out to be related to <em>reversible computing</em>.
This shouldn't have been a surprise, since groups are one of the simplest
foundations for modelling symmetry; it should have been obvious to me that trying to
make programs conform to them, would make them (semantically) symmetrical, and
thus reversible.  But, it wasn't.</p>

<p>We may ask: in what sense is Burro reversible?  And we may compare it
to other esolangs in an attempt to understand.</p>

<p>Well, it's not reversible in the sense that 
<a href="http://esolangs.org/wiki/Befreak">Befreak</a> is reversible —
you can't pause it at any point, change the direction of execution, and watch it
"go backwards".  Specifically, you can't "undo" a loop in Burro by executing
20 iterations, then turning around and "un-executing" those 20 iterations; instead,
you "undo" the loop by neutralizing the toggling of the halt flag.  With this approach,
inversion is instead <em>like the loop never existed in the first place</em>.</p>

<p>If one did want to make a Brainfuck-like language which was reversible more in
the sense that Befreak is reversible, one approach might be to add rules like
"<code>+</code> acts like <code>-</code> if the program counter is incoming from
the right". But, I haven't pondered on this approach much at all.</p>

<p>Conversely, the concatenation concept doesn't have a clear
correspondence in a two-dimensional language like Befreak — how do you put two programs
next to each other?  Side-by-side, top-to-bottom?  You would probably need multiple
operators, which would definately complicate things.</p>

<p>It's also not reversible in the same way that
<a href="http://esolangs.org/wiki/Kayak">Kayak</a> is reversible —
Burro programs need not be palindromes, for instance.  In fact, I specifically made
the "then" and "else" components of both <code>(/)</code> and <code>{\}</code>
occur in the same order, so as to break the reflectional symmetry somewhat, and
add some translational similarity.</p>

<p>Conversely, Kayak doesn't cotton to concatenation too well either.
In order to preserve the palindrome nature, concatenation would have to
occur both at the beginning and the end simultaneously.
I haven't given this idea much thought, and I'm not sure where it'd get you.</p>

<p>Lastly, we could go outside the world of esolangs and use the
definition of reversible computing given by Mike Frank<sup><a href="#2">2</a></sup>:</p>

<blockquote><p>When we say reversible computing, we mean performing computation
in such a way that any previous state of the computation can always be reconstructed
given a description of the current state.</p></blockquote>

<p>Burro appears to qualify by this definition — <em>almost</em>.  The requirement
that we can reconstruct <em>any</em> previous state is a bit heavy.  We can definately
reconstruct states up to the start of the last loop iteration, if we want to, due to the mechanism
(continuations) that we've defined to remember what the program state was before any given
conditional.</p>

<p>But what about <em>before</em> the last loop iteration?  Each time we reach the end
of the program text with halt flag unset, we repeat execution from the beginning, and
when this happens, there might still be one or more continuations in storage that were the
result of executing <code>(/)</code>'s that did not have
matching <code>{\}</code>'s.</p>

<p>We didn't say what happens to these "leftover" continuations.  In fact, computationally
speaking, it doesn't matter: since syntactically no
<code>{\}</code> can precede any <code>(/)</code>, those leftover continuations
couldn't actually have any affect during the next iteration.  Any <code>{\}</code> that
might consume them next time 'round must be preceded by a <code>(/)</code> which will
produce one for it to consume instead.</p>

<p>And indeed, discarding any continuation that remains when a Burro program loops
means that continuations need occupy only a bounded amount of space during execution (because there
is only a fixed number of conditionals in any given Burro program.)  This
is a desirable thing in a practical implementation, and
both the C and Haskell reference implementations do just this.</p>

<p>But this is an implementation choice, and it would be equally valid to write an interpreter
which retains all these leftover continuations.  And such an interpreter would qualify as a
reversible computer under Mike Frank's definition, since these continuations would allow one
to reconstruct the entire computation history of the program.</p>

<p>On this last point, it's interesting to note the similarity between Burro's continuations
and Kayak's bit bucket.  Although Burro continuations record the value tested, they really
don't <em>need</em> to; they <em>could</em> just
contain bits indicating whether the tests were successes or failures.  Both emptying
the bit bucket, and discarding continuations, results in a destruction of information that
prevents reversibility (and thermodynamically "generates heat") but allows for a limit on the amount of
storage required.</p>

<h2>History</h2>

<p>I began formulating Burro in the summer of 2005.
The basic design of Burro was finished by winter of 2005, as was the C implementation.
But its release was delayed for several reasons.  Mainly, I was busy with other (ostensibly more
important) things, like schoolwork.  However, I also had the nagging feeling that certain parts of
the language were not quite described correctly.  These doubts led me to introduce the
concept of a group over an equivalence relation, and to decide that Burro needed
real syntax rules (lest inverting a Burro program was "too easy.")  So it wasn't until spring of 2007
that I had a general description that I was satisfied with.
I also wanted a better reference implementation, in something a bit more abstract and
rigorous than C. So I wrote the Haskell version over the summer of 2007.</p>

<p>In addition, part of me wanted to write a publishable paper on Burro.
After all, group theory and reversible computing are valid and relatively mainstream
research topics, so why not?  But in the end, considering doing this was really a
waste of my time.  Densening my writing style to conform to acceptable academic
standards of impermeability, and puffing up my "discovery" to acceptable academic
standards of self-importance, really didn't appeal to me.  There's no sense pretending,
in high-falutin' language, that Burro represents some profound advance in human
knowledge.  It's just something neat that I built!  And in the end it seemed
just as valuable, if not moreso, to try to turn esolangers on to group theory than
to turn academics on to Brainfuck...</p>

<p>Happy annihilating!</p>

<p>-Chris Pressey
<br/>Cat's Eye Technologies
<br/>October 26, 2007
<br/>Windsor, Ontario, Canada</p>

<h2>Footnotes</h2>

<ul>
<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
Systems</i>, 19(3):427-443, May 1997.</li>
<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>

</ul>

</body></html>