1 (*<*)

     2 theory Paper

     3 imports "../thys/uncomputable"

     4 begin

     5 

     6 (*

     7 hide_const (open) s 

     8 *)

     9 

    10 abbreviation

    11   "update2 p a \<equiv> update a p"

    12 

    13 consts DUMMY::'a

    14 

    15 notation (latex output)

    16   Cons ("_::_" [78,77] 73) and

    17   set ("") and

    18   W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and

    19   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and

    20   update2 ("update") and

    21 (*  abc_lm_v ("lookup") and

    22   abc_lm_s ("set") and*)

    23   haltP ("stdhalt") and 

    24   tcopy ("copy") and 

    25   tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 

    26   tm_comp ("_ \<oplus> _") and 

    27   DUMMY  ("\<^raw:\mbox{$\_$}>")

    28 

    29 declare [[show_question_marks = false]]

    30 (*>*)

    31 

    32 section {* Introduction *}

    33 

    34 text {*

    35 

    36 \noindent

    37 We formalised in earlier work the correctness proofs for two

    38 algorithms in Isabelle/HOL---one about type-checking in

    39 LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests

    40 in access control~\cite{WuZhangUrban12}.  The formalisations

    41 uncovered a gap in the informal correctness proof of the former and

    42 made us realise that important details were left out in the informal

    43 model for the latter. However, in both cases we were unable to

    44 formalise in Isabelle/HOL computability arguments about the

    45 algorithms. The reason is that both algorithms are formulated in terms

    46 of inductive predicates. Suppose @{text "P"} stands for one such

    47 predicate.  Decidability of @{text P} usually amounts to showing

    48 whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work

    49 in Isabelle/HOL, since it is a theorem prover based on classical logic

    50 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}

    51 is always provable no matter whether @{text P} is constructed by

    52 computable means. The same problem would arise if we had formulated

    53 the algorithms as recursive functions, because internally in

    54 Isabelle/HOL, like in all HOL-based theorem provers, functions are

    55 represented as inductively defined predicates too.

    56 

    57 The only satisfying way out of this problem in a theorem prover based on classical

    58 logic is to formalise a theory of computability. Norrish provided such

    59 a formalisation for the HOL4 theorem prover. He choose the

    60 $\lambda$-calculus as the starting point for his formalisation

    61 of computability theory,

    62 because of its ``simplicity'' \cite[Page 297]{Norrish11}.  Part of his

    63 formalisation is a clever infrastructure for reducing

    64 $\lambda$-terms. He also established the computational equivalence

    65 between the $\lambda$-calculus and recursive functions.  Nevertheless he

    66 concluded that it would be ``appealing'' to have formalisations for more

    67 operational models of computations, such as Turing machines or register

    68 machines.  One reason is that many proofs in the literature use 

    69 them.  He noted however that in the context of theorem provers

    70 \cite[Page 310]{Norrish11}:

    71 

    72 \begin{quote}

    73 \it``If register machines are unappealing because of their 

    74 general fiddliness, Turing machines are an even more 

    75 daunting prospect.''

    76 \end{quote}

    77 

    78 \noindent

    79 In this paper we take on this daunting prospect and provide a

    80 formalisation of Turing machines, as well as abacus machines (a kind

    81 of register machines) and recursive functions. To see the difficulties

    82 involved with this work, one has to understand that interactive

    83 theorem provers, like Isabelle/HOL, are at their best when the

    84 data-structures at hand are ``structurally'' defined, like lists,

    85 natural numbers, regular expressions, etc. Such data-structures come

    86 with convenient reasoning infrastructures (for example induction

    87 principles, recursion combinators and so on).  But this is \emph{not}

    88 the case with Turing machines (and also not with register machines):

    89 underlying their definitions are sets of states together with 

    90 transition functions, all of which are not structurally defined.  This

    91 means we have to implement our own reasoning infrastructure in order

    92 to prove properties about them. This leads to annoyingly fiddly

    93 formalisations.  We noticed first the difference between both,

    94 structural and non-structural, ``worlds'' when formalising the

    95 Myhill-Nerode theorem, where regular expressions fared much better

    96 than automata \cite{WuZhangUrban11}.  However, with Turing machines

    97 there seems to be no alternative if one wants to formalise the great

    98 many proofs from the literature that use them.  We will analyse one

    99 example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The

   100 standard proof of this property uses the notion of universal

   101 Turing machines.

   102 

   103 We are not the first who formalised Turing machines in a theorem

   104 prover: we are aware of the preliminary work by Asperti and Ricciotti

   105 \cite{AspertiRicciotti12}. They describe a complete formalisation of

   106 Turing machines in the Matita theorem prover, including a universal

   107 Turing machine. They report that the informal proofs from which they

   108 started are \emph{not} ``sufficiently accurate to be directly usable as a

   109 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For

   110 our formalisation we followed mainly the proofs from the textbook

   111 \cite{Boolos87} and found that the description there is quite

   112 detailed. Some details are left out however: for example, it is only

   113 shown how the universal Turing machine is constructed for Turing

   114 machines computing unary functions. We had to figure out a way to

   115 generalise this result to $n$-ary functions. Similarly, when compiling

   116 recursive functions to abacus machines, the textbook again only shows

   117 how it can be done for 2- and 3-ary functions, but in the

   118 formalisation we need arbitrary functions. But the general ideas for

   119 how to do this are clear enough in \cite{Boolos87}. However, one

   120 aspect that is completely left out from the informal description in

   121 \cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing

   122 machines are correct. We will introduce Hoare-style proof rules

   123 which help us with such correctness arguments of Turing machines.

   124 

   125 The main difference between our formalisation and the one by Asperti

   126 and Ricciotti is that their universal Turing machine uses a different

   127 alphabet than the machines it simulates. They write \cite[Page

   128 23]{AspertiRicciotti12}:

   129 

   130 \begin{quote}\it

   131 ``In particular, the fact that the universal machine operates with a

   132 different alphabet with respect to the machines it simulates is

   133 annoying.'' 

   134 \end{quote}

   135 

   136 \noindent

   137 In this paper we follow the approach by Boolos et al \cite{Boolos87},

   138 which goes back to Post \cite{Post36}, where all Turing machines

   139 operate on tapes that contain only \emph{blank} or \emph{occupied} cells

   140 (represented by @{term Bk} and @{term Oc}, respectively, in our

   141 formalisation). Traditionally the content of a cell can be any

   142 character from a finite alphabet. Although computationally equivalent,

   143 the more restrictive notion of Turing machines in \cite{Boolos87} makes

   144 the reasoning more uniform. In addition some proofs \emph{about} Turing

   145 machines are simpler.  The reason is that one often needs to encode

   146 Turing machines---consequently if the Turing machines are simpler, then the coding

   147 functions are simpler too. Unfortunately, the restrictiveness also makes

   148 it harder to design programs for these Turing machines. In order

   149 to construct a universal Turing machine we therefore do not follow 

   150 \cite{AspertiRicciotti12}, instead follow the proof in

   151 \cite{Boolos87} by relating abacus machines to Turing machines and in

   152 turn recursive functions to abacus machines. The universal Turing

   153 machine can then be constructed as a recursive function.

   154 

   155 \smallskip

   156 \noindent

   157 {\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the

   158 description of Boolos et al \cite{Boolos87} where tapes only have blank or

   159 occupied cells. We mechanise the undecidability of the halting problem and

   160 prove the correctness of concrete Turing machines that are needed

   161 in this proof; such correctness proofs are left out in the informal literature.  

   162 We construct the universal Turing machine from \cite{Boolos87} by

   163 relating recursive functions to abacus machines and abacus machines to

   164 Turing machines. Since we have set up in Isabelle/HOL a very general computability

   165 model and undecidability result, we are able to formalise the

   166 undecidability of Wang's tiling problem. We are not aware of any other

   167 formalisation of a substantial undecidability problem.

   168 *}

   169 

   170 section {* Turing Machines *}

   171 

   172 text {* \noindent

   173   Turing machines can be thought of as having a read-write-unit, also

   174   referred to as \emph{head},

   175   ``gliding'' over a potentially infinite tape. Boolos et

   176   al~\cite{Boolos87} only consider tapes with cells being either blank

   177   or occupied, which we represent by a datatype having two

   178   constructors, namely @{text Bk} and @{text Oc}.  One way to

   179   represent such tapes is to use a pair of lists, written @{term "(l,

   180   r)"}, where @{term l} stands for the tape on the left-hand side of the

   181   head and @{term r} for the tape on the right-hand side. We have the

   182   convention that the head, abbreviated @{term hd}, of the right-list is

   183   the cell on which the head of the Turing machine currently operates. This can

   184   be pictured as follows:

   185 

   186   \begin{center}

   187   \begin{tikzpicture}

   188   \draw[very thick] (-3.0,0)   -- ( 3.0,0);

   189   \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);

   190   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

   191   \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

   192   \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

   193   \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

   194   \draw[very thick] (-1.25,0)   -- (-1.25,0.5);

   195   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

   196   \draw[very thick] (-1.75,0)   -- (-1.75,0.5);

   197   \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);

   198   \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

   199   \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);

   200   \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);

   201   \draw[fill]     (-0.35,0.1) rectangle (-0.65,0.4);

   202   \draw (-0.25,0.8) -- (-0.25,-0.8);

   203   \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);

   204   \node [anchor=base] at (-0.8,-0.5) {\small left list};

   205   \node [anchor=base] at (0.35,-0.5) {\small right list};

   206   \node [anchor=base] at (0.1,0.7) {\small head};

   207   \node [anchor=base] at (-2.2,0.2) {\ldots};

   208   \node [anchor=base] at ( 2.3,0.2) {\ldots};

   209   \end{tikzpicture}

   210   \end{center}

   211   

   212   \noindent

   213   Note that by using lists each side of the tape is only finite. The

   214   potential infinity is achieved by adding an appropriate blank or occupied cell 

   215   whenever the head goes over the ``edge'' of the tape. To 

   216   make this formal we define five possible \emph{actions} 

   217   the Turing machine can perform:

   218 

   219   \begin{center}

   220   \begin{tabular}{rcll}

   221   @{text "a"} & $::=$  & @{term "W0"} & write blank (@{term Bk})\\

   222   & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\

   223   & $\mid$ & @{term L} & move left\\

   224   & $\mid$ & @{term R} & move right\\

   225   & $\mid$ & @{term Nop} & do-nothing operation\\

   226   \end{tabular}

   227   \end{center}

   228 

   229   \noindent

   230   We slightly deviate

   231   from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use

   232   will become important when we formalise halting computations and also universal Turing 

   233   machines. Given a tape and an action, we can define the

   234   following tape updating function:

   235 

   236   \begin{center}

   237   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   238   @{thm (lhs) update.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(1)}\\

   239   @{thm (lhs) update.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(2)}\\

   240   @{thm (lhs) update.simps(3)} & @{text "\<equiv>"} & \\

   241   \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) update.simps(3)}}\\

   242   @{thm (lhs) update.simps(4)} & @{text "\<equiv>"} & \\

   243   \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) update.simps(4)}}\\

   244   @{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(5)}\\

   245   \end{tabular}

   246   \end{center}

   247 

   248   \noindent

   249   The first two clauses replace the head of the right-list

   250   with a new @{term Bk} or @{term Oc}, respectively. To see that

   251   these two clauses make sense in case where @{text r} is the empty

   252   list, one has to know that the tail function, @{term tl}, is defined in

   253   Isabelle/HOL

   254   such that @{term "tl [] == []"} holds. The third clause 

   255   implements the move of the head one step to the left: we need

   256   to test if the left-list @{term l} is empty; if yes, then we just prepend a 

   257   blank cell to the right-list; otherwise we have to remove the

   258   head from the left-list and prepend it to the right-list. Similarly

   259   in the fourth clause for a right move action. The @{term Nop} operation

   260   leaves the the tape unchanged (last clause).

   261 

   262   Note that our treatment of the tape is rather ``unsymmetric''---we

   263   have the convention that the head of the right-list is where the

   264   head is currently positioned. Asperti and Ricciotti

   265   \cite{AspertiRicciotti12} also considered such a representation, but

   266   dismiss it as it complicates their definition for \emph{tape

   267   equality}. The reason is that moving the head one step to

   268   the left and then back to the right might change the tape (in case

   269   of going over the ``edge''). Therefore they distinguish four types

   270   of tapes: one where the tape is empty; another where the head

   271   is on the left edge, respectively right edge, and in the middle

   272   of the tape. The reading, writing and moving of the tape is then

   273   defined in terms of these four cases.  In this way they can keep the

   274   tape in a ``normalised'' form, and thus making a left-move followed

   275   by a right-move being the identity on tapes. Since we are not using

   276   the notion of tape equality, we can get away with the unsymmetric

   277   definition above, and by using the @{term update} function

   278   cover uniformly all cases including corner cases.

   279 

   280   Next we need to define the \emph{states} of a Turing machine.  Given

   281   how little is usually said about how to represent them in informal

   282   presentations, it might be surprising that in a theorem prover we

   283   have to select carefully a representation. If we use the naive

   284   representation where a Turing machine consists of a finite set of

   285   states, then we will have difficulties composing two Turing

   286   machines: we would need to combine two finite sets of states,

   287   possibly renaming states apart whenever both machines share

   288   states.\footnote{The usual disjoint union operation in Isabelle/HOL

   289   cannot be used as it does not preserve types.} This renaming can be

   290   quite cumbersome to reason about. Therefore we made the choice of

   291   representing a state by a natural number and the states of a Turing

   292   machine will always consist of the initial segment of natural

   293   numbers starting from @{text 0} up to the number of states of the

   294   machine. In doing so we can compose two Turing machine by

   295   shifting the states of one by an appropriate amount to a higher

   296   segment and adjusting some ``next states'' in the other.

   297 

   298   An \emph{instruction} @{term i} of a Turing machine is a pair consisting of 

   299   an action and a natural number (the next state). A \emph{program} @{term p} of a Turing

   300   machine is then a list of such pairs. Using as an example the following Turing machine

   301   program, which consists of four instructions

   302 

   303   \begin{equation}

   304   \begin{tikzpicture}

   305   \node [anchor=base] at (0,0) {@{thm dither_def}};

   306   \node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};

   307   \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};

   308   \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};

   309   \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};

   310   \end{tikzpicture}

   311   \label{dither}

   312   \end{equation}

   313 

   314   \noindent

   315   the reader can see we have organised our Turing machine programs so

   316   that segments of two belong to a state. The first component of the

   317   segment determines what action should be taken and which next state

   318   should be transitioned to in case the head reads a @{term Bk};

   319   similarly the second component determines what should be done in

   320   case of reading @{term Oc}. We have the convention that the first

   321   state is always the \emph{starting state} of the Turing machine.

   322   The zeroth state is special in that it will be used as the

   323   ``halting state''.  There are no instructions for the @{text

   324   0}-state, but it will always perform a @{term Nop}-operation and

   325   remain in the @{text 0}-state.  Unlike Asperti and Riccioti

   326   \cite{AspertiRicciotti12}, we have chosen a very concrete

   327   representation for programs, because when constructing a universal

   328   Turing machine, we need to define a coding function for programs.

   329   This can be easily done for our programs-as-lists, but is more

   330   difficult for the functions used by Asperti and Ricciotti.

   331 

   332   Given a program @{term p}, a state

   333   and the cell being read by the head, we need to fetch

   334   the corresponding instruction from the program. For this we define 

   335   the function @{term fetch}

   336  

   337   \begin{center}

   338   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   339   \multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\

   340   @{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & \\

   341   \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\

   342   \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\

   343   \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}\\

   344   @{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & \\

   345   \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\

   346   \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\

   347   \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}

   348   \end{tabular}

   349   \end{center}

   350 

   351   \noindent

   352   In this definition the function @{term nth_of} returns the @{text n}th element

   353   from a list, provided it exists (@{term Some}-case), or if it does not, it

   354   returns the default action @{term Nop} and the default state @{text 0} 

   355   (@{term None}-case). In doing so we slightly deviate from the description

   356   in \cite{Boolos87}: if their Turing machines transition to a non-existing

   357   state, then the computation is halted. We will transition in such cases

   358   to the @{text 0}-state. However, with introducing the

   359   notion of \emph{well-formed} Turing machine programs we will later exclude such

   360   cases and make the  @{text 0}-state the only ``halting state''. A program 

   361   @{term p} is said to be well-formed if it satisfies

   362   the following three properties:

   363 

   364   \begin{center}

   365   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   366   @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\

   367                         & @{text "\<and>"} & @{term "iseven (length p)"}\\

   368                         & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}

   369   \end{tabular}

   370   \end{center}

   371 

   372   \noindent

   373   The first says that @{text p} must have at least an instruction for the starting 

   374   state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every 

   375   state, and the third that every next-state is one of the states mentioned in

   376   the program or being the @{text 0}-state.

   377 

   378   A \emph{configuration} @{term c} of a Turing machine is a state together with 

   379   a tape. This is written as @{text "(s, (l, r))"}. If we have a 

   380   configuration and a program, we can calculate

   381   what the next configuration is by fetching the appropriate action and next state

   382   from the program, and by updating the state and tape accordingly. 

   383   This single step of execution is defined as the function @{term tstep}

   384 

   385   \begin{center}

   386   \begin{tabular}{l}

   387   @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\

   388   \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\

   389   \hspace{10mm}@{text "in (s', update (l, r) a)"}

   390   \end{tabular}

   391   \end{center}

   392 

   393   \noindent

   394   where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is

   395   empty it returns @{term Bk}.

   396   It is impossible in Isabelle/HOL to lift the @{term step}-function realising

   397   a general evaluation function for Turing machines. The reason is that functions in HOL-based

   398   provers need to be terminating, and clearly there are Turing machine 

   399   programs that are not. We can however define an evaluation

   400   function so that it performs exactly @{text n} steps:

   401 

   402   \begin{center}

   403   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   404   @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\

   405   @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\

   406   \end{tabular}

   407   \end{center}

   408 

   409   \noindent

   410   Recall our definition of @{term fetch} with the default value for

   411   the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less 

   412   then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation

   413   does not actually halt, but rather transitions to the @{text 0}-state and 

   414   remains there performing @{text Nop}-actions until @{text n} is reached. 

   415 

   416   Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program 

   417   @{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}

   418 

   419   \begin{center}

   420   \begin{tabular}{l}

   421   @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\

   422   \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}

   423   \end{tabular}

   424   \end{center}

   425 

   426   \noindent

   427   where @{text 1} stands for the starting state and @{text 0} for our final state.

   428   A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff

   429 

   430   \begin{center}

   431   @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>

   432   \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}

   433   \end{center}

   434 

   435   \noindent

   436   Later on we need to consider specific Turing machines that 

   437   start with a tape in standard form and halt the computation

   438   in standard form. To define a tape in standard form, it is

   439   useful to have an operation %@{ term "tape_of_nat_list DUMMY"} 

   440   that translates lists of natural numbers into tapes. 

   441 

   442   

   443   \begin{center}

   444   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   445   %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\

   446   %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\

   447   %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\

   448   \end{tabular}

   449   \end{center}

   450 

   451   

   452 

   453 

   454   By this we mean

   455 

   456   \begin{center}

   457   %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}

   458   \end{center}

   459 

   460   \noindent

   461   This means the Turing machine starts with a tape containg @{text n} @{term Oc}s

   462   and the head pointing to the first one; the Turing machine

   463   halts with a tape consisting of some @{term Bk}s, followed by a 

   464   ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.

   465   The head in the output is pointing again at the first @{term Oc}.

   466   The intuitive meaning of this definition is to start the Turing machine with a

   467   tape corresponding to a value @{term n} and producing

   468   a new tape corresponding to the value @{term l} (the number of @{term Oc}s

   469   clustered on the output tape).

   470 

   471   Before we can prove the undecidability of the halting problem for Turing machines, 

   472   we have to define how to compose two Turing machines. Given our setup, this is 

   473   relatively straightforward, if slightly fiddly. We use the following two

   474   auxiliary functions:

   475 

   476   \begin{center}

   477   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

   478   @{thm (lhs) shift.simps} @{text "\<equiv>"}\\

   479   \hspace{4mm}@{thm (rhs) shift.simps}\\

   480   @{thm (lhs) adjust.simps} @{text "\<equiv>"}\\

   481   \hspace{4mm}@{text "map (\<lambda> (a, s)."}\\

   482   \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\

   483   \end{tabular}

   484   \end{center}

   485 

   486   \noindent

   487   The first adds @{text n} to all states, exept the @{text 0}-state,

   488   thus moving all ``regular'' states to the segment starting at @{text

   489   n}; the second adds @{term "length p div 2 + 1"} to the @{text

   490   0}-state, thus ridirecting all references to the ``halting state''

   491   to the first state after the program @{text p}.  With these two

   492   functions in place, we can define the \emph{sequential composition}

   493   of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}

   494 

   495   \begin{center}

   496   @{thm tm_comp.simps[THEN eq_reflection]}

   497   \end{center}

   498 

   499   \noindent

   500   This means @{text "p\<^isub>1"} is executed first. Whenever it originally

   501   transitioned to the @{text 0}-state, it will in the composed program transition to the starting

   502   state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}

   503   have been shifted in order to make sure that the states of the composed 

   504   program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' 

   505   an initial segment of the natural numbers.

   506 

   507   \begin{center}

   508   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}

   509   @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}

   510   \end{tabular}

   511   \end{center}

   512 

   513 

   514   assertion holds for all tapes

   515 

   516   Hoare rule for composition

   517 

   518   For showing the undecidability of the halting problem, we need to consider

   519   two specific Turing machines. copying TM and dithering TM

   520 

   521   correctness of the copying TM

   522 

   523   measure for the copying TM, which we however omit.

   524 

   525   halting problem

   526 *}

   527 

   528 section {* Abacus Machines *}

   529 

   530 text {*

   531   \noindent

   532   Boolos et al \cite{Boolos87} use abacus machines as a 

   533   stepping stone for making it less laborious to write

   534   programs for Turing machines. Abacus machines operate

   535   over an unlimited number of registers $R_0$, $R_1$, \ldots

   536   each being able to hold an arbitrary large natural number.

   537   We use natural numbers to refer to registers, but also

   538   to refer to \emph{opcodes} of abacus 

   539   machines. Obcodes are given by the datatype

   540 

   541   \begin{center}

   542   \begin{tabular}{rcll}

   543   @{text "o"} & $::=$  & @{term "Inc R\<iota>"} & increment register $R$ by one\\

   544   & $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\

   545   & & & then decrement it by one\\

   546   & & & otherwise jump to opcode $o$\\

   547   & $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$

   548   \end{tabular}

   549   \end{center}

   550 

   551   \noindent

   552   A \emph{program} of an abacus machine is a list of such

   553   obcodes. For example the program clearing the register

   554   $R$ (setting it to 0) can be defined as follows:

   555 

   556   \begin{center}

   557   %@ {thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}

   558   \end{center}

   559 

   560   \noindent

   561   The second opcode @{term "Goto 0"} in this programm means we 

   562   jump back to the first opcode, namely @{text "Dec R o"}.

   563   The \emph{memory} $m$ of an abacus machine holding the values

   564   of the registers is represented as a list of natural numbers.

   565   We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},

   566   which looks up the content of register $R$; if $R$

   567   is not in this list, then we return 0. Similarly we

   568   have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which

   569   sets the value of $R$ to $n$, and if $R$ was not yet in $m$

   570   it pads it approriately with 0s.

   571 

   572 

   573   Abacus machine halts when it jumps out of range.

   574 *}

   575 

   576 

   577 section {* Recursive Functions *}

   578 

   579 section {* Wang Tiles\label{Wang} *}

   580 

   581 text {*

   582   Used in texture mapings - graphics

   583 *}

   584 

   585 

   586 section {* Related Work *}

   587 

   588 text {*

   589   The most closely related work is by Norrish \cite{Norrish11}, and Asperti and 

   590   Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on 

   591   lambda-terms. For this he introduced a clever rewriting technology

   592   based on combinators and de-Bruijn indices for

   593   rewriting modulo $\beta$-equivalence (to keep it manageable)

   594 *}

   595 

   596 

   597 (*

   598 Questions:

   599 

   600 Can this be done: Ackerman function is not primitive 

   601 recursive (Nora Szasz)

   602 

   603 Tape is represented as two lists (finite - usually infinite tape)?

   604 

   605 *)

   606 

   607 

   608 (*<*)

   609 end

   610 (*>*)