Reversible Brainfuck
Reversible Brainfuck is a brainfuck derivative created by User:ais523 at the end of 2006. It uses the same rightinfinite tape starting with zeros as brainfuck does, and most of the same commands.
Contents
Commands
Six of the commands are identical to brainfuck.  

+ 
Increment the current cell. 
 
Decrement the current cell. 
> 
The cell to the right of the current cell becomes current. 
< 
The cell to the left of the current cell becomes current. 
. 
Output a character whose ASCII code is that of the current cell. 
] 
If the current cell is nonzero, jump backwards to just after the matching [ .

Two of the commands are changed.  
, 
Input a character and store its ASCII code in the current cell, if it contains a 0. If the current cell doesn't contain a 0, end the program. EOF is treated as if a 0 were read. 
[ 
If the current cell is nonzero, jump forwards to just after the matching ] . (In brainfuck, [ jumps forwards if the current cell is zero, but Reversible Brainfuck jumps forwards if the current cell is nonzero).

Compatibility
Reversible Brainfuck uses a rightinfinite tape. Each cell on the tape must be able to be decremented 255 times from zero and incremented 255 times from zero without giving a zero result on any increment. (However, it's legal to use a wrapping system where, for instance, 128 and 128 are the same number.)
Algorithms
Some algorithms to use in later computational class constructions.
Inspired by the notation in brainfuck algorithms, the balanced loop algorithms below don't use <>
directly. For portability, other commands are instead labeled with the cell they affect. To make this more visually reversible, the labels are put on a separate line above the commands.
Moving a value
Moving from cell x
to cell y
, initially zero, using temp flag f
.
MOV(x,y;f): x=a>=0, y=0, f=0 > x=0, y=a, f=0 x f x f y f y x f x f y f y [ + ] [ [ + ]+ [  ] ] [  ]
Other commands can be inserted inside the main loop, e.g. to do addition:
ADD(x,y,z;f): x=a>=0, y=0, z=b, f=0 > x=0, y=a, z=a+b, f=0 x f x f y f y z x f x f y f y [ + ] [ [ + ]+ + [  ] ] [  ]
Wrapping increment/decrement
Two methods of simulating a wrapping cell with cell size b
(either with unbounded cells or simply with a larger wrapping) are given.
The first one can also be used if b
is not statically known. It uses two cells, one with the intended value a
and the other with value ba
. In addition, increment uses a temp flag with value 1:
W1+(x,y;f): x=a, y=ba, f=1 > x=(a+1)%b, y=b(a+1)%b, f=1 x f x f x f x y f y f y f y x W1+(x,y;f) = [  ] [ [ + ]+ [  ] ] [ + ]+ 
Reverse to decrement:
x y f y f y f y x f x f x f x W1(x,y;f) = + [  ] [ [ + ]+ [  ] ] [ + ]
The second method is defined recursively on b
, so requires it to be statically known, and is also more complicated except for b=2
. However, it uses one fewer cell:
W2+(x;f;b): x=a, f=0 > x=(a+1)%b, f=0 x f x f x f x f x f W2+(x;f;2) = [ + ]+ [  ] [ + ]  x f x f x x f x f x f x f x f x W2+(x;f;b) = [ + ] [  W2+(x;f;b1) ] [ W2+(f;x;2) ] [ + ] [  ]
Decrement (b=2
is its own inverse):
x f x f x f x f x f x x f x f x W2(x;f;b) = [ + ] [  ] [ W2+(f;x;2) ] [ W2(x;f;b1) + ] [  ]
The following table shows how each subloop in the recursive W2+
case acts on (x,f)
:
a=0  1<=a<b  a=b ++ (0, 0)  (a, 0)  (b, 0) (0, 1)  (a, 0)  (b, 0) (0, 1)  (a, 0)  (0, 0) (0, 0)  (a, 0)  (0, 1) (1, 0)  (a+1, 0)  (0, 1) (1, 0)  (a+1, 0)  (0, 0)
Pushing / popping digits from a base b
number
This algorithm and its reverse can be used to implement a stack, and to do multiplication/division with remainder, which will be the core of later computational class proofs.
Here X
is a wrapping cell with size b
, simulated using either of the methods above.
PUSH(X,s,t;f): X=a, s=c>=0, t=0, f=0 > X=0, s=0, t=a+b*c, f=0 X s f s X f t f t X s X s f s X f t f t PUSH(X,s,t;f) = [ [ + ] ] [ [ + ]+ [  ]W[ [  ] ] ] [  ]
The algorithm here is essentially the one for MOV(X,t;f)
adjusted such that both X
and s
must be 0 to skip/exit the loop, and such that s
is decremented whenever X
is decremented from 0.
Reverse:
t f t f X s f s X s X t f t f X s f s X POP(X,s,t;f) = [ + ] [ [ [ + ] ]W+[ + ] [  ] ] [ [  ] ]
Using the first wrapping method where X
is implemented with x
and y
summing to b
, PUSH1(x,y,s,t;f)
expands to:
x s f s x f t f t x s f x f x f x y f y f y f y x s f s x f t f t [ [ + ] ] [ [ + ]+ [   ] [ [ + ]+ [  ] ] [ + ]+ [ [  ] ] ] [  ]
Using the second method, f
needs to be adjusted:
x s f s x f t f t x s x f x f x s f s x f t f t PUSH2(x,s,t;f;b) = [ [ + ] ] [ [ + ]+ [  ]  W2(x;f;b) + [ [  ] ] ] [  ]
Computational class
The following reduction from ordinary brainfuck to Reversible Brainfuck proves that the latter is Turing complete. It ignores the special behavior of input on a nonzero cell.
To avoid the impossible deletion of information in a reversible language, the translation works by keeping a complete history of all branching.
Note that all nonbrainfuck data cells will contain only values 0 or 1. Therefore this reduction can be applied to any cell size, even single bit cells. (E.g. this also proves Turing complete reversible boolfuck.)
Tape layout  

Position  Contents  Description 
0  0  Left boundary data search mark 
1  0  Left boundary history search mark 
2  d_{0}  First brainfuck data cell 
3  h_{0}  First branch history flag 
4n  1  Search marks to the left of current brainfuck data cell 
0  Search marks to the right of current brainfuck data cell  
4n+1  1  Search marks to the left of current branch history flag 
0  Search marks to the right of current branch history flag  
4n+2  d_{n}  Brainfuck data cell 
4n+3  h_{n}  Branch history flag 
Brainfuck command  Reversible brainfuck 

+ 
+ 
 
 
> 
>>+>> 
< 
<<<< 
. 
. 
, 
, (with limitations)

[ 
[>>[<<<<]>[>>>>]<< +>>[<<<<]<[>>>>]<< ]>>[<<<<]>[>>>>]<< [>>+>> >>[<<<<]<[>>>>]<< 
] 
>>[<<<<]>[>>>>]<< +>>[<<<<]<[>>>>]<< [>>[<<<<]>[>>>>]<< >>[<<<<]<[>>>>]<< ]>>[<<<<]>[>>>>]<< ]>>+>> >>[<<<<]<[>>>>]<< 
Unbounded cells, bounded tape
The previous construction shows that Reversible Brainfuck with bounded cells and unbounded tape is Turing complete. Using the notation from the Algorithms section, two wellknown constructions for Minsky machines can be adapted to give further reductions to a bounded tape with unbounded (only nonnegative values used) cells, thus proving that too Turing complete.
The first construction does a reduction from an unbounded tape with size b
cells to five unbounded registers:

x
 source program's current cell 
f
 status flag 
l
 left part of tape, as a baseb
number 
r
 right part of tape, as a baseb
number 
t
 temporary storage
x x x x [ ] . , are implemented as [ ] . , respectively (that is, as themselves applied at cell x). x x + W2+(x;f;b), or just + if known not to wrap. x x  W2(x;f;b), or just  if known not to wrap. > PUSH2(x,l,t;f;b) MOV(t,l;f) POP2(x,r,t;f;b) MOV(t,r;f) < PUSH2(x,r,t;f;b) MOV(t,r;f) POP2(x,l,t;f;b) MOV(t,l;f)
The second construction translates a cell labeled program on an already bounded tape of unbounded nonnegative cells, to a similar program using only four cells. I/O is not supported.
An original RBF program needs first to be put in cell labeled notation, which means each command must be applied to a statically known cell, which is equivalent to all of its loops having an equal number of <
s and >
s, aka a "balanced loop" program.
This construction encodes all the source cells as prime exponents of a single number. First, to each cell c
in the source program assign a distinct prime number p(c)
. E.g.
p(x)=2, p(f)=3, p(l)=5, p(r)=7, p(t)=11
The cells of the target program are:

x
 used for divisibility checking, otherwise kept zero 
f
 status flag 
n
 number whose prime exponents encode the source cells 
t
 temporary storage
Next, translate each basic labelled command as follows:
n Start + (Initialize n to 1, or all exponents to 0.) c + PUSH2(x,n,t;f;p(c)) MOV(t,n;f) (multiplies n by p(c)) c  POP2(x,t,n;f;p(c)) MOV(t,n;f) (divides n by p(c), undefined behavior if not divisible) c x f x f x f x [ POP2(x,t,n;f;p(c)) [ + ] [ [  ] PUSH2(x,t,n;f;p(c)) (divides n by p(c), checks the remainder to branch, then multiplies back) c x f x f x f x ] POP2(x,t,n;f;p(c)) [ + ] ] [  ] PUSH2(x,t,n;f;p(c)) (ditto)
As a final note, the resulting labeled 4 cell program can also be interpreted as a "reversible Minsky machine", whose registers are n
and t
and whose finite state consists of a combination of the RBF program position, and the cells x
and f
(whose values are bounded).
This then proves the probably wellknown result that a reversible machine needs only two unbounded registers to be TC, same as a nonreversible one.
Implementations
weave.rb supports Reversible Brainfuck with the r flag.