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

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

where the left and right side of inline_formula not implemented represent actions

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

Before:

              3

              ↓

| - | 0 | 0 | 0 | 1 | 0 | - |    <- tape

—————————————————————————————

After:

              4

              ↓ (3 0 1 4)  <- rule applied

| - | 0 | 0 | 1 | 1 | 0 | - |

—————————————————————————————

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.

Before:

              4

              ↓

| - | 0 | 0 | 1 | 1 | 0 | - |

—————————————————————————————

After:

          5

          ↓ (4 / ← 5)

| - | 0 | 0 | 1 | 1 | 0 | - |

—————————————————————————————

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.

]add NiLang

First, we define some constants and structs.

using NiLang

const BLANK = -10000000

const SLASH = -10000001

const LEFT = -10000002

const RIGHT = -10000003

const STAY = -10000004

struct RTM{QT,RT}

    qs::QT

    qf::QT

    rules::RT

end

struct Quadruple{QT, ST}

    q1::QT

    s1::ST

    s2::ST

    q2::QT

end

We use integers as "symbols" in our simulation, where

• BLANK: the special blank symbol

• SLASH: move rule "\"

• LEFT: left move "←"

• RIGHT: right move "→"

• STAY: do not move "inline_formula not implemented"

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.

"""

`rtm` is an RTM instance,

`tape` is a vector of symbols,

`loc` is the location of read/write head on the tape,

`pc` is the program counter to search rules, it if often initialized to 1.

"""

@i function run!(rtm::RTM, tape, loc, pc)

    q ← rtm.qs

    while (q != rtm.qf, q != rtm.qs)

        # state q, at loc

        instr(q, tape[loc], rtm.rules[pc], loc)

        pc += identity(1)

        if (pc == length(rtm.rules)+1, pc == 1)

            pc -= @const length(rtm.rules)

        end

    end

    q → rtm.qf

end

The macro @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.

"""

An RTM in state `q`, with the head in `loc` while reading symbol `s`, try to apply the qadruple rule `cmd`.

"""

@i function instr(q, s, cmd::Quadruple, loc)

    if (q == cmd.q1 && s == cmd.s1, q == cmd.q2 && s == cmd.s2)

        # Symbol rule

        q += cmd.q2 - cmd.q1

        s += cmd.s2 - cmd.s1

    elseif (q == cmd.q1 && cmd.s1 == SLASH, q == cmd.q2 && cmd.s1 == SLASH)

        # Shift rule

        q += cmd.q2 - cmd.q1

        if (cmd.s2 == RIGHT, ~)

            loc += identity(1)

        elseif (cmd.s2 == LEFT, ~)

            loc -= identity(1)

        end

    end

end

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.

Done!

Implement the incrementor on this RTM.

Let's first define the quadruple rules for the incrementor, as well as the corresponding RTM.

rules = [

    1 BLANK BLANK 2;

    2 SLASH RIGHT 3;

    3 0     1     4;

    3 1     0     2;

    3 BLANK BLANK 4;

    4 SLASH LEFT  5;

    5 0     0     4;

    5 BLANK BLANK 6;

]

prog = [Quadruple(rules[i,:]...) for i=1:size(rules, 1)]

rtm = RTM(1,6,prog);

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.

tape = [BLANK, 1, 1, 0, 0, 1, BLANK]

function read_tape(tape)

    sum(tape[2:end-1] .* (1 .<< (0:length(tape)-3)))

end

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

function main(rtm, tape)

    loc = 1

    pc = 1

    println("marching forward")

    for i=1:10

        @instr run!(rtm, tape, loc, pc)

        println("number → $(read_tape(tape))")

    end

    println("marching backward")

    for i=1:10

        @instr (~run!)(rtm, tape, loc, pc)

        println("number → $(read_tape(tape))")

    end

end

The macro @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

main(rtm, tape)

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.

julia> ReversibleTuringMachine.run!(rtm, tape, 1, 1; visualize=true);

  2

  ↓ (1 _ _ 2)

| - | 1 | 1 | 0 | 0 | 1 | - |

—————————————————————————————

      3

      ↓ (2 / → 3)

| - | 1 | 1 | 0 | 0 | 1 | - |

—————————————————————————————

      2

      ↓ (3 1 0 2)

| - | 0 | 1 | 0 | 0 | 1 | - |

—————————————————————————————

          3

          ↓ (2 / → 3)

| - | 0 | 1 | 0 | 0 | 1 | - |

—————————————————————————————

          2

          ↓ (3 1 0 2)

| - | 0 | 0 | 0 | 0 | 1 | - |

—————————————————————————————

              3

              ↓ (2 / → 3)

| - | 0 | 0 | 0 | 0 | 1 | - |

—————————————————————————————

              4

              ↓ (3 0 1 4)

| - | 0 | 0 | 1 | 0 | 1 | - |

—————————————————————————————

          5

          ↓ (4 / ← 5)

| - | 0 | 0 | 1 | 0 | 1 | - |

—————————————————————————————

          4

          ↓ (5 0 0 4)

| - | 0 | 0 | 1 | 0 | 1 | - |

—————————————————————————————

      5

      ↓ (4 / ← 5)

| - | 0 | 0 | 1 | 0 | 1 | - |

—————————————————————————————

      4

      ↓ (5 0 0 4)

| - | 0 | 0 | 1 | 0 | 1 | - |

—————————————————————————————

  5

  ↓ (4 / ← 5)

| - | 0 | 0 | 1 | 0 | 1 | - |

—————————————————————————————

  6

  ↓ (5 _ _ 6)

| - | 0 | 0 | 1 | 0 | 1 | - |

—————————————————————————————

References

1. Principles of a reversible programming language

2. Reversible computing and cellular automata—A survey

3. Logical Reversibility of Computation