(*<*)+
−
theory Paper+
−
imports UTM+
−
begin+
−
+
−
hide_const (open) s +
−
+
−
abbreviation +
−
  "update p a == new_tape a p"+
−
+
−
+
−
lemma fetch_def2: +
−
  shows "fetch p 0 b == (Nop, 0)"+
−
  and "fetch p (Suc s) Bk == +
−
     (case nth_of p (2 * s) of+
−
        Some i \<Rightarrow> i+
−
      | None \<Rightarrow> (Nop, 0))"+
−
  and "fetch p (Suc s) Oc == +
−
     (case nth_of p ((2 * s) + 1) of+
−
         Some i \<Rightarrow> i+
−
       | None \<Rightarrow> (Nop, 0))"+
−
apply -+
−
apply(rule_tac [!] eq_reflection)+
−
by (auto split: block.splits simp add: fetch.simps)+
−
+
−
lemma new_tape_def2: +
−
  shows "new_tape W0 (l, r) == (l, Bk#(tl r))" +
−
  and "new_tape W1 (l, r) == (l, Oc#(tl r))"+
−
  and "new_tape L (l, r) == +
−
     (if l = [] then ([], Bk#r) else (tl l, (hd l) # r))" +
−
  and "new_tape R (l, r) ==+
−
     (if r = [] then (Bk#l,[]) else ((hd r)#l, tl r))" +
−
  and "new_tape Nop (l, r) == (l, r)"+
−
apply -+
−
apply(rule_tac [!] eq_reflection)+
−
apply(auto split: taction.splits simp add: new_tape.simps)+
−
done+
−
+
−
+
−
abbreviation +
−
  "read r == if (r = []) then Bk else hd r"+
−
+
−
lemma tstep_def2:+
−
  shows "tstep (s, l, r) p == (let (a, s') = fetch p s (read r) in (s', new_tape a (l, r)))"+
−
apply -+
−
apply(rule_tac [!] eq_reflection)+
−
by (auto split: if_splits prod.split list.split simp add: tstep.simps)+
−
+
−
consts DUMMY::'a+
−
+
−
notation (latex output)+
−
  Cons ("_::_" [78,77] 73) and+
−
  W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and+
−
  W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and+
−
  tstep ("step") and+
−
  steps ("nsteps") and+
−
  abc_lm_v ("lookup") and+
−
  abc_lm_s ("set") and+
−
  DUMMY  ("\<^raw:\mbox{$\_$}>")+
−
+
−
declare [[show_question_marks = false]]+
−
(*>*)+
−
+
−
section {* Introduction *}+
−
+
−
text {*+
−
+
−
\noindent+
−
We formalised in earlier work the correctness proofs for two+
−
algorithms in Isabelle/HOL---one about type-checking in+
−
LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests+
−
in access control~\cite{WuZhangUrban12}.  The formalisations+
−
uncovered a gap in the informal correctness proof of the former and+
−
made us realise that important details were left out in the informal+
−
model for the latter. However, in both cases we were unable to+
−
formalise in Isabelle/HOL computability arguments about the+
−
algorithms. The reason is that both algorithms are formulated in terms+
−
of inductive predicates. Suppose @{text "P"} stands for one such+
−
predicate.  Decidability of @{text P} usually amounts to showing+
−
whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work+
−
in Isabelle/HOL, since it is a theorem prover based on classical logic+
−
where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}+
−
is always provable no matter whether @{text P} is constructed by+
−
computable means. The same problem would arise if we had formulated+
−
the algorithms as recursive functions, because internally in+
−
Isabelle/HOL, like in all HOL-based theorem provers, functions are+
−
represented as inductively defined predicates too.+
−
+
−
The only satisfying way out of this problem in a theorem prover based on classical+
−
logic is to formalise a theory of computability. Norrish provided such+
−
a formalisation for the HOL4 theorem prover. He choose the+
−
$\lambda$-calculus as the starting point for his formalisation+
−
of computability theory,+
−
because of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his+
−
formalisation is a clever infrastructure for reducing+
−
$\lambda$-terms. He also established the computational equivalence+
−
between the $\lambda$-calculus and recursive functions.  Nevertheless he+
−
concluded that it would be ``appealing'' to have formalisations for more+
−
operational models of computations, such as Turing machines or register+
−
machines.  One reason is that many proofs in the literature use +
−
them.  He noted however that in the context of theorem provers+
−
\cite[Page 310]{Norrish11}:+
−
+
−
\begin{quote}+
−
\it``If register machines are unappealing because of their +
−
general fiddliness, Turing machines are an even more +
−
daunting prospect.''+
−
\end{quote}+
−
+
−
\noindent+
−
In this paper we took on this daunting prospect and provide a+
−
formalisation of Turing machines, as well as abacus machines (a kind+
−
of register machines) and recursive functions. To see the difficulties+
−
involved with this work, one has to understand that interactive+
−
theorem provers, like Isabelle/HOL, are at their best when the+
−
data-structures at hand are ``structurally'' defined, like lists,+
−
natural numbers, regular expressions, etc. Such data-structures come+
−
with convenient reasoning infrastructures (for example induction+
−
principles, recursion combinators and so on).  But this is \emph{not}+
−
the case with Turing machines (and also not with register machines):+
−
underlying their definition is a set of states together with a+
−
transition function, both of which are not structurally defined.  This+
−
means we have to implement our own reasoning infrastructure in order+
−
to prove properties about them. This leads to annoyingly fiddly+
−
formalisations.  We noticed first the difference between both,+
−
structural and non-structural, ``worlds'' when formalising the+
−
Myhill-Nerode theorem, where regular expressions fared much better+
−
than automata \cite{WuZhangUrban11}.  However, with Turing machines+
−
there seems to be no alternative if one wants to formalise the great+
−
many proofs from the literature that use them.  We will analyse one+
−
example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The+
−
standard proof of this property uses the notion of \emph{universal+
−
Turing machines}.+
−
+
−
We are not the first who formalised Turing machines in a theorem+
−
prover: we are aware of the preliminary work by Asperti and Ricciotti+
−
\cite{AspertiRicciotti12}. They describe a complete formalisation of+
−
Turing machines in the Matita theorem prover, including a universal+
−
Turing machine. They report that the informal proofs from which they+
−
started are not ``sufficiently accurate to be directly useable as a+
−
guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For+
−
our formalisation we followed mainly the proofs from the textbook+
−
\cite{Boolos87} and found that the description there is quite+
−
detailed. Some details are left out however: for example, it is only+
−
shown how the universal Turing machine is constructed for Turing+
−
machines computing unary functions. We had to figure out a way to+
−
generalize this result to $n$-ary functions. Similarly, when compiling+
−
recursive functions to abacus machines, the textbook again only shows+
−
how it can be done for 2- and 3-ary functions, but in the+
−
formalisation we need arbitrary functions. But the general ideas for+
−
how to do this are clear enough in \cite{Boolos87}. However, one+
−
aspect that is completely left out from the informal description in+
−
\cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turing+
−
machines are correct. We will introduce Hoare-style proof rules+
−
which help us with such correctness arguments of Turing machines.+
−
+
−
The main difference between our formalisation and the one by Asperti+
−
and Ricciotti is that their universal Turing machine uses a different+
−
alphabet than the machines it simulates. They write \cite[Page+
−
23]{AspertiRicciotti12}:+
−
+
−
\begin{quote}\it+
−
``In particular, the fact that the universal machine operates with a+
−
different alphabet with respect to the machines it simulates is+
−
annoying.'' +
−
\end{quote}+
−
+
−
\noindent+
−
In this paper we follow the approach by Boolos et al \cite{Boolos87},+
−
which goes back to Post \cite{Post36}, where all Turing machines+
−
operate on tapes that contain only \emph{blank} or \emph{occupied} cells+
−
(represented by @{term Bk} and @{term Oc}, respectively, in our+
−
formalisation). Traditionally the content of a cell can be any+
−
character from a finite alphabet. Although computationally equivalent,+
−
the more restrictive notion of Turing machines in \cite{Boolos87} makes+
−
the reasoning more uniform. In addition some proofs \emph{about} Turing+
−
machines will be simpler.  The reason is that one often needs to encode+
−
Turing machines---consequently if the Turing machines are simpler, then the coding+
−
functions are simpler too. Unfortunately, the restrictiveness also makes+
−
it harder to design programs for these Turing machines. Therefore in order+
−
to construct a \emph{universal Turing machine} we follow the proof in+
−
\cite{Boolos87} by relating abacus machines to Turing machines and in+
−
turn recursive functions to abacus machines. The universal Turing+
−
machine can then be constructed as a recursive function.+
−
+
−
\smallskip+
−
\noindent+
−
{\bf Contributions:} +
−
+
−
*}+
−
+
−
section {* Turing Machines *}+
−
+
−
text {* \noindent+
−
  Turing machines can be thought of as having a read-write-unit, also+
−
  referred to as \emph{head},+
−
  ``gliding'' over a potentially infinite tape. Boolos et+
−
  al~\cite{Boolos87} only consider tapes with cells being either blank+
−
  or occupied, which we represent by a datatype having two+
−
  constructors, namely @{text Bk} and @{text Oc}.  One way to+
−
  represent such tapes is to use a pair of lists, written @{term "(l,+
−
  r)"}, where @{term l} stands for the tape on the left-hand side of the+
−
  head and @{term r} for the tape on the right-hand side. We have the+
−
  convention that the head, written @{term hd}, of the right-list is+
−
  the cell on which the head of the Turing machine currently operates. This can+
−
  be pictured as follows:+
−
+
−
  \begin{center}+
−
  \begin{tikzpicture}+
−
  \draw[very thick] (-3.0,0)   -- ( 3.0,0);+
−
  \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);+
−
  \draw[very thick] (-0.25,0)   -- (-0.25,0.5);+
−
  \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);+
−
  \draw[very thick] (-0.75,0)   -- (-0.75,0.5);+
−
  \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);+
−
  \draw[very thick] (-1.25,0)   -- (-1.25,0.5);+
−
  \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);+
−
  \draw[very thick] (-1.75,0)   -- (-1.75,0.5);+
−
  \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);+
−
  \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);+
−
  \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);+
−
  \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);+
−
  \draw[fill]     (-0.35,0.1) rectangle (-0.65,0.4);+
−
  \draw (-0.25,0.8) -- (-0.25,-0.8);+
−
  \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);+
−
  \node [anchor=base] at (-0.8,-0.5) {\small left list};+
−
  \node [anchor=base] at (0.35,-0.5) {\small right list};+
−
  \node [anchor=base] at (0.1,0.7) {\small head};+
−
  \node [anchor=base] at (-2.2,0.2) {\ldots};+
−
  \node [anchor=base] at ( 2.3,0.2) {\ldots};+
−
  \end{tikzpicture}+
−
  \end{center}+
−
  +
−
  \noindent+
−
  Note that by using lists each side of the tape is only finite. The+
−
  potential infinity is achieved by adding an appropriate blank cell +
−
  whenever the read-write unit goes over the ``edge'' of the tape. To +
−
  make this formal we define five possible \emph{actions} +
−
  the Turing machine can perform:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{rcll}+
−
  @{text "a"} & $::=$  & @{term "W0"} & write blank (@{term Bk})\\+
−
  & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\+
−
  & $\mid$ & @{term L} & move left\\+
−
  & $\mid$ & @{term R} & move right\\+
−
  & $\mid$ & @{term Nop} & do-nothing operation\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  We slightly deviate+
−
  from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use+
−
  will become important when we formalise universal Turing +
−
  machines later. Given a tape and an action, we can define the+
−
  following tape updating function:+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}+
−
  @{thm (lhs) new_tape_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(1)}\\+
−
  @{thm (lhs) new_tape_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(2)}\\+
−
  @{thm (lhs) new_tape_def2(3)} & @{text "\<equiv>"} & \\+
−
  \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\+
−
  @{thm (lhs) new_tape_def2(4)} & @{text "\<equiv>"} & \\+
−
  \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\+
−
  @{thm (lhs) new_tape_def2(5)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(5)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The first two clauses replace the head of the right-list+
−
  with a new @{term Bk} or @{term Oc}, repsectively. To see that+
−
  these two clauses make sense in case where @{text r} is the empty+
−
  list, one has to know that the tail function, @{term tl}, is in+
−
  Isabelle/HOL defined+
−
  such that @{term "tl [] == []"} holds. The third clause +
−
  implements the move of the head one step to the left: we need+
−
  to test if the left-list @{term l} is empty; if yes, then we just prepend a +
−
  blank cell to the right-list; otherwise we have to remove the+
−
  head from the left-list and prepend it to the right-list. Similarly+
−
  in the clause for a right move action. The @{term Nop} operation+
−
  leaves the the tape unchanged.+
−
+
−
  Note that our treatment of the tape is rather ``unsymmetric''---we+
−
  have the convention that the head of the right-list is where the+
−
  head is currently positioned. Asperti and Ricciotti+
−
  \cite{AspertiRicciotti12} also consider such a representation, but+
−
  dismiss it as it complicates their definition for \emph{tape+
−
  equality}. The reason is that moving the head one step to+
−
  the left and then back to the right might change the tape (in case+
−
  of going over the ``edge''). Therefore they distinguish four types+
−
  of tapes: one where the tape is empty; another where the head+
−
  is on the left edge, respectively right edge, and in the middle+
−
  of the tape. The reading, writing and moving of the tape is then+
−
  defined in terms of these four cases.  In this way they can keep the+
−
  tape in a ``normalised'' form, and thus making a left-move followed+
−
  by a right-move being the identity on tapes. Since we are not using+
−
  the notion of tape equality, we can get away with the unsymmetric+
−
  definition above, and by using the @{term update} function+
−
  cover uniformely all cases including corner cases.+
−
+
−
  Next we need to define the \emph{states} of a Turing machine.  Given+
−
  how little is usually said about how to represent them in informal+
−
  presentations, it might be surprising that in a theorem prover we have +
−
  to select carfully a representation. If we use the naive representation+
−
  where a Turing machine consists of a finite set of states, then we+
−
  will have difficulties composing two Turing machines. In this case we +
−
  would need to combine two finite sets of states, possibly requiring +
−
  renaming states apart whenever both machines share states. This +
−
  renaming can be quite cumbersome to reason about. Therefore we made +
−
  the choice of representing a state by a natural number and the states +
−
  of a Turing machine will always consist of the initial segment+
−
  of natural numbers starting from @{text 0} up to number of states+
−
  of the machine minus @{text 1}. In doing so we can compose+
−
  two Turing machine by ``shifting'' the states of one by an appropriate+
−
  amount to a higher segment and adjust some ``next states''.+
−
+
−
  An \emph{instruction} @{term i} of a Turing machine is a pair consisting of +
−
  an action and a natural number (the next state). A \emph{program} @{term p} of a Turing+
−
  machine is then a list of such pairs. Using the following Turing machine+
−
  program (consisting of four instructions) as an example+
−
+
−
  \begin{center}+
−
  \begin{tikzpicture}+
−
  \node [anchor=base] at (0,0) {@{thm dither_def}};+
−
  \node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};+
−
  \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};+
−
  \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};+
−
  \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};+
−
  \end{tikzpicture}+
−
  \end{center}+
−
+
−
  \noindent+
−
  the reader can see we have organised our Turing machine programs so +
−
  that segments of two belong to a state. The first component +
−
  of the segment determines what action should be taken and which next+
−
  state should be transitioned to in case the head read a @{term Bk};+
−
  similarly the second component determines what should be done in+
−
  case of reading @{term Oc}. We have the convention that the+
−
  first state is always the \emph{starting state} of the Turing machine. +
−
  The 0-state is special in that it will be used as \emph{halting state}.+
−
  There are no instructions for the 0-state, but it will always +
−
  perform a @{term Nop}-operation and remain in the 0-state.+
−
+
−
  Given a program @{term p}, a state+
−
  and the cell being read by the head, we need to fetch+
−
  the corresponding instruction from the program. For this we define +
−
  the function @{term fetch}+
−
 +
−
  \begin{center}+
−
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}+
−
  \multicolumn{3}{l}{@{thm fetch_def2(1)[where b=DUMMY]}}\\+
−
  @{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\+
−
  \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\+
−
  \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\+
−
  \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}\\+
−
  @{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\+
−
  \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\+
−
  \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\+
−
  \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
+
−
+
−
  A \emph{configuration} @{term c} of a Turing machine is a state together with +
−
  a tape. This is written as the triple @{term "(s, l, r)"}. If we have a +
−
  configuration and a program, we can calculate+
−
  what the next configuration is by fetching the appropriate next state+
−
  and action from the program. Such a single step of execution can be defined as+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l}+
−
  @{thm (lhs) tstep_def2(1)} @{text "\<equiv>"}\\+
−
  \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\+
−
  \hspace{10mm}@{text "in (s', update (l, r) a)"}+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  No evaluator in HOL, because of totality.+
−
+
−
  \begin{center}+
−
  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}+
−
  @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\+
−
  @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \emph{well-formedness} of a Turing program+
−
+
−
  programs halts+
−
+
−
  shift and change of a p+
−
+
−
  composition of two ps+
−
+
−
  assertion holds for all tapes+
−
+
−
  Hoare rule for composition+
−
+
−
  For showing the undecidability of the halting problem, we need to consider+
−
  two specific Turing machines. copying TM and dithering TM+
−
+
−
  correctness of the copying TM+
−
+
−
  measure for the copying TM, which we however omit.+
−
+
−
  standard configuration+
−
+
−
  halting problem+
−
*}+
−
+
−
section {* Abacus Machines *}+
−
+
−
text {*+
−
  \noindent+
−
  Boolos et al \cite{Boolos87} use abacus machines as a +
−
  stepping stone for making it less laborious to write+
−
  programs for Turing machines. Abacus machines operate+
−
  over an unlimited number of registers $R_0$, $R_1$, \ldots+
−
  each being able to hold an arbitrary large natural number.+
−
  We use natural numbers to refer to registers, but also+
−
  to refer to \emph{opcodes} of abacus +
−
  machines. Obcodes are given by the datatype+
−
+
−
  \begin{center}+
−
  \begin{tabular}{rcll}+
−
  @{text "o"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\+
−
  & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\+
−
  & & & then decrement it by one\\+
−
  & & & otherwise jump to opcode $o$\\+
−
  & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
  \noindent+
−
  A \emph{program} of an abacus machine is a list of such+
−
  obcodes. For example the program clearing the register+
−
  $R$ (setting it to 0) can be defined as follows:+
−
+
−
  \begin{center}+
−
  @{thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}+
−
  \end{center}+
−
+
−
  \noindent+
−
  The second opcode @{term "Goto 0"} in this programm means we +
−
  jump back to the first opcode, namely @{text "Dec R o"}.+
−
  The \emph{memory} $m$ of an abacus machine holding the values+
−
  of the registers is represented as a list of natural numbers.+
−
  We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},+
−
  which looks up the content of register $R$; if $R$+
−
  is not in this list, then we return 0. Similarly we+
−
  have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which+
−
  sets the value of $R$ to $n$, and if $R$ was not yet in $m$+
−
  it pads it approriately with 0s.+
−
+
−
+
−
  Abacus machine halts when it jumps out of range.+
−
*}+
−
+
−
+
−
section {* Recursive Functions *}+
−
+
−
section {* Wang Tiles\label{Wang} *}+
−
+
−
text {*+
−
  Used in texture mapings - graphics+
−
*}+
−
+
−
+
−
section {* Related Work *}+
−
+
−
text {*+
−
  The most closely related work is by Norrish \cite{Norrish11}, and Asperti and +
−
  Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on +
−
  lambda-terms. For this he introduced a clever rewriting technology+
−
  based on combinators and de-Bruijn indices for+
−
  rewriting modulo $\beta$-equivalence (to keep it manageable)+
−
*}+
−
+
−
+
−
(*+
−
Questions:+
−
+
−
Can this be done: Ackerman function is not primitive +
−
recursive (Nora Szasz)+
−
+
−
Tape is represented as two lists (finite - usually infinite tape)?+
−
+
−
*)+
−
+
−
+
−
(*<*)+
−
end+
−
(*>*)+
−