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.
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).
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.