git @ Cat's Eye Technologies Burro / rel_2_0_2012_0619
Remove obsolete files. Cat's Eye Technologies 8 years ago
3 changed file(s) with 0 addition(s) and 758 deletion(s). Raw diff Collapse all Expand all
+0
-686
doc/burro.html less more
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, v2.0</title>
6 <link rel="stylesheet" type="text/css" href="markdown-lhs.css" />
7 </head>
8 <body>
9 <h1>The Burro Programming Language</h1>
10
11 <p>Version 2.0
12 June 2010, Chris Pressey, Cat's Eye Technologies</p>
13
14 <h2>Introduction</h2>
15
16 <p>Burro is a programming language whose programs form an algebraic group under
17 the operation of concatenation and over the equivalence relation of "computes
18 the same function." This means that, for every Burro program, we can
19 construct a corresponding antiprogram that, when appended onto the first
20 program, results in a "no-op" program (a program with no effect — the
21 identity function.)</p>
22
23 <p>(In fact, for every set of Burro programs that compute the same function,
24 there is a corresponding set of antiprograms, any of which can "cancel out"
25 any program in the first set. From our proof that Burro programs form a
26 group, we obtain a constructive algorithm which, for any given program, will
27 derive only one corresponding antiprogram, a kind of syntactic inverse.)</p>
28
29 <p>This is a kind of reversible computing, but Burro differs from most reversible
30 languages in that it is not the execution trace that is being "undone", but
31 the program itself that is being annihilated.</p>
32
33 <p>This document describes version 2.0 of the Burro language, a reformulation
34 which addresses several issues with Burro 1.0. An update to the language was
35 desired by the author after it was pointed out by Alex Smith that the set of
36 Burro version 1.0 programs do not, in fact, form a proper group (the inverse
37 of (/) is {}, but no inverse of {} is defined; also, the implementations
38 (at least) did not support moving the tape head left past the "start" of the
39 tape, so &lt;> was not a well-defined program.)</p>
40
41 <p>Additionally in this document, we construct a Burro 2.0 program equivalent to
42 a certain Turing machine. While this Turing machine is not universal, the
43 translation method we use demonstrates how it would be possible to map an
44 arbitrary Turing machine to a Burro program, hopefully making uncontroversial
45 the idea that Burro qualifies as universal.</p>
46
47 <p>For further background information on the Burro project, you may also wish
48 to read the <a href="burro-1.0.html">Burro 1.0 article</a>, with the understanding that
49 the language description given there is obsolete.</p>
50
51 <h2>Changes from Burro 1.0</h2>
52
53 <p>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".</p>
57
58 <p>Henceforth in this document, the term Burro refers to Burro 2.0.</p>
59
60 <h2>About this Document</h2>
61
62 <p>This document is a reference implementation of Burro in literate Haskell,
63 using Markdown syntax for the textual prose portions (although the version
64 you are reading may have been converted to another format, such as HTML,
65 for presentation.) As such, this document serves as an "executable
66 semantics", both defining the language and providing a ready tool.</p>
67
68 <pre><code> module Main where
69 import System
70 </code></pre>
71
72 <h2>Inductive Definition of a Burro Program</h2>
73
74 <p>The symbol e is a Burro program. <br />
75 The symbol ! is a Burro program. <br />
76 The symbol + is a Burro program. <br />
77 The symbol - is a Burro program. <br />
78 The symbol &lt; is a Burro program. <br />
79 The symbol > is a Burro program. <br />
80 If a and b are Burro programs, then (a/b) is a Burro program. <br />
81 If a and b are Burro programs, then ab is a Burro program. <br />
82 Nothing else is a Burro program. </p>
83
84 <pre><code> 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 </code></pre>
94
95 <h2>Representation of Burro Programs</h2>
96
97 <p>For a concrete representation, the symbols in the inductive definition
98 given above can be taken to be a subset of a character set; for the
99 purposes of this semantics, we will use the ASCII character set. Parsing
100 a given string of symbols into a Burro program is straightforward; all
101 symbols which are not Burro symbols are simply ignored.</p>
102
103 <pre><code> instance Show Burro where
104 show Null = "e"
105 show ToggleHalt = "!"
106 show Inc = "+"
107 show Dec = "-"
108 show GoLeft = "&lt;"
109 show GoRight = "&gt;"
110 show (Test a b) = "(" ++ (show a) ++ "/" ++ (show b) ++ ")"
111 show (Seq a b) = (show a) ++ (show b)
112
113 parse string =
114 let
115 (rest, acc) = parseProgram string Null
116 in
117 trim acc
118
119 parseProgram [] acc =
120 ([], acc)
121 parseProgram ('e':rest) acc =
122 parseProgram rest (Seq acc Null)
123 parseProgram ('+':rest) acc =
124 parseProgram rest (Seq acc Inc)
125 parseProgram ('-':rest) acc =
126 parseProgram rest (Seq acc Dec)
127 parseProgram ('&lt;':rest) acc =
128 parseProgram rest (Seq acc GoLeft)
129 parseProgram ('&gt;':rest) acc =
130 parseProgram rest (Seq acc GoRight)
131 parseProgram ('!':rest) acc =
132 parseProgram rest (Seq acc ToggleHalt)
133 parseProgram ('(':rest) acc =
134 let
135 (rest', thenprog) = parseProgram rest Null
136 (rest'', elseprog) = parseProgram rest' Null
137 test = Test thenprog elseprog
138 in
139 parseProgram rest'' (Seq acc test)
140 parseProgram ('/':rest) acc =
141 (rest, acc)
142 parseProgram (')':rest) acc =
143 (rest, acc)
144 parseProgram (_:rest) acc =
145 parseProgram rest acc
146
147 trim (Seq Null a) = trim a
148 trim (Seq a Null) = trim a
149 trim (Seq a b) = Seq (trim a) (trim b)
150 trim (Test a b) = Test (trim a) (trim b)
151 trim x = x
152 </code></pre>
153
154 <h2>Group Properties of Burro Programs</h2>
155
156 <p>We assert these first, and when we describe the program semantics we will
157 show that the semantics do not violate them.</p>
158
159 <p>The inverse of e is e: ee = e <br />
160 The inverse of ! is !: !! = e <br />
161 The inverse of + is -: +- = e <br />
162 The inverse of - is +: -+ = e <br />
163 The inverse of &lt; is >: &lt;> = e <br />
164 The inverse of > is &lt;: >&lt; = e <br />
165 If aa' = e and bb' = e, (a/b)(b'/a') = e. <br />
166 If aa' = e and bb' = e, abb'a' = e. </p>
167
168 <pre><code> inverse Null = Null
169 inverse ToggleHalt = ToggleHalt
170 inverse Inc = Dec
171 inverse Dec = Inc
172 inverse GoLeft = GoRight
173 inverse GoRight = GoLeft
174 inverse (Test a b) = Test (inverse b) (inverse a)
175 inverse (Seq a b) = Seq (inverse b) (inverse a)
176 </code></pre>
177
178 <p>For every Burro program x, annihilationOf x is always equivalent
179 computationally to e.</p>
180
181 <pre><code> annihilationOf x = Seq x (inverse x)
182 </code></pre>
183
184 <h2>State Model for Burro Programs</h2>
185
186 <p>Central to the state of a Burro program is an object called a tape.
187 A tape consists of a sequence of cells in a one-dimensional array,
188 unbounded in both directions. Each cell contains an integer of unbounded
189 extent, both positive and negative. The initial value of each cell is
190 zero. One of the cells of the tape is distinguished as the "current cell";
191 this is the cell that we think of as having the "tape head" hovering over it
192 at the moment.</p>
193
194 <p>In this semantics, we represent a tape as two lists, which we treat as
195 stacks. The first list contains the cell under the tape head, and
196 everything to the left of the tape head (in the reverse order from how it
197 appears on the tape.) The second list contains everything to the right of
198 the tape head, in the same order as it appears on the tape.</p>
199
200 <pre><code> data Tape = Tape [Integer] [Integer]
201 deriving (Read)
202
203 instance Show Tape where
204 show t@(Tape l r) =
205 let
206 (Tape l' r') = strip t
207 in
208 show (reverse l') ++ "&lt;" ++ (show r')
209 </code></pre>
210
211 <p>When comparing two tapes for equality, we must disregard any zero cells
212 farther to the left/right than the outermost non-zero cells. Specifically,
213 we strip leading/trailing zeroes from tapes before comparison. We don't
214 strip out a zero that a tape head is currently over, however.</p>
215
216 <p>Also, the current cell must be the same for both tapes (that is, tape heads
217 must be in the same location) for two tapes to be considered equal.</p>
218
219 <pre><code> stripzeroes list = (reverse (sz (reverse list)))
220 where sz [] = []
221 sz (0:rest) = sz rest
222 sz x = x
223
224 ensurecell [] = [0]
225 ensurecell x = x
226
227 strip (Tape l r) = Tape (ensurecell (stripzeroes l)) (stripzeroes r)
228
229 tapeeq :: Tape -&gt; Tape -&gt; Bool
230 tapeeq t1 t2 =
231 let
232 (Tape t1l t1r) = strip t1
233 (Tape t2l t2r) = strip t2
234 in
235 (t1l == t2l) &amp;&amp; (t1r == t2r)
236
237 instance Eq Tape where
238 t1 == t2 = tapeeq t1 t2
239 </code></pre>
240
241 <p>A convenience function for creating an inital tape is also provided.</p>
242
243 <pre><code> tape :: [Integer] -&gt; Tape
244 tape x = Tape [head x] (tail x)
245 </code></pre>
246
247 <p>We now define some operations on tapes that we will use in the semantics.
248 First, operations on tapes that alter or access the cell under the tape head.</p>
249
250 <pre><code> inc (Tape (cell:left) right) = Tape (cell + 1 : left) right
251 dec (Tape (cell:left) right) = Tape (cell - 1 : left) right
252 get (Tape (cell:left) right) = cell
253 set (Tape (_:left) right) value = Tape (value : left) right
254 </code></pre>
255
256 <p>Next, operations on tapes that move the tape head.</p>
257
258 <pre><code> 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 </code></pre>
263
264 <p>Finally, an operation on two tapes that swaps the current cell between
265 them.</p>
266
267 <pre><code> swap t1 t2 = (set t1 (get t2), set t2 (get t1))
268 </code></pre>
269
270 <p>A program state consists of:</p>
271
272 <ul>
273 <li>A "data tape";</li>
274 <li>A "stack tape"; and</li>
275 <li>A flag called the "halt flag", which may be 0 or 1.</li>
276 </ul>
277
278 <p>The 0 and 1 are represented by False and True boolean values in this
279 semantics.</p>
280
281 <pre><code> data State = State Tape Tape Bool
282 deriving (Show, Read, Eq)
283
284 newstate = State (tape [0]) (tape [0]) True
285 </code></pre>
286
287 <h2>Semantics of Burro Programs</h2>
288
289 <p>Each instruction is defined as a function from program state to program
290 state. Concatenation of instructions is defined as composition of
291 functions, like so:</p>
292
293 <p>If ab is a Burro program, and a maps state S to state S', and b maps
294 state S' to S'', then ab maps state S to state S''.</p>
295
296 <pre><code> exec (Seq a b) t = exec b (exec a t)
297 </code></pre>
298
299 <p>The e instruction is the identity function on states.</p>
300
301 <pre><code> exec Null s = s
302 </code></pre>
303
304 <p>The ! instruction toggles the halt flag. If it is 0 in the input state, it
305 is 1 in the output state, and vice versa.</p>
306
307 <pre><code> exec ToggleHalt (State dat stack halt) = (State dat stack (not halt))
308 </code></pre>
309
310 <p>The + instruction increments the current data cell, while - decrements the
311 current data cell.</p>
312
313 <pre><code> exec Inc (State dat stack halt) = (State (inc dat) stack halt)
314 exec Dec (State dat stack halt) = (State (dec dat) stack halt)
315 </code></pre>
316
317 <p>The instruction &lt; makes the cell to the left of the current data cell, the
318 new current data cell. The instruction > makes the cell to the right of the
319 current data cell, the new current data cell.</p>
320
321 <pre><code> exec GoLeft (State dat stack halt) = (State (left dat) stack halt)
322 exec GoRight (State dat stack halt) = (State (right dat) stack halt)
323 </code></pre>
324
325 <p>(a/b) is the conditional construct, which is quite special.</p>
326
327 <p>First, the current data cell is remembered for the duration of the execution
328 of this construct — let's call it x.</p>
329
330 <p>Second, the current data cell and the current stack cell are swapped.</p>
331
332 <p>Third, the current stack cell is negated.</p>
333
334 <p>Fourth, the stack cell to the right of the current stack cell is made
335 the new current stack cell.</p>
336
337 <p>Fifth, if x is positive, a is evaluated; if x is negative, b is evaluated;
338 otherwise x = 0 and neither is evaluated. Evaluation occurs in the state
339 established by the preceding four steps.</p>
340
341 <p>Sixth, the stack cell to the left of the current stack cell is made
342 the new current stack cell.</p>
343
344 <p>Seventh, the current data cell and the current stack cell are swapped again.</p>
345
346 <pre><code> exec (Test thn els) (State dat stack halt) =
347 let
348 x = get dat
349 (dat', stack') = swap dat stack
350 stack'' = right (set stack' (0 - (get stack')))
351 f = if x &gt; 0 then thn else if x &lt; 0 then els else Null
352 (State dat''' stack''' halt') = exec f (State dat' stack'' halt)
353 (dat'''', stack'''') = swap dat''' (left stack''')
354 in
355 (State dat'''' stack'''' halt')
356 </code></pre>
357
358 <p>We observe an invariant here: because only the (a/b) construct affects the
359 stack tape, and because it does so in a monotonic way — that is, both a
360 and b inside (a/b) have access only to the portion of the stack tape to the
361 right of what (a/b) has access to — the current stack cell in step seven
362 always holds the same value as the current stack cell in step two, except
363 negated.</p>
364
365 <h2>Repetition</h2>
366
367 <p>The repetition model of Burro 2.0 is identical to that of Burro 1.0.
368 The program text is executed, resulting in a final state, S. If, in
369 S, the halt flag is 1, execution terminates with state S. On the other
370 hand, if the halt flag is 0, the program text is executed once more,
371 this time on state S, and the whole procedure repeats. Initially the
372 halt flag is 1, so if ! is never executed, the program never repeats.</p>
373
374 <p>Additionally, each time the program repeats, the stack tape is cleared.</p>
375
376 <pre><code> run program state =
377 let
378 state'@(State dat' stack' halt') = exec program state
379 in
380 if
381 not halt'
382 then
383 run program (State dat' (tape [0]) True)
384 else
385 state'
386 </code></pre>
387
388 <h2>Central theorem of Burro</h2>
389
390 <p>We now have established enough definitions to give a proof of the central
391 theorem of Burro, which is:</p>
392
393 <p><em>Theorem: The set of all Burro programs forms a group over computational
394 equivalence under the operation of concatenation.</em></p>
395
396 <p>As covered in the Burro 1.0 article, a "group over an equivalence relation"
397 captures the notion of replacing the concept of equality in the group
398 axioms with the concept of equivalency. Our particular equivalence relation
399 here is that two programs are equivalent if they compute the same function.</p>
400
401 <p>In order to show that a set G is a group, it is sufficient to show the
402 following four properties hold:</p>
403
404 <ol>
405 <li><p>Closure: For all a, b in G, ab is also in G.</p>
406
407 <p>This follows from the inductive definition of Burro programs.</p></li>
408 <li><p>Associativity: For all a, b and c in G, (ab)c ≡ a(bc).</p>
409
410 <p>This follows from the definition of concatenation (sequential composition);
411 it doesn't matter if we concatenate a with b first, then concatenate that
412 with c, or if we concatenate b with c first, then concatenate a with that.
413 Either way the result is the same string (or in this case, the same Burro
414 program.)</p></li>
415 <li><p>Identity element: There exists an element e in G, such that for every
416 element a in G, ea ≡ ae ≡ a.</p>
417
418 <p>The instruction e in Burro has no effect on the program state. Therefore
419 concatenating it to any existing program, or concatenating any existing
420 program to it, results in a computationally equivalent program.</p></li>
421 <li><p>Inverse element: For each a in G, there exists an element b in G such
422 that ab ≡ ba ≡ e.</p>
423
424 <p>This is the key property. We first show that it holds for each element of
425 the inductive definition of Burro programs. We can then conclude, through
426 structural induction, that all Burro programs have this property.</p>
427
428 <ol>
429 <li><p>Since e is the identity function on states, e is trivially its own
430 inverse.</p></li>
431 <li><p>Since toggling the flag twice is the same as not changing it at all,
432 the inverse of ! is !.</p></li>
433 <li><p>By the definitions of incrementation and decrementation, and because
434 data cells cannot overflow, the inverse of + is -, and the inverse
435 of - is +.</p></li>
436 <li><p>By the definitions of left and right, and because the data tape is
437 unbounded (never reaches an end,) the inverse of > is &lt;, and the inverse
438 of &lt; is >.</p></li>
439 <li><p>The inverse of ab is b'a' where b' is the inverse of b and a' is the
440 inverse of a. This is because abb'a' ≡ aea' ≡ aa' ≡ e.</p></li>
441 <li><p>The inverse of (a/b) is (b'/a'). (This is the key case of the key
442 property.) Going back to the definition of (/), we see there are three
443 sub-cases to consider. Before execution of (a/b)(b'/a'), the data tape
444 may be in one of three possible states:</p>
445
446 <ol>
447 <li><p>The current data cell is zero. So in (a/b), x is 0, which goes on
448 the stack and the current data cell becomes whatever was on the
449 stack (call it k.) The 0 on the stack is negated, thus stays 0
450 (because 0 - 0 = 0). The stack head is moved right. Neither a nor
451 b is evaluated. The stack head is moved back left. The stack and
452 data cells are swapped again, so 0 is back in the current data cell
453 and k is back in the current stack cell. This is the same as the
454 initial configuration, so (a/b) is equivalent to e. By the same
455 reasoning, (b'/a') is equivalent to e, and (a/b)(b'/a') ≡ ee ≡ e.</p></li>
456 <li><p>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 &lt; 0. The stack head is moved to the right.</p>
460
461 <p>Because x > 0, the first of the sub-programs, a, is now evaluated.
462 The current data cell could be anything — call it k'.</p>
463
464 <p>The stack head is moved back to the left, so that the current stack
465 cell is once again -x &lt; 0, and it is swapped with the current data
466 cell, making it -x and making the current stack cell k'.</p>
467
468 <p>We are now to evaluate (b'/a'). This time, we know the current data
469 cell is negative (-x &lt; 0). The data and stack cells are swapped:
470 the current data cell becomes k', and the current stack cell becomes
471 -x &lt; 0. The current stack cell is negated, so becomes x > 0. The
472 stack head is moved to the right.</p>
473
474 <p>Because -x &lt; 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.</p>
479
480 <p>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.</p></li>
484 <li><p>Case 3 is an exact mirror image of case 2 — the only difference
485 is that the first time through, x &lt; 0 and b is evaluated, thus the
486 second time through, -x > 0 and b' is evaluated. Therefore
487 (a/b)(b'/a') ≡ e in this instance as well.</p></li>
488 </ol></li>
489 </ol></li>
490 </ol>
491
492 <p>QED.</p>
493
494 <h2>Driver and Unit Tests</h2>
495
496 <p>We define a few more convenience functions to cater for the execution
497 of Burro programs on an initial state.</p>
498
499 <pre><code> interpret text = run (parse text) newstate
500
501 main = do
502 [fileName] &lt;- getArgs
503 burroText &lt;- readFile fileName
504 putStrLn $ show $ interpret burroText
505 </code></pre>
506
507 <p>Although we have proved that Burro programs form a group, it is not a
508 mechanized proof, and only goes so far in helping us tell if the
509 implementation (which, for an executable semantics, is one and the same
510 as the formal semantic formulation) is correct. Unit tests can't tell us
511 definitively that there are no errors in the formulation, but they can
512 help us catch a class of errors, if there is one present.</p>
513
514 <p>For the first set of test cases, we give a set of pairs of Burro programs.
515 In each of these pairs, both programs should be equivalent in the sense of
516 evaluating to the same tape given an initial blank tape.</p>
517
518 <p>For the second set, we simply give a list of Burro programs. We test
519 each one by applying the annihilationOf function to it and checking that
520 the result of executing it on a blank tape is equivalent to e.</p>
521
522 <pre><code> testCases = [
523 ("+++", "-++-++-++"),
524 ("+(&gt;+++&lt;/---)", "-&gt;+++&lt;"),
525 ("-(+++/&gt;---&lt;)", "+&gt;---&lt;"),
526 ("(!/!)", "e"),
527 ("+(--------!/e)", "+(/)+"),
528 ("+++(/)", "---"),
529 ("---(/)", "+++"),
530 ("+&gt; +++ --(--(--(/&gt;&gt;&gt;&gt;&gt;+)+/&gt;&gt;&gt;+)+/&gt;+)+",
531 "+&gt; &gt;&gt;&gt; +(---(/+)/)+")
532 ]
533
534 annihilationTests = [
535 "e", "+", "-", "&lt;", "&gt;", "!",
536 "++", "--", "&lt;+&lt;-", "--&gt;&gt;--",
537 "(+/-)", "+(+/-)", "-(+/-)",
538 "+(--------!/e)"
539 ]
540
541 allTestCases = testCases ++ map nihil annihilationTests
542 where
543 nihil x = ((show (annihilationOf (parse x))), "e")
544 </code></pre>
545
546 <p>Our unit test harness evaluates to a list of tests which did
547 not pass. If all went well, it will evaluate to the empty list.</p>
548
549 <pre><code> test [] =
550 []
551 test ((a, b):cases) =
552 let
553 resultA = interpret a
554 resultB = interpret b
555 in
556 if
557 resultA == resultB
558 then
559 test cases
560 else
561 ((a, b):(test cases))
562 </code></pre>
563
564 <p>Finally, some miscellaneous functions for helping analyze why the
565 Burro tests you've written aren't working :)</p>
566
567 <pre><code> debug (a, b) = ((a, interpret a), (b, interpret b))
568
569 debugTests = map debug (test allTestCases)
570 </code></pre>
571
572 <h2>Implementing a Turing Machine in Burro</h2>
573
574 <p>First we note a Burro idiom. Assume the current data cell (which
575 we'll call C) contains an odd positive integer (which we'll call x.)
576 We can test if x = 1, write a zero into C, write -x into the cell
577 to the right of C, with the following construct:</p>
578
579 <pre><code>--(F&gt;/T&gt;)&lt;
580 </code></pre>
581
582 <p>T if executed if x = 1 and F is executed otherwise. (Remember,
583 we're assuming x is odd and positive.) To make the idiom hold, we
584 also insist that T and F both leave the data tape head in the
585 position they found it. If you are wondering where the zero came
586 from — it came from the stack.</p>
587
588 <p>We now note that this idiom can be nested to detect larger odd
589 numbers. For example, to determine if x is 1 or 3 or 5:</p>
590
591 <pre><code>--(--(--(F&gt;/T5&gt;)&lt;&gt;/T3&gt;)&lt;&gt;/T1&gt;)&lt;
592 </code></pre>
593
594 <p>We can of course optimize that a bit:</p>
595
596 <pre><code>--(--(--(F&gt;/T5&gt;)/T3&gt;)/T1&gt;)&lt;
597 </code></pre>
598
599 <p>Our basic strategy is to encode the state of the Turing machine's finite
600 control as a positive odd integer, which we will call a "finite control
601 index." We make sure to always keep the current finite control index
602 available in the current data cell at the start of each loop, and we
603 dispatch on its contents using the above idiom to simulate the finite
604 control. We may use odd integers to encode the symbols on the Turing
605 Machine's tape as well.</p>
606
607 <p>We map the Turing machine state onto the Burro data tape in an interleaved
608 fashion, where three adjacent cells are used to represent one TM tape
609 cell. The first (leftmost) cell in the triple contains the finite control
610 index described above. The second cell is a "junk cell" where we can write
611 stuff and never care about it again. The third cell contains our
612 representation of the contents of the TM tape cell. Moving the TM tape
613 head one cell is simulated by moving the Burro data tape head three cells,
614 skipping over the interim finite control cell and junk cell.</p>
615
616 <p>As we always want to be on an up-to-date finite control cell at the start
617 of each iteration, we must make sure to copy it to the new tape cell triple
618 each time we move the TM tape head to a new position. If we are
619 transitioning to a different TM state as well as moving the TM tape head,
620 we can even just write in the new state at the new finite control cell.
621 None of this copying requires intermediate loops, as these value are all
622 fixed constants. The only subtlety is that we must "erase" any finite
623 control cell we move off of (set it back to zero) so that we can get it to
624 the desired value by incrementation and decrementation only. The idiom
625 given above supplies that functionality for us.</p>
626
627 <p>Note that the junk cell is used to store the end result of (/), which
628 we don't care to predict, and don't care to use again. Note also that
629 the junk cell in which the value is stored belongs to the triple of the
630 destination TM tape cell, the one to which the TM tape head is moving
631 on this transition.</p>
632
633 <p>A concrete example follows. We consider the TM tape to be over an
634 alphabet of two symbols, 1 and 3 (or in fact any odd integer greater
635 than 1), and the finite control to have three states, denoted 1, 3,
636 and 5. In addition, state 7 (or in fact any odd integer greater than 5)
637 is a halt state.</p>
638
639 <p>In state 1, <br />
640 - If the symbol is 1, enter state 3; <br />
641 - If the symbol is 3, move head right one square, and remain in state 1. </p>
642
643 <pre><code>&gt;&gt;--(+++&gt;+&gt;/+&lt;&lt;+++&gt;)&lt;
644 </code></pre>
645
646 <p>In state 3, <br />
647 - If the symbol is 1, write 3, move head left one square, and remain in
648 state 3; <br />
649 - If the symbol is 3, move head right one square, and enter state 5. </p>
650
651 <pre><code>&gt;&gt;--(+++&gt;+++++&gt;/+++&lt;&lt;&lt;&lt;&lt;+++&gt;)&lt;
652 </code></pre>
653
654 <p>In state 5, <br />
655 - If the symbol is 1, write 3, move head right one square, and remain in
656 state 5; <br />
657 - If the symbol is 3, write 1 and enter state 7. </p>
658
659 <pre><code>&gt;&gt;--(+&lt;&lt;+++++++&gt;/+++&gt;+++++&gt;)&lt;
660 </code></pre>
661
662 <p>Putting it all together, including toggling the halt flag so that, unless
663 we reach state 7 or higher, we loop through this sequence indefinitely:</p>
664
665 <pre><code>!--(--(--(!&gt;/
666 &gt;&gt;--(+&lt;&lt;+++++++&gt;/+++&gt;+++++&gt;)&lt;
667 &gt;)/
668 &gt;&gt;--(+++&gt;+++++&gt;/+++&lt;&lt;&lt;&lt;&lt;+++&gt;)&lt;
669 &gt;)/
670 &gt;&gt;--(+++&gt;+&gt;/+&lt;&lt;+++&gt;)&lt;
671 &gt;)&lt;
672 </code></pre>
673
674 <p>It is not a very interesting Turing machine, but by following this
675 construction, it should be apparent how any arbitrary Turing machine
676 could be mapped to a Burro program in the same way.</p>
677
678 <p>Happy annihilating (for reals this time)!</p>
679
680 <p>-Chris Pressey <br />
681 Cat's Eye Technologies <br />
682 June 7, 2010 <br />
683 Evanston, Illinois, USA</p>
684 </body>
685 </html>
+0
-55
doc/make.pl less more
0 #!/usr/bin/perl -w
1
2 $title = "The Burro Programming Language, v2.0";
3 $lhs_input = "../src/Burro.lhs";
4 $lhs_temp = "lhs.tmp";
5 $html_temp = "html.tmp";
6 $html_output = "burro.html";
7
8 open INFILE, "<$lhs_input";
9 open OUTFILE, ">$lhs_temp";
10
11 while (defined ($line = <INFILE>)) {
12 chomp $line;
13 if ($line =~ /^\>(.*?)coding\:(.*?)$/) {
14 # pass
15 } elsif ($line =~ /^\>(.*?)$/) {
16 print OUTFILE " $1\n";
17 } else {
18 print OUTFILE "$line\n";
19 }
20 }
21
22 close INFILE;
23 close OUTFILE;
24
25 system "Markdown.pl <$lhs_temp >$html_temp";
26
27 open INFILE, "<$html_temp";
28 open OUTFILE, ">$html_output";
29
30 print OUTFILE <<"EOH";
31 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
32 <!-- encoding: UTF-8 -->
33 <html xmlns="http://www.w3.org/1999/xhtml" lang="en">
34 <head>
35 <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
36 <title>$title</title>
37 <link rel="stylesheet" type="text/css" href="markdown-lhs.css" />
38 </head>
39 <body>
40 EOH
41
42 while (defined ($line = <INFILE>)) {
43 print OUTFILE $line;
44 }
45
46 print OUTFILE <<"EOF";
47 </body>
48 </html>
49 EOF
50
51 close INFILE;
52 close OUTFILE;
53
54 system "rm *.tmp";
+0
-17
doc/markdown-lhs.css less more
0 blockquote {
1 font-family: monospace;
2 white-space: pre;
3 border-style: solid;
4 border-width: 1px;
5 border-color: black;
6 padding-left: 3em;
7 }
8
9 pre {
10 border-style: solid;
11 border-width: 1px;
12 border-color: black;
13 padding-left: 3em;
14 padding-top: 1em;
15 padding-bottom: 1em;
16 }