Reversible Brainfuck

Reversible Brainfuck is a brainfuck derivative created by User:ais523 at the end of 2006. It uses the same right-infinite tape starting with zeros as brainfuck does, and most of the same commands.
==Commands==
Six of the commands are identical to brainfuck.	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. 	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 non-zero).
==Compatibility==
Reversible Brainfuck uses a right-infinite 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 b-a. In addition, increment uses a temp flag with value 1:
 W1+(x,y;f): x=a, y=b-a, 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;b-1) ] [ 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;b-1) + ] [ - ]
The following table shows how each subloop in the recursive W2+ case acts on (x,f):
 a=0 | 1<=ab</code> 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 non-zero 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 non-brainfuck 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	Tape layout	Tape layout
Position 	Contents 	Description
0 	0 	Left boundary data search mark
1 	0 	Left boundary history search mark
2 	d0 	First brainfuck data cell
3 	h0 	First branch history flag
4n 	1 	Search marks to the left of current brainfuck data cell
4n 	0 	Search marks to the right of current brainfuck data cell
4n+1 	1 	Search marks to the left of current branch history flag
4n+1 	0 	Search marks to the right of current branch history flag
4n+2 	dn 	Brainfuck data cell
4n+3 	hn 	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 well-known constructions for Minsky machines can be adapted to give further reductions to a bounded tape with unbounded (only non-negative 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 base b number
* r - right part of tape, as a base b 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 non-negative 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 well-known result that a reversible machine needs only two unbounded registers to be TC, same as a non-reversible one.
==Implementations==
weave.rb supports Reversible Brainfuck with the -r flag.
==See also==
*Brainfuck
*Reversible Bitfuck
Category:Languages
Category:Reversible computing
Category:2006
Category:Implemented
Category:Brainfuck derivatives
Category:Turing complete