# Simulate a reversible Turing machine in 50 lines of code ![julia.png][nextjournal#file#5c09851e-4fbd-4fb1-afbe-1152084be27b] 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](https://zhuanlan.zhihu.com/p/126192021)) ## 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** $q \in Q$. The tape is consists of a sequence of cells, with each cell containing a **symbol** $s\in S$. Each time step, the head can take **action** specified by the **rule table** $\delta$. Hence, the quadruple form of 1-tape Turing machine can be defined as $$ T_4 = (Q, S, q_s, q_f, s_b, δ), $$ where $q_s$ and $q_f$ are initial and final states of a TM. The symbol set $S$ contains a special symbol "_", which represents BLANK. An element in $\delta$ is defined as $$ (q_1, s_1, s_2, q_2)\in (Q × S × S × Q) ∪ (Q × {/} × \{\leftarrow, \leftrightarrow, \rightarrow\} × Q), $$ where the left and right side of $\cup$ represent **actions** 1. **Symbol rule** if $s_1$ is a symbol in $S$. If the head is in state $q_1$ while on tape cell with content $s_1$, overwrite the cell content with $s_2$ and change the head state to $q_2$ . In the following example, symbol rule (3, 0, 1,4) is matched. ```no-exec id=8b61a7b0-3e2e-42d8-ac82-a4afddb5b4f6 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 $s_1$ is a "/" (SLASH). If $s_2$ is "$\leftarrow$" (LEFT), move left, else if $s_2$ is "$\leftrightarrow$" (STAY), otherwise, $s_2$ must be "$\rightarrow$", move right. In the following example, move rule (4, /, ←, 5) is matched. ```no-exec id=478069bb-b36b-4e8b-9f9a-ad92257a0f77 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 $(q_1, s_1, s_2, q_2)$ and $(p_1, c_1, c_2, p_2)$, if $p_1 = q_1$, then we must have $c_1 \neq / ∧ s_1 \neq / ∧ c_1 \neq s_1$ , 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 $q_1 = q_2$ , then $c_1 \neq / ∧ s_1 \neq / ∧ s_2 \neq c_2$ , 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](https://julialang.org/) language and make it run forward and backward. Codes have been uploaded to [Github](https://github.com/GiggleLiu/ReversibleTuringMachine.jl), 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​](https://arxiv.org/abs/2003.04617) Since NiLang is r-Turing complete, it can of cause be used to simulate RTM. You can get some guide in [NiLang's README](https://github.com/GiggleLiu/NiLang.jl). To install this package in Julia is convenient, open a Julia REPL, and type the following command. ```julia id=0d150555-172a-4a20-8c96-d9629954cc83 ]add NiLang ``` First, we **define some constants and structs.** ```julia id=929538bc-f7ae-46e1-9bd8-cf623d71d17a 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 "$\leftrightarrow$" RTM struct contains an initial state `qs`, a final state `qf`, and a collection of rules (the $\delta$). Each rule is a Quadruple instance. The following is **the main function.** ```julia id=df65238e-4156-4b9b-9f42-03c3e7656564 """ `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](https://arxiv.org/abs/2003.04617) 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. ```julia id=d238e3b1-08e9-481d-8d6d-52f2783ae1fd """ 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. ```julia id=cb4442c4-aa31-4afd-9686-0d9bc1785a54 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](https://en.wikipedia.org/wiki/Endianness) format. ```julia id=44b1ccdc-70c2-4110-b0b4-70a4ae33a0fc 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 $19 = 1\times 2^0 + 1\times 2^1 + 1\times 2^4$. Then we define a test function to print and check the result ```julia id=2443f7c4-6682-4e78-9e2d-3fe16dcd038a 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](https://arxiv.org/abs/2003.04617) for details. 10 forward and 10 backward executions are done. Notice the inverse function `~run!` is defined automatically. The results are shown bellow ```julia id=b334a484-f5fc-4f38-ab2e-3d9a748c4df4 main(rtm, tape) ``` It will increment the number with a period of 32. The [Github version](https://github.com/JuliaReverse/ReversibleTuringMachine.jl) supports the visualize keyword argument so that we can visualize the computational process. ```no-exec id=25090007-4b34-4def-8278-cc531ba384aa 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](https://dl.acm.org/doi/10.1145/1366230.1366239) 2. [Reversible computing and cellular automata—A survey](https://www.sciencedirect.com/science/article/pii/S030439750800100X) 3. [Logical Reversibility of Computation](https://pdfs.semanticscholar.org/4c76/71550671deba9ec318d867522897f20e19ba.pdf?_ga=2.54101544.1421561968.1586161542-1569382451.1571329389) [nextjournal#file#5c09851e-4fbd-4fb1-afbe-1152084be27b]:
This notebook was exported from https://nextjournal.com/a/MQFWwVteEkLMF659qMv6x?change-id=CsUMT4ZhFsY3qPbtuWekSx ```edn nextjournal-metadata {:article {:settings nil, :nodes {"0d150555-172a-4a20-8c96-d9629954cc83" {:compute-ref #uuid "c790d817-a409-446a-a690-5b9972d66b38", :exec-duration 77182, :id "0d150555-172a-4a20-8c96-d9629954cc83", :kind "code", :output-log-lines {:stdout 150}, :runtime [:runtime "90436991-2923-44bb-b0d1-f235aec846ef"], :stdout-collapsed? false}, "2443f7c4-6682-4e78-9e2d-3fe16dcd038a" {:compute-ref #uuid "1eab29d3-63db-4488-9b52-0e31d68f8c78", :exec-duration 151, :id "2443f7c4-6682-4e78-9e2d-3fe16dcd038a", :kind "code", :output-log-lines {}, :runtime [:runtime "90436991-2923-44bb-b0d1-f235aec846ef"]}, "25090007-4b34-4def-8278-cc531ba384aa" {:id "25090007-4b34-4def-8278-cc531ba384aa", :kind "code-listing"}, "44b1ccdc-70c2-4110-b0b4-70a4ae33a0fc" {:compute-ref #uuid "42fff7fa-670d-49dd-9938-695391631eda", :exec-duration 473, :id "44b1ccdc-70c2-4110-b0b4-70a4ae33a0fc", :kind "code", :output-log-lines {}, :runtime [:runtime "90436991-2923-44bb-b0d1-f235aec846ef"]}, "478069bb-b36b-4e8b-9f9a-ad92257a0f77" {:id "478069bb-b36b-4e8b-9f9a-ad92257a0f77", :kind "code-listing"}, "5c09851e-4fbd-4fb1-afbe-1152084be27b" {:id "5c09851e-4fbd-4fb1-afbe-1152084be27b", :kind "file"}, "8b61a7b0-3e2e-42d8-ac82-a4afddb5b4f6" {:id "8b61a7b0-3e2e-42d8-ac82-a4afddb5b4f6", :kind "code-listing"}, "90436991-2923-44bb-b0d1-f235aec846ef" {:environment [:environment {:article/nextjournal.id #uuid "02d93432-6116-4485-9ef3-246489903c6d", :change/nextjournal.id #uuid "5e8d78fc-f357-4d5b-96bb-b563f9f76e81", :node/id "90436991-2923-44bb-b0d1-f235aec846ef"}], :environment? true, :id "90436991-2923-44bb-b0d1-f235aec846ef", :kind "runtime", :language "julia", :name "Julia13", :resources {:machine-type "n1-standard-2"}, :type :nextjournal, :docker/environment-image "docker.nextjournal.com/environment@sha256:0e437901f01f7b2e671635b85a04403a2cafcb2e397ca8a6285feb7a3c650c10", :runtime/service-runtimes []}, "929538bc-f7ae-46e1-9bd8-cf623d71d17a" {:compute-ref #uuid "70ededf3-c01f-4750-aeac-c2f31acc0f63", :exec-duration 34948, :id "929538bc-f7ae-46e1-9bd8-cf623d71d17a", :kind "code", :output-log-lines {}, :runtime [:runtime "90436991-2923-44bb-b0d1-f235aec846ef"]}, "b334a484-f5fc-4f38-ab2e-3d9a748c4df4" {:compute-ref #uuid "d6e452df-4365-4860-a5b2-1a1fe667a0b8", :exec-duration 1151, :id "b334a484-f5fc-4f38-ab2e-3d9a748c4df4", :kind "code", :output-log-lines {:stdout 23}, :runtime [:runtime "90436991-2923-44bb-b0d1-f235aec846ef"]}, "cb4442c4-aa31-4afd-9686-0d9bc1785a54" {:compute-ref #uuid "698abde7-34ba-404d-a7c0-6709b8ef8cb9", :exec-duration 284, :id "cb4442c4-aa31-4afd-9686-0d9bc1785a54", :kind "code", :output-log-lines {}, :runtime [:runtime "90436991-2923-44bb-b0d1-f235aec846ef"]}, "d238e3b1-08e9-481d-8d6d-52f2783ae1fd" {:compute-ref #uuid "ddbfc47c-2828-4cec-806e-fa2944a69d1a", :exec-duration 209, :id "d238e3b1-08e9-481d-8d6d-52f2783ae1fd", :kind "code", :output-log-lines {}, :runtime [:runtime "90436991-2923-44bb-b0d1-f235aec846ef"]}, "df65238e-4156-4b9b-9f42-03c3e7656564" {:compute-ref #uuid "86beb891-52ea-4320-b45a-94dc65fe4b80", :exec-duration 7391, :id "df65238e-4156-4b9b-9f42-03c3e7656564", :kind "code", :output-log-lines {}, :runtime [:runtime "90436991-2923-44bb-b0d1-f235aec846ef"]}}, :nextjournal/id #uuid "02d93432-6116-4485-9ef3-246489903c6d", :article/change {:nextjournal/id #uuid "60209204-9e8e-4386-9741-260350b5dbc5"}}} ```