--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/Paper.thy Fri Jan 18 11:40:01 2013 +0000
@@ -0,0 +1,610 @@
+(*<*)
+theory Paper
+imports "../thys/uncomputable"
+begin
+
+(*
+hide_const (open) s
+*)
+
+abbreviation
+ "update2 p a \<equiv> update a p"
+
+consts DUMMY::'a
+
+notation (latex output)
+ Cons ("_::_" [78,77] 73) and
+ set ("") and
+ W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
+ W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
+ update2 ("update") and
+(* abc_lm_v ("lookup") and
+ abc_lm_s ("set") and*)
+ haltP ("stdhalt") and
+ tcopy ("copy") and
+ tape_of_nat_list ("\<ulcorner>_\<urcorner>") and
+ tm_comp ("_ \<oplus> _") 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 take 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 definitions are sets of states together with
+transition functions, all 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 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 \emph{not} ``sufficiently accurate to be directly usable 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
+generalise 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, is 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 are 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. In order
+to construct a universal Turing machine we therefore do not follow
+\cite{AspertiRicciotti12}, instead 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:} We formalised in Isabelle/HOL Turing machines following the
+description of Boolos et al \cite{Boolos87} where tapes only have blank or
+occupied cells. We mechanise the undecidability of the halting problem and
+prove the correctness of concrete Turing machines that are needed
+in this proof; such correctness proofs are left out in the informal literature.
+We construct the universal Turing machine from \cite{Boolos87} by
+relating recursive functions to abacus machines and abacus machines to
+Turing machines. Since we have set up in Isabelle/HOL a very general computability
+model and undecidability result, we are able to formalise the
+undecidability of Wang's tiling problem. We are not aware of any other
+formalisation of a substantial undecidability problem.
+*}
+
+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, abbreviated @{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 or occupied cell
+ whenever the head 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 halting computations and also universal Turing
+ machines. 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) update.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(1)}\\
+ @{thm (lhs) update.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(2)}\\
+ @{thm (lhs) update.simps(3)} & @{text "\<equiv>"} & \\
+ \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) update.simps(3)}}\\
+ @{thm (lhs) update.simps(4)} & @{text "\<equiv>"} & \\
+ \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) update.simps(4)}}\\
+ @{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(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}, respectively. 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 defined in
+ Isabelle/HOL
+ 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 fourth clause for a right move action. The @{term Nop} operation
+ leaves the the tape unchanged (last clause).
+
+ 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 considered 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 uniformly 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 carefully 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: we would need to combine two finite sets of states,
+ possibly renaming states apart whenever both machines share
+ states.\footnote{The usual disjoint union operation in Isabelle/HOL
+ cannot be used as it does not preserve types.} 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 the number of states of the
+ machine. In doing so we can compose two Turing machine by
+ shifting the states of one by an appropriate amount to a higher
+ segment and adjusting some ``next states'' in the other.
+
+ 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 as an example the following Turing machine
+ program, which consists of four instructions
+
+ \begin{equation}
+ \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}
+ \label{dither}
+ \end{equation}
+
+ \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 reads 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 zeroth state is special in that it will be used as the
+ ``halting state''. There are no instructions for the @{text
+ 0}-state, but it will always perform a @{term Nop}-operation and
+ remain in the @{text 0}-state. Unlike Asperti and Riccioti
+ \cite{AspertiRicciotti12}, we have chosen a very concrete
+ representation for programs, because when constructing a universal
+ Turing machine, we need to define a coding function for programs.
+ This can be easily done for our programs-as-lists, but is more
+ difficult for the functions used by Asperti and Ricciotti.
+
+ 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.simps(1)[where b=DUMMY]}}\\
+ @{thm (lhs) fetch.simps(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.simps(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
+ In this definition the function @{term nth_of} returns the @{text n}th element
+ from a list, provided it exists (@{term Some}-case), or if it does not, it
+ returns the default action @{term Nop} and the default state @{text 0}
+ (@{term None}-case). In doing so we slightly deviate from the description
+ in \cite{Boolos87}: if their Turing machines transition to a non-existing
+ state, then the computation is halted. We will transition in such cases
+ to the @{text 0}-state. However, with introducing the
+ notion of \emph{well-formed} Turing machine programs we will later exclude such
+ cases and make the @{text 0}-state the only ``halting state''. A program
+ @{term p} is said to be well-formed if it satisfies
+ the following three properties:
+
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
+ & @{text "\<and>"} & @{term "iseven (length p)"}\\
+ & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The first says that @{text p} must have at least an instruction for the starting
+ state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
+ state, and the third that every next-state is one of the states mentioned in
+ the program or being the @{text 0}-state.
+
+ A \emph{configuration} @{term c} of a Turing machine is a state together with
+ a tape. This is written as @{text "(s, (l, r))"}. If we have a
+ configuration and a program, we can calculate
+ what the next configuration is by fetching the appropriate action and next state
+ from the program, and by updating the state and tape accordingly.
+ This single step of execution is defined as the function @{term tstep}
+
+ \begin{center}
+ \begin{tabular}{l}
+ @{text "step (s, (l, r)) p"} @{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}
+
+ \noindent
+ where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is
+ empty it returns @{term Bk}.
+ It is impossible in Isabelle/HOL to lift the @{term step}-function realising
+ a general evaluation function for Turing machines. The reason is that functions in HOL-based
+ provers need to be terminating, and clearly there are Turing machine
+ programs that are not. We can however define an evaluation
+ function so that it performs exactly @{text n} steps:
+
+ \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}
+
+ \noindent
+ Recall our definition of @{term fetch} with the default value for
+ the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less
+ then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation
+ does not actually halt, but rather transitions to the @{text 0}-state and
+ remains there performing @{text Nop}-actions until @{text n} is reached.
+
+ Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program
+ @{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"}
+
+ \begin{center}
+ \begin{tabular}{l}
+ @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
+ \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ where @{text 1} stands for the starting state and @{text 0} for our final state.
+ A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
+
+ \begin{center}
+ @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
+ \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
+ \end{center}
+
+ \noindent
+ Later on we need to consider specific Turing machines that
+ start with a tape in standard form and halt the computation
+ in standard form. To define a tape in standard form, it is
+ useful to have an operation %@{ term "tape_of_nat_list DUMMY"}
+ that translates lists of natural numbers into tapes.
+
+
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
+ %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
+ %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
+ \end{tabular}
+ \end{center}
+
+
+
+
+ By this we mean
+
+ \begin{center}
+ %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
+ \end{center}
+
+ \noindent
+ This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
+ and the head pointing to the first one; the Turing machine
+ halts with a tape consisting of some @{term Bk}s, followed by a
+ ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
+ The head in the output is pointing again at the first @{term Oc}.
+ The intuitive meaning of this definition is to start the Turing machine with a
+ tape corresponding to a value @{term n} and producing
+ a new tape corresponding to the value @{term l} (the number of @{term Oc}s
+ clustered on the output tape).
+
+ Before we can prove the undecidability of the halting problem for Turing machines,
+ we have to define how to compose two Turing machines. Given our setup, this is
+ relatively straightforward, if slightly fiddly. We use the following two
+ auxiliary functions:
+
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
+ @{thm (lhs) shift.simps} @{text "\<equiv>"}\\
+ \hspace{4mm}@{thm (rhs) shift.simps}\\
+ @{thm (lhs) adjust.simps} @{text "\<equiv>"}\\
+ \hspace{4mm}@{text "map (\<lambda> (a, s)."}\\
+ \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ The first adds @{text n} to all states, exept the @{text 0}-state,
+ thus moving all ``regular'' states to the segment starting at @{text
+ n}; the second adds @{term "length p div 2 + 1"} to the @{text
+ 0}-state, thus ridirecting all references to the ``halting state''
+ to the first state after the program @{text p}. With these two
+ functions in place, we can define the \emph{sequential composition}
+ of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}
+
+ \begin{center}
+ @{thm tm_comp.simps[THEN eq_reflection]}
+ \end{center}
+
+ \noindent
+ This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+ transitioned to the @{text 0}-state, it will in the composed program transition to the starting
+ state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+ have been shifted in order to make sure that the states of the composed
+ program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
+ an initial segment of the natural numbers.
+
+ \begin{center}
+ \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
+ @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
+ \end{tabular}
+ \end{center}
+
+
+ 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.
+
+ 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
+(*>*)
\ No newline at end of file