| 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 <> 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 < 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 = "<"
|
| 109 | |
show GoRight = ">"
|
| 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 ('<':rest) acc =
|
| 128 | |
parseProgram rest (Seq acc GoLeft)
|
| 129 | |
parseProgram ('>':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 < is >: <> = e <br />
|
| 164 | |
The inverse of > is <: >< = 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') ++ "<" ++ (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 -> Tape -> Bool
|
| 230 | |
tapeeq t1 t2 =
|
| 231 | |
let
|
| 232 | |
(Tape t1l t1r) = strip t1
|
| 233 | |
(Tape t2l t2r) = strip t2
|
| 234 | |
in
|
| 235 | |
(t1l == t2l) && (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] -> 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 < 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 > 0 then thn else if x < 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 <, and the inverse
|
| 438 | |
of < 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 < 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 < 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 < 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.</p>
|
| 473 | |
|
| 474 | |
<p>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.</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 < 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] <- getArgs
|
| 503 | |
burroText <- 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 | |
("+(>+++</---)", "->+++<"),
|
| 525 | |
("-(+++/>---<)", "+>---<"),
|
| 526 | |
("(!/!)", "e"),
|
| 527 | |
("+(--------!/e)", "+(/)+"),
|
| 528 | |
("+++(/)", "---"),
|
| 529 | |
("---(/)", "+++"),
|
| 530 | |
("+> +++ --(--(--(/>>>>>+)+/>>>+)+/>+)+",
|
| 531 | |
"+> >>> +(---(/+)/)+")
|
| 532 | |
]
|
| 533 | |
|
| 534 | |
annihilationTests = [
|
| 535 | |
"e", "+", "-", "<", ">", "!",
|
| 536 | |
"++", "--", "<+<-", "-->>--",
|
| 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>/T>)<
|
| 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>/T5>)<>/T3>)<>/T1>)<
|
| 592 | |
</code></pre>
|
| 593 | |
|
| 594 | |
<p>We can of course optimize that a bit:</p>
|
| 595 | |
|
| 596 | |
<pre><code>--(--(--(F>/T5>)/T3>)/T1>)<
|
| 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>>>--(+++>+>/+<<+++>)<
|
| 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>>>--(+++>+++++>/+++<<<<<+++>)<
|
| 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>>>--(+<<+++++++>/+++>+++++>)<
|
| 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>!--(--(--(!>/
|
| 666 | |
>>--(+<<+++++++>/+++>+++++>)<
|
| 667 | |
>)/
|
| 668 | |
>>--(+++>+++++>/+++<<<<<+++>)<
|
| 669 | |
>)/
|
| 670 | |
>>--(+++>+>/+<<+++>)<
|
| 671 | |
>)<
|
| 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>
|