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