Simulate a reversible Turing machine in 50 lines of code
This blog covers
What is a reversible Turing machine (RTM),
Simulate an RTM in 50 lines,
Implement the incrementor on this RTM.
(For the Chinese version)
What is a reversible Turing machine?
To understand the RTM, let's first review what a Turing machine is. We can imagine a Turing machine as a walking read-write head on tape. The head has a state inline_formula not implemented. The tape is consists of a sequence of cells, with each cell containing a symbol inline_formula not implemented. Each time step, the head can take action specified by the rule table inline_formula not implemented. Hence, the quadruple form of 1-tape Turing machine can be defined as
formula not implemented
where inline_formula not implemented and inline_formula not implemented are initial and final states of a TM. The symbol set inline_formula not implemented contains a special symbol "_", which represents BLANK. An element in inline_formula not implemented is defined as
formula not implemented
where the left and right side of inline_formula not implemented represent actions
Symbol rule if inline_formula not implemented is a symbol in inline_formula not implemented. If the head is in state inline_formula not implemented while on tape cell with content inline_formula not implemented, overwrite the cell content with inline_formula not implemented and change the head state to inline_formula not implemented . In the following example, symbol rule (3, 0, 1,4) is matched.
2. Move rule if inline_formula not implemented is a "/" (SLASH). If inline_formula not implemented is "inline_formula not implemented" (LEFT), move left, else if inline_formula not implemented is "inline_formula not implemented" (STAY), otherwise, inline_formula not implemented must be "inline_formula not implemented", move right. In the following example, move rule (4, /, ←, 5) is matched.
Note: If you are familiar with the quintuple definition of a Turing machine, the quadruple rule simply separates the Move rule and Symbol rule for later convenience of defining RTM.
A TM that we often discuss is deterministic, that is, no two rules apply in the same case. For an arbitrary pair of rules inline_formula not implemented and inline_formula not implemented, if inline_formula not implemented, then we must have inline_formula not implemented , that is, for the head in the same state, there should not be two move rules, the coexistence of move rules and symbol rules or two Symbol rules that modifies the same symbol.
What is an Reversible-TM? RTM puts more restrictions on a Turing machine. The restriction is if inline_formula not implemented , then inline_formula not implemented , or inverse deterministic. In any condition, there exists a unique rule to undo the previous operation. This definition was first proposed in Bennett's paper in 1973 [Ref. 3]. This paper also mentions the multi-tape version, which can be defined similarly. The first programming language implementation of RTM is in Janus [Ref. 1]. In the following, we introduce how to simulate it in NiLang - a reversible eDSL in Julia.
Simulate an RTM in 50 lines
In this section, we are going to implement an RTM with Julia language and make it run forward and backward. Codes have been uploaded to Github, welcome for star, issue, and pull requests.
First, we need to install a package NiLang, an embeded reversible domain-specific language (eDSL) in Julia. We will use it to write reversible functions. You can find NiLang's paper on arxiv:
Differentiate Everything with a Reversible Programming Language
Since NiLang is r-Turing complete, it can of cause be used to simulate RTM. You can get some guide in NiLang's README. To install this package in Julia is convenient, open a Julia REPL, and type the following command.
First, we define some constants and structs.
We use integers as "symbols" in our simulation, where
RTM struct contains an initial state
qs, a final state
qf, and a collection of rules (the inline_formula not implemented). Each rule is a Quadruple instance.
The following is the main function.
@i before the function keywork is from NiLang. This macro compiles the function body of a reversible function. The return values of this function are same as input arguments. In the body, there are reversible statements. Left and right arrows are variable allocation and deallocation. One can simply take "←" as assign, "→" as assert. The condition expression in the
while statement contains two expressions, one for precondition and another for postcondition.
identity is the identity mapping. For more details about grammar, please read NiLang's paper or its Github. Here, rules are matched through enumeration. In each iteration, the program increments the program counter
pc for one and try the match and execute the
pc-th rule using
instr defined bellow.
This function is also reversible. It tries to match the symbol rule or the move rule
cmd, if either of the rules matches, apply the rule, otherwise, do nothing. Notice here, an additional postcondition is provided to ensure reversibility. Here, the rules must satisfy the reversibility condition mentioned above. Otherwise, an
InvertibilityError will be thrown.
Implement the incrementor on this RTM.
Let's first define the quadruple rules for the incrementor, as well as the corresponding RTM.
It requires some paperwork to figure out why this rule calculates an incrementor. In the following, we define the tape as a vector. We put a
BLANK symbol in head and tail, the bits in between represents an integer in the big-endian format.
read_tape read the bits on tape as an integer, we can see the tape is initialized in state inline_formula not implemented.
Then we define a test function to print and check the result
@instr is defined in NiLang, it changes variables inplace, see NiLang paper for details. 10 forward and 10 backward executions are done. Notice the inverse function
~run! is defined automatically. The results are shown bellow
It will increment the number with a period of 32. The Github version supports the visualize keyword argument so that we can visualize the computational process.
Principles of a reversible programming language
Reversible computing and cellular automata—A survey
Logical Reversibility of Computation