Burro
Burro is a brainfucklike language, the set of whose programs form an algebraic group under the operation of concatenation and over the equivalence relation "computes the same function". Burro was designed by Chris Pressey between 2005 and 2007, and revised in 2010.
The fact that Burro programs form an algebraic group means that every program has an inverse that, when concatenated with it, results in a nop. This is a form of reversible computing.
Contents
Language overview
This section describes Burro 2.0, the revision published in 2010.
Each of the symbols e
, !
, +
, 
, <
, and >
are Burro programs, as are the constructions (
a/
b)
and ab, where a and b are Burro programs. Anything not constructed from this definition is not a Burro program.
Program state consists of two tapes, a data tape and a stack tape (each unbounded on left and right), and a Boolean halt flag, initially 1 (for true). Each tape cell holds an integer value, initially 0, which is unbounded and can be positive or negative. The commands (and constructions) work as follows:
Command  Inverse  Description 

e

e

Do nothing; nop. 
!

!

Toggle halt flag. 
+



Increment value under tape head on data tape. 


+

Decrement value under tape head on data tape. 
<

>

Move data tape head one cell left. 
>

<

Move data tape head one cell right. 
( a/ b)

( b'/ a')

Conditional construct (see below). 
ab  b'a'  Effect of executing a followed by b. 
The inverses are given on the assumption that a and b are Burro programs, and that their inverses are a' and b' respectively.
The conditional construct (
a/
b)
works as follows:
 The value of the current cell on the data tape is saved (as x, let's say) while this construct is run.
 The current data cell and stack cell are swapped.
 The current stack cell is negated.
 The stack tape's head moves one cell to the right.
 With this starting state, a is executed if x > 0; b is executed if x < 0; nothing is done if x = 0.
 The stack tape's head moves one cell to the left.
 The current data cell and stack cell are again swapped.
When the end of the code is reached, if the halt flag is still 1, the program halts. Otherwise, the code is executed again from the beginning (without resetting program state).
Constructing More Conditionals
In any language it is important to be able to construct arbitrary conditionals.
With the (a/b)
, if a
and b
has the same amount of >
as <
and data pointer's value
where the pointer starts before the conditional is unchanged by a
and b
then, the space under the pointer will be set to its negative.
Because of this, (e/e)
will just negate the data under the pointer.
(e/e)(b/a)
removes the negating effect of the condition.
x = 0
can be achieved by using
(a'/a')a
, a
must start at the conditional's start
x >= 0
with (e/a')a
, a
must start at the conditional's start
x <= 0
with (a'/e)a
, a
must start at the conditional's start
All the rest of the comparing conditionals can be done by starting with a sequence of 
with the same number of +
afterwards
or a sequence of +
with the same number if 
afterwards
Converting from BF
Given how close it is to brainfuck
if BF's [a]
conditional is replicateable in Burro then Burro is Turing Complete.
The main problem is that the (a/b)
can not change the value of the spot that's used on during a
or b
.
Significance
Chris Pressey's documentation for version 2.0 contains a proof that every Burro program has an inverse, or "annihilator", such that the concatenation of a program and its annihilator results in a nop. This is the most important of four properties (the other three being fairly trivial) required to prove the "central theorem of Burro": "The set of all Burro programs forms a group over computational equivalence under the operation of concatenation."
It is suggested that Burro 2.0 is Turingcomplete, but this is not fully proven, only demonstrated via the implementation of a specific Turing machine in Burro.