git @ Cat's Eye Technologies
Import of Burro version 2.0 revision 2011.0525 sources. Cat's Eye Technologies 8 years ago
4 changed file(s) with 69 addition(s) and 67 deletion(s).
 0 0 1 1 2 2 3 3 4 25 26 But the first version is close enough for jazz, and rolls off the tongue more easily...)

26 27 27 28

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

31 same semantics as no program at all — a "no-op," or a zero-length program.

31 32 32 33

Why is this at all remarkable? Well, take the Brainfuck program fragment [-]+[]. 33 34 What could you append to it to it to make it into a "no-op" program? 51 52 52 53

Recall (or go look up in an abstract algebra textbook) that a group is 53 54 a pair of a set S and a binary operation 54 · : S × SS 55 · : S × SS 55 56 that obeys the following three axioms:

56 57 57 58
58 59 59 60
• For any three elements a, b, and c of 60 the set S, (a · b) · c = 61 a · (b · c). In other words, 61 the set S, (a · b) · c = 62 a · (b · c). In other words, 62 63 the operation is "associative." Parentheses don't matter, and we generally leave them out.
• 63 64 64 65
• There exists some element of S, which we call e, such that 65 a · e = e · a = a 66 a · e = e · a = a 66 67 for every element a of S. Think of 67 68 e as a "neutral" element that just doesn't contribute anything.
• 68 69 69 70
• For every element a of S there is an element 70 a' of S such that a · a' = e. 71 a' of S such that a · a' = e. 71 72 That is, for any element, you can find some element that "annihilates" it.
• 72 73 73 74
74 75 75

There are lots of examples of groups — the integers under the operation of 76

There are lots of examples of groups — the integers under the operation of 76 77 addition, for example, where e is 0, and the annihilator for any integer 77 78 is simply its negative (because x + (-x) always equals 0.)

78 79 79 80

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

85 86 107 108

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

114 115 125 126

To this end, let's examine the idea of a group over an equivalence relation. 126 127 All this is, really, is being specific about what constitutes "equals" in those 127 128 group axioms I listed earlier. In mathematics there is a well-established notion of 128 an equivalence relation — a relationship between elements 129 an equivalence relation — a relationship between elements 129 130 which paritions a set into 130 131 disjoint equivalence classes, where every element in a class is considered 131 132 equivalent to every other element in that same class (and inequivalent to any 153 154 interchangably with respect to the group axioms.

154 155 155 156

I'll summarize the modified definition here. A group over an equivalence relation 156 is a triple ⟨S,·,≡⟩ where:

157 is a triple 〈S,·,≡〉 where:

157 158
158 159
• S is a set
• 159
• · : S × SS is a binary operation over S
• 160
• ≡ is a reflexive, transitive, and symmetrical binary relation over S
• 160
• · : S × SS is a binary operation over S
• 161
• ≡ is a reflexive, transitive, and symmetrical binary relation over S
• 161 162
162 163

where the following axioms are also satisfied:

163 164
164
• a, b, cS: (a · b) · c ≡ 165 a · (b · c)
• 166
• eS: ∀ aS: a · ee · aa
• 167
• aS: ∃ a'S: a · a'e
• 165
• a, b, cS: (a · b) · c ≡ 166 a · (b · c)
• 167
• eS: ∀ aS: a · ee · aa
• 168
• aS: ∃ a'S: a · a'e
• 168 169
169 170 170 171

Every theorem that applies to groups should be easy to modify to be applicable 171 to a group over an equivalence relation: just replace = with ≡. So what 172 to a group over an equivalence relation: just replace = with ≡. So what 172 173 we have, for example, is that while any given e itself might not be unique, the 173 equivalence class ES that contains it is: 174 equivalence class ES that contains it is: 174 175 E is the only equivalence class that contains 175 176 elements like e and, for the purposes of the group, all of these elements are 176 177 interchangeable.

253 254 254 255
InstructionInverseConcatenationNet effect
b+-b'b+-b'beb'bb'e
b+-b'beb'bb'e
b-+b'b-+b'beb'bb'e
b-+b'beb'bb'e
b><b'b><b'beb'bb'e
b><b'beb'bb'e
b<>b'b<>b'beb'bb'e
bebeb'b'eb'b<>b'beb'bb'e
bebeb'b'eb'bb'e
255 256 256 257 257 258 258 259 259 260 260 261 261 262 262 263 263 264 264 265 265 266 266 267 271 272 272 273
InstructionInverseConcatenationNet effect
+bb'-+bb'-+e-+-e
+bb'-+e-+-e
-bb'+-bb'+-e+-+e
-bb'+-e+-+e
>bb'<>bb'<>e<><e
>bb'<>e<><e
<bb'><bb'><e><>e
ebbb'eeb'b'<bb'><e><>e
ebbb'eeb'b'bb'e
273 274 274 275 275 276 276 277 277 278 278 279 279 280 280 281 281 282 282 283 283 284 284 285 293 294 the construction of infinite loops that we can't invert by concatenation.

294 295 295 296

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

299 300 300 301

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

306 307 326 327
!!!!e
!bb'!!bb'!!e!!!e
!bb'!!e!!!e
b!!b'b!!b'beb'bb'e
b!!b'beb'bb'e
327 328 328 329 329 330 330 331 331 332 332 333 333 334 334 335

Seems so. Now we can write Burro programs that halt, and Burro programs that loop 379 380 semantics of "no-op", then every Burro program has a trivial annihilator: just 380 381 tack on an unmatching parenthesis. Similarly, if malformed programs are 381 382 considered to loop forever, how do you invert them? So, for these reasons, 382 Burro has some small amount of syntax — a bit more than Brainfuck is usually 383 Burro has some small amount of syntax — a bit more than Brainfuck is usually 383 384 considered to have, but not much.)

384 385 385 386

Now, it turns out we will have to do a fair bit of work on () in order 387 388 bit of code that includes ().

388 389 389 390

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

392 393 393 394
• (-/e)
397 398 inside the "if"... or is it because it was 1 before 398 399 the ( was encountered, and decremented to 0 by the - 399 400 instruction inside the "if"? 400 It could be either, and we don't know — so we can't find an inverse.

401 It could be either, and we don't know — so we can't find an inverse.

401 402 402 403

We remedy this in a somewhat disappointingly uninteresting way: we make a copy of 403 404 the value being tested and squirrel it away for future reference, so that pending code 408 409 It's not a full-bodied continuation, as the term continuation is often used, in the 409 410 sense of "function representing the entire remainder of the computation." 410 411 But, it's a bit of context that is retained during execution that is intended to affect 411 some future control flow decision — and that's the basic purpose of a continuation. 412 some future control flow decision — and that's the basic purpose of a continuation. 412 413 So, I will call it a continuation, although it is perhaps a diminished sort of continuation. 413 414 (In this sense, the machine stack where arguments and 414 415 return addresses are stored in a language like C is also a kind of continuation.)

423 424

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

434 435 435 436

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

440 441 513 514 514 515
InstructionInverseTest resultConcatenationNet effect
a(b/c)dd'{b'\c'}a'zeroacdd'c'a'acc'a'aa'e
zeroacdd'c'a'acc'a'aa'e
a(b/c)dd'{b'\c'}a'non-zeroabdd'b'a'abb'a'aa'e
non-zeroabdd'b'a'abb'a'aa'e
515 516 516 517 517 518 518 519 519 520 520 521 521 522

There you have it: every Burro program has an inverse.

542 543 are placed on the tape initially, starting from the head-start position, extending right. 543 544 All unspecified cells are considered to contain 0 initially.

544 545 545

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

546

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.

547 548 548 549

The meanings of the flags are as follows:

549 550 601 602 to other esolangs in an attempt to understand.

602 603 603 604

Well, it's not reversible in the sense that 604 Befreak is reversible — 605 Befreak is reversible — 605 606 you can't pause it at any point, change the direction of execution, and watch it 606 607 "go backwards". Specifically, you can't "undo" a loop in Burro by executing 607 608 20 iterations, then turning around and "un-executing" those 20 iterations; instead, 614 615 the right". But, I haven't pondered on this approach much at all.

615 616 616 617

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

620 621 621 622

It's also not reversible in the same way that 622 Kayak is reversible — 623 Kayak is reversible — 623 624 Burro programs need not be palindromes, for instance. In fact, I specifically made 624 625 the "then" and "else" components of both (/) and {\} 625 626 occur in the same order, so as to break the reflectional symmetry somewhat, and 637 638 in such a way that any previous state of the computation can always be reconstructed 638 639 given a description of the current state.

639 640 640

Burro appears to qualify by this definition — almost. The requirement 641

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

 0 0 1 1 2 2 3 3 4 16 17 the operation of concatenation and over the equivalence relation of "computes 17 18 the same function." This means that, for every Burro program, we can 18 19 construct a corresponding antiprogram that, when appended onto the first 19 program, results in a "no-op" program (a program with no effect — the 20 program, results in a "no-op" program (a program with no effect — the 20 21 identity function.)

21 22 22 23

(In fact, for every set of Burro programs that compute the same function, 324 325

(a/b) is the conditional construct, which is quite special.

325 326 326 327

First, the current data cell is remembered for the duration of the execution 327 of this construct — let's call it x.

328 of this construct — let's call it x.

328 329 329 330

Second, the current data cell and the current stack cell are swapped.

330 331 355 356 356 357 357 358

We observe an invariant here: because only the (a/b) construct affects the 358 stack tape, and because it does so in a monotonic way — that is, both a 359 stack tape, and because it does so in a monotonic way — that is, both a 359 360 and b inside (a/b) have access only to the portion of the stack tape to the 360 right of what (a/b) has access to — the current stack cell in step seven 361 right of what (a/b) has access to — the current stack cell in step seven 361 362 always holds the same value as the current stack cell in step two, except 362 363 negated.

363 364 458 459 is negated, so becomes -x < 0. The stack head is moved to the right.

459 460 460 461

Because x > 0, the first of the sub-programs, a, is now evaluated. 461 The current data cell could be anything — call it k'.

462 The current data cell could be anything — call it k'.

462 463 463 464

The stack head is moved back to the left, so that the current stack 464 465 cell is once again -x < 0, and it is swapped with the current data 480 481 cell is once again x > 0, and it is swapped with the current data 481 482 cell, making it x and making the current stack cell k. This is 482 483 the state we started from, so (a/b)(b'/a') ≡ e.

483
• Case 3 is an exact mirror image of case 2 — the only difference 484

• Case 3 is an exact mirror image of case 2 — the only difference 484 485 is that the first time through, x < 0 and b is evaluated, thus the 485 486 second time through, -x > 0 and b' is evaluated. Therefore 486 487 (a/b)(b'/a') ≡ e in this instance as well.

• 581 582

T if executed if x = 1 and F is executed otherwise. (Remember, 582 583 we're assuming x is odd and positive.) To make the idiom hold, we 583 584 also insist that T and F both leave the data tape head in the 584 position they found it. If you are wonderinf where the zero came 585 from — it came from the stack.

585 position they found it. If you are wondering where the zero came 586 from — it came from the stack.

586 587 587 588

We now note that this idiom can be nested to detect larger odd 588 589 numbers. For example, to determine if x is 1 or 3 or 5:

 15 15 } elsif (\$line =~ /^\>(.*?)\$/) { 16 16 print OUTFILE " \$1\n"; 17 17 } else { 18 \$line =~ s/\s\-\-\s/ \&mdash\; /g; 19 18 print OUTFILE "\$line\n"; 20 19 } 21 20 } 30 29 31 30 print OUTFILE <<"EOH"; 32 31 32 33 33 34 34 35 35
 12 12 the operation of concatenation and over the equivalence relation of "computes 13 13 the same function." This means that, for every Burro program, we can 14 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 15 program, results in a "no-op" program (a program with no effect — the 16 16 identity function.) 17 17 18 18 (In fact, for every set of Burro programs that compute the same function, 315 315 (a/b) is the conditional construct, which is quite special. 316 316 317 317 First, the current data cell is remembered for the duration of the execution 318 of this construct -- let's call it x. 318 of this construct — let's call it x. 319 319 320 320 Second, the current data cell and the current stack cell are swapped. 321 321 345 345 > (State dat'''' stack'''' halt') 346 346 347 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 348 stack tape, and because it does so in a monotonic way — that is, both a 349 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 350 right of what (a/b) has access to — the current stack cell in step seven 351 351 always holds the same value as the current stack cell in step two, except 352 352 negated. 353 353 457 457 is negated, so becomes -x < 0. The stack head is moved to the right. 458 458 459 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'. 460 The current data cell could be anything — call it k'. 461 461 462 462 The stack head is moved back to the left, so that the current stack 463 463 cell is once again -x < 0, and it is swapped with the current data 480 480 cell, making it x and making the current stack cell k. This is 481 481 the state we started from, so (a/b)(b'/a') ≡ e. 482 482 483 3. Case 3 is an exact mirror image of case 2 -- the only difference 483 3. Case 3 is an exact mirror image of case 2 — the only difference 484 484 is that the first time through, x < 0 and b is evaluated, thus the 485 485 second time through, -x > 0 and b' is evaluated. Therefore 486 486 (a/b)(b'/a') ≡ e in this instance as well. 577 577 T if executed if x = 1 and F is executed otherwise. (Remember, 578 578 we're assuming x is odd and positive.) To make the idiom hold, we 579 579 also insist that T and F both leave the data tape head in the 580 position they found it. If you are wonderinf where the zero came 581 from -- it came from the stack. 580 position they found it. If you are wondering where the zero came 581 from — it came from the stack. 582 582 583 583 We now note that this idiom can be nested to detect larger odd 584 584 numbers. For example, to determine if x is 1 or 3 or 5: