git @ Cat's Eye Technologies Burro / rel_2_0_2011_0525
Import of Burro version 2.0 revision 2011.0525 sources. Cat's Eye Technologies 8 years ago
4 changed file(s) with 69 addition(s) and 67 deletion(s). Raw diff Collapse all Expand all
00 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
1 <!-- encoding: UTF-8 -->
12 <html xmlns="http://www.w3.org/1999/xhtml" lang="en">
23 <head>
34 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
2526 But the first version is close enough for jazz, and rolls off the tongue more easily...)</p>
2627
2728 <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 an <em>antiprogram</em> — a series of instructions that can be appended to it
2930 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 same semantics as no program at all — a "no-op," or a zero-length program.</p>
3132
3233 <p>Why is this at all remarkable? Well, take the Brainfuck program fragment <code>[-]+[]</code>.
3334 What could you append to it to it to make it into a "no-op" program?
5152
5253 <p>Recall (or go look up in an abstract algebra textbook) that a <em>group</em> is
5354 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 · : <var>S</var> × <var>S</var> → <var>S</var>
5556 that obeys the following three axioms:</p>
5657
5758 <ul>
5859
5960 <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,
61 the set <var>S</var>, (<var>a</var> · <var>b</var>) · <var>c</var> =
62 <var>a</var> · (<var>b</var> · <var>c</var>). In other words,
6263 the operation is "associative." Parentheses don't matter, and we generally leave them out.</li>
6364
6465 <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 <var>a</var> · <b>e</b> = <b>e</b> · <var>a</var> = <var>a</var>
6667 for every element <var>a</var> of <var>S</var>. Think of
6768 <b>e</b> as a "neutral" element that just doesn't contribute anything.</li>
6869
6970 <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 <var>a'</var> of <var>S</var> such that <var>a</var> · <var>a'</var> = <b>e</b>.
7172 That is, for any element, you can find some element that "annihilates" it.</li>
7273
7374 </ul>
7475
75 <p>There are lots of examples of groups &mdash; the integers under the operation of
76 <p>There are lots of examples of groups — the integers under the operation of
7677 addition, for example, where <b>e</b> is 0, and the annihilator for any integer
7778 is simply its negative (because <var>x</var> + (-<var>x</var>) always equals 0.)</p>
7879
7980 <p>There are also lots of things you can prove are true about any group
8081 (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
82 <var>a</var> · <var>x</var> = <var>a</var> and
83 <var>a</var> · <var>y</var> = <var>a</var> then
8384 <var>x</var> = <var>y</var> = <b>e</b>. (This particular property will
8485 become relevant very soon, so keep it in mind as you read the next section.)</p>
8586
107108 <p>This distinction becomes important with respect to treating programs
108109 as elements of a group, like we're doing in Burro. Some program will
109110 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
111 be equivalent to this program — in which case <b>e</b> is not unique, contrary to
112 what group theory tells us — or we are talking about abstract programs
112113 independent of any programming language, in which case our goal of defining a particular
113114 language called "Burro" for this purpose seems a bit futile.</p>
114115
125126 <p>To this end, let's examine the idea of a <em>group over an equivalence relation</em>.
126127 All this is, really, is being specific about what constitutes "equals" in those
127128 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 an <em>equivalence relation</em> — a relationship between elements
129130 which paritions a set into
130131 disjoint equivalence classes, where every element in a class is considered
131132 equivalent to every other element in that same class (and inequivalent to any
153154 interchangably with respect to the group axioms.</p>
154155
155156 <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 is a triple 〈<var>S</var>,·,≡〉 where:</p>
157158 <ul>
158159 <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>
160 <li>· : <var>S</var> × <var>S</var> → <var>S</var> is a binary operation over <var>S</var></li>
161 <li>≡ is a reflexive, transitive, and symmetrical binary relation over <var>S</var></li>
161162 </ul>
162163 <p>where the following axioms are also satisfied:</p>
163164 <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>
165 <li>∀ <var>a</var>, <var>b</var>, <var>c</var> ∈ <var>S</var>: (<var>a</var> · <var>b</var>) · <var>c</var> ≡
166 <var>a</var> · (<var>b</var> · <var>c</var>)</li>
167 <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>
168 <li>∀ <var>a</var> ∈ <var>S</var>: ∃ <var>a'</var> ∈ <var>S</var>: <var>a</var> · <var>a'</var> ≡ <b>e</b></li>
168169 </ul>
169170
170171 <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 to a group over an equivalence relation: just replace = with ≡. So what
172173 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 equivalence class <b>E</b> ⊆ <var>S</var> that contains it is:
174175 <b>E</b> is the only equivalence class that contains
175176 elements like <b>e</b> and, for the purposes of the group, all of these elements are
176177 interchangeable.</p>
253254 <table border="1" cellpadding="5">
254255 <tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
255256 <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 <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>
257258 <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 <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>
259260 <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 <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>
261262 <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>
263 <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>
264 <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>
264265 <td align="center"><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
265266 </table>
266267
271272 <table border="1" cellpadding="5">
272273 <tr><th>Instruction</th><th>Inverse</th><th>Concatenation</th><th>Net effect</th></tr>
273274 <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 <td align="center"><code>+<i>bb'</i>-</code> ≡ <code>+e-</code> ≡ <code>+-</code></td><td align="center"><code>e</code></td></tr>
275276 <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 <td align="center"><code>-<i>bb'</i>+</code> ≡ <code>-e+</code> ≡ <code>-+</code></td><td align="center"><code>e</code></td></tr>
277278 <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 <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>
279280 <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>
281 <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>
282 <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>
282283 <td align="center"><code><i>bb'</i></code></td><td align="center"><code>e</code></td></tr>
283284 </table>
284285
293294 the construction of infinite loops that we can't invert by concatenation.</p>
294295
295296 <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 Burro less powerful than Brainfuck — it would only be capable of expressing
297298 the primitive recursive functions. The real challenge is in having Burro be Turing-complete,
298299 like Brainfuck.</p>
299300
300301 <p>This situation looks dire, but there turns out to be a way. What we
301302 do is borrow the trick used in languages like L00P and Version (and probably
302303 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 (There is a classic formal proof that this is sufficient — the interested
304305 reader is referred to the paper "Kleene algebra with tests"<sup><a href="#1">1</a></sup>,
305306 which gives a brief history, references, and its own proof.)</p>
306307
326327 <tr><td align="center"><code>!</code></td><td align="center"><code>!</code></td>
327328 <td align="center"><code>!!</code></td><td align="center"><code>e</code></td></tr>
328329 <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 <td align="center"><code>!<i>bb'</i>!</code> ≡ <code>!e!</code> ≡ <code>!!</code></td><td align="center"><code>e</code></td></tr>
330331 <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 <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>
332333 </table>
333334
334335 <p>Seems so. Now we can write Burro programs that halt, and Burro programs that loop
379380 semantics of "no-op", then every Burro program has a trivial annihilator: just
380381 tack on an unmatching parenthesis. Similarly, if malformed programs are
381382 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 Burro has some small amount of syntax — a bit more than Brainfuck is usually
383384 considered to have, but not much.)</p>
384385
385386 <p>Now, it turns out we will have to do a fair bit of work on <code>()</code> in order
387388 bit of code that includes <code>()</code>.</p>
388389
389390 <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 we don't know which branch was executed — so we have no idea what the "right"
391392 inverse of it would be. For example,</p>
392393
393394 <ul><li><code>(-/e)</code></li></ul>
397398 inside the "if"... or is it because it was 1 before
398399 the <code>(</code> was encountered, and decremented to 0 by the <code>-</code>
399400 instruction inside the "if"?
400 It could be either, and we don't know &mdash; so we can't find an inverse.</p>
401 It could be either, and we don't know — so we can't find an inverse.</p>
401402
402403 <p>We remedy this in a somewhat disappointingly uninteresting way: we make a copy of
403404 the value being tested and squirrel it away for future reference, so that pending code
408409 It's not a full-bodied continuation, as the term continuation is often used, in the
409410 sense of "function representing the entire remainder of the computation."
410411 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 some future control flow decision — and that's the basic purpose of a continuation.
412413 So, I will call it a continuation, although it is perhaps a diminished sort of continuation.
413414 (In this sense, the machine stack where arguments and
414415 return addresses are stored in a language like C is also a kind of continuation.)</p>
423424 <p>To actually accomplish this latter action we need to define the control structure
424425 for undoing conditional tests. We introduce the construct
425426 <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 doesn't come from the tape — instead, it comes from the continuation. We establish similar
427428 syntactic rules about matching every <code>{</code> with a <code>}</code> and an
428429 intervening <code>\</code>, in addition to a rule that says every <code>{\}</code>
429430 must be preceded by a <code>(/)</code>.</p>
434435
435436 <p>If the current cell contains 0 after <code>(-/e)</code>, the continuation will contain either
436437 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 <code>{+\e}</code> will be executed — i.e. nothing will happen. On the other hand, if the
438439 continuation contains a 1, the "then" part of <code>{+\e}</code> will be executed.
439440 Either way, the tape is correctly restored to its original (pre-<code>(-/e)</code>) state.</p>
440441
513514 <table border="1" cellpadding="5">
514515 <tr><th>Instruction</th><th>Inverse</th><th>Test result</th><th>Concatenation</th><th>Net effect</th></tr>
515516 <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 <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>
517518 <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 <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>
519520 </table>
520521
521522 <p>There you have it: every Burro program has an inverse.</p>
542543 are placed on the tape initially, starting from the head-start position, extending right.
543544 All unspecified cells are considered to contain 0 initially.</p>
544545
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>
546 <p>When the program has halted, all tape cells that were "touched" — either given initially as
547 part of the input, or passed over by the tape head — are output to standard output.</p>
547548
548549 <p>The meanings of the flags are as follows:</p>
549550
601602 to other esolangs in an attempt to understand.</p>
602603
603604 <p>Well, it's not reversible in the sense that
604 <a href="http://esolangs.org/wiki/Befreak">Befreak</a> is reversible &mdash;
605 <a href="http://esolangs.org/wiki/Befreak">Befreak</a> is reversible —
605606 you can't pause it at any point, change the direction of execution, and watch it
606607 "go backwards". Specifically, you can't "undo" a loop in Burro by executing
607608 20 iterations, then turning around and "un-executing" those 20 iterations; instead,
614615 the right". But, I haven't pondered on this approach much at all.</p>
615616
616617 <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 correspondence in a two-dimensional language like Befreak — how do you put two programs
618619 next to each other? Side-by-side, top-to-bottom? You would probably need multiple
619620 operators, which would definately complicate things.</p>
620621
621622 <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 <a href="http://esolangs.org/wiki/Kayak">Kayak</a> is reversible —
623624 Burro programs need not be palindromes, for instance. In fact, I specifically made
624625 the "then" and "else" components of both <code>(/)</code> and <code>{\}</code>
625626 occur in the same order, so as to break the reflectional symmetry somewhat, and
637638 in such a way that any previous state of the computation can always be reconstructed
638639 given a description of the current state.</p></blockquote>
639640
640 <p>Burro appears to qualify by this definition &mdash; <em>almost</em>. The requirement
641 <p>Burro appears to qualify by this definition — <em>almost</em>. The requirement
641642 that we can reconstruct <em>any</em> previous state is a bit heavy. We can definately
642643 reconstruct states up to the start of the last loop iteration, if we want to, due to the mechanism
643644 (continuations) that we've defined to remember what the program state was before any given
00 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
1 <!-- encoding: UTF-8 -->
12 <html xmlns="http://www.w3.org/1999/xhtml" lang="en">
23 <head>
34 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
1617 the operation of concatenation and over the equivalence relation of "computes
1718 the same function." This means that, for every Burro program, we can
1819 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 program, results in a "no-op" program (a program with no effect — the
2021 identity function.)</p>
2122
2223 <p>(In fact, for every set of Burro programs that compute the same function,
324325 <p>(a/b) is the conditional construct, which is quite special.</p>
325326
326327 <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 of this construct — let's call it x.</p>
328329
329330 <p>Second, the current data cell and the current stack cell are swapped.</p>
330331
355356 </code></pre>
356357
357358 <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 stack tape, and because it does so in a monotonic way — that is, both a
359360 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 right of what (a/b) has access to — the current stack cell in step seven
361362 always holds the same value as the current stack cell in step two, except
362363 negated.</p>
363364
458459 is negated, so becomes -x &lt; 0. The stack head is moved to the right.</p>
459460
460461 <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 The current data cell could be anything — call it k'.</p>
462463
463464 <p>The stack head is moved back to the left, so that the current stack
464465 cell is once again -x &lt; 0, and it is swapped with the current data
480481 cell is once again x > 0, and it is swapped with the current data
481482 cell, making it x and making the current stack cell k. This is
482483 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 <li><p>Case 3 is an exact mirror image of case 2 — the only difference
484485 is that the first time through, x &lt; 0 and b is evaluated, thus the
485486 second time through, -x > 0 and b' is evaluated. Therefore
486487 (a/b)(b'/a') ≡ e in this instance as well.</p></li>
581582 <p>T if executed if x = 1 and F is executed otherwise. (Remember,
582583 we're assuming x is odd and positive.) To make the idiom hold, we
583584 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>
585 position they found it. If you are wondering where the zero came
586 from — it came from the stack.</p>
586587
587588 <p>We now note that this idiom can be nested to detect larger odd
588589 numbers. For example, to determine if x is 1 or 3 or 5:</p>
1515 } elsif ($line =~ /^\>(.*?)$/) {
1616 print OUTFILE " $1\n";
1717 } else {
18 $line =~ s/\s\-\-\s/ \&mdash\; /g;
1918 print OUTFILE "$line\n";
2019 }
2120 }
3029
3130 print OUTFILE <<"EOH";
3231 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
32 <!-- encoding: UTF-8 -->
3333 <html xmlns="http://www.w3.org/1999/xhtml" lang="en">
3434 <head>
3535 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
1212 the operation of concatenation and over the equivalence relation of "computes
1313 the same function." This means that, for every Burro program, we can
1414 construct a corresponding antiprogram that, when appended onto the first
15 program, results in a "no-op" program (a program with no effect -- the
15 program, results in a "no-op" program (a program with no effect — the
1616 identity function.)
1717
1818 (In fact, for every set of Burro programs that compute the same function,
315315 (a/b) is the conditional construct, which is quite special.
316316
317317 First, the current data cell is remembered for the duration of the execution
318 of this construct -- let's call it x.
318 of this construct — let's call it x.
319319
320320 Second, the current data cell and the current stack cell are swapped.
321321
345345 > (State dat'''' stack'''' halt')
346346
347347 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
348 stack tape, and because it does so in a monotonic way — that is, both a
349349 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
350 right of what (a/b) has access to — the current stack cell in step seven
351351 always holds the same value as the current stack cell in step two, except
352352 negated.
353353
457457 is negated, so becomes -x < 0. The stack head is moved to the right.
458458
459459 Because x > 0, the first of the sub-programs, a, is now evaluated.
460 The current data cell could be anything -- call it k'.
460 The current data cell could be anything — call it k'.
461461
462462 The stack head is moved back to the left, so that the current stack
463463 cell is once again -x < 0, and it is swapped with the current data
480480 cell, making it x and making the current stack cell k. This is
481481 the state we started from, so (a/b)(b'/a') ≡ e.
482482
483 3. Case 3 is an exact mirror image of case 2 -- the only difference
483 3. Case 3 is an exact mirror image of case 2 — the only difference
484484 is that the first time through, x < 0 and b is evaluated, thus the
485485 second time through, -x > 0 and b' is evaluated. Therefore
486486 (a/b)(b'/a') ≡ e in this instance as well.
577577 T if executed if x = 1 and F is executed otherwise. (Remember,
578578 we're assuming x is odd and positive.) To make the idiom hold, we
579579 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.
580 position they found it. If you are wondering where the zero came
581 from — it came from the stack.
582582
583583 We now note that this idiom can be nested to detect larger odd
584584 numbers. For example, to determine if x is 1 or 3 or 5: