1 (*<*)

     2 theory Paper

     3 imports "../thys/UTM" "../thys/Abacus_Defs"

     4 begin

     5 

     6 (*

     7 value "map (steps (1,[],[Oc]) ([(L,0),(L,2),(R,2),(R,0)],0)) [0 ..< 4]"

     8 *)

     9 hide_const (open) s 

    10 

    11 

    12 

    13 hide_const (open) Divides.adjust

    14 

    15 abbreviation

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

    17 

    18 consts DUMMY::'a

    19 

    20 (* Theorems as inference rules from LaTeXsugar.thy *)

    21 notation (Rule output)

    22   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

    23 

    24 syntax (Rule output)

    25   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    26   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")

    27 

    28   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 

    29   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")

    30 

    31   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

    32 

    33 notation (Axiom output)

    34   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

    35 

    36 notation (IfThen output)

    37   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    38 syntax (IfThen output)

    39   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    40   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    41   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

    42   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

    43 

    44 notation (IfThenNoBox output)

    45   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    46 syntax (IfThenNoBox output)

    47   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    48   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    49   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

    50   "_asm" :: "prop \<Rightarrow> asms" ("_")

    51 

    52 

    53 context uncomputable

    54 begin

    55 

    56 notation (latex output)

    57   Cons ("_::_" [48,47] 48) and

    58   set ("") and

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

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

    61   update2 ("update") and

    62   tm_wf0 ("wf") and

    63   tcopy_begin ("cbegin") and

    64   tcopy_loop ("cloop") and

    65   tcopy_end ("cend") and

    66   step0 ("step") and

    67   tcontra ("contra") and

    68   code_tcontra ("code contra") and

    69   steps0 ("steps") and

    70   adjust0 ("adjust") and

    71   exponent ("_\<^bsup>_\<^esup>") and

    72   tcopy ("copy") and 

    73   tape_of ("\<langle>_\<rangle>") and 

    74   tm_comp ("_ ; _") and 

    75   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and

    76   inv_begin0 ("I\<^isub>0") and

    77   inv_begin1 ("I\<^isub>1") and

    78   inv_begin2 ("I\<^isub>2") and

    79   inv_begin3 ("I\<^isub>3") and

    80   inv_begin4 ("I\<^isub>4") and 

    81   inv_begin ("I\<^bsub>cbegin\<^esub>") and

    82   inv_loop1 ("J\<^isub>1") and

    83   inv_loop0 ("J\<^isub>0") and

    84   inv_end1 ("K\<^isub>1") and

    85   inv_end0 ("K\<^isub>0") and

    86   measure_begin_step ("M\<^bsub>cbegin\<^esub>") and

    87   layout_of ("layout") and

    88   findnth ("find'_nth") and

    89   recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and

    90   Pr ("Pr\<^isup>_") and

    91   Cn ("Cn\<^isup>_") and

    92   Mn ("Mn\<^isup>_") and

    93   rec_exec ("eval") and

    94   tm_of_rec ("translate") and

    95   listsum ("\<Sigma>")

    96 

    97  

    98 lemma inv_begin_print:

    99   shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and

   100         "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 

   101         "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and 

   102         "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and 

   103         "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and

   104         "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"

   105 apply(case_tac [!] tp)

   106 by (auto)

   107 

   108 

   109 lemma inv1: 

   110   shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"

   111 unfolding Turing_Hoare.assert_imp_def

   112 unfolding inv_loop1.simps inv_begin0.simps

   113 apply(auto)

   114 apply(rule_tac x="1" in exI)

   115 apply(auto simp add: replicate.simps)

   116 done

   117 

   118 lemma inv2: 

   119   shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"

   120 apply(rule ext)

   121 apply(case_tac x)

   122 apply(simp add: inv_end1.simps)

   123 done

   124 

   125 

   126 lemma measure_begin_print:

   127   shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and

   128         "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and

   129         "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 

   130         "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"

   131 by (simp_all)

   132 

   133 declare [[show_question_marks = false]]

   134 

   135 lemma nats2tape:

   136   shows "<([]::nat list)> = []"

   137   and "<[n]> = <n>"

   138   and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>"

   139   and "<(n, m)> = <n> @ [Bk] @ <m>"

   140   and "<[n, m]> = <(n, m)>"

   141   and "<n> = Oc \<up> (n + 1)" 

   142 apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)

   143 apply(case_tac ns)

   144 apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)

   145 done 

   146 

   147 lemmas HR1 = 

   148   Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]

   149 

   150 lemmas HR2 =

   151   Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]

   152 

   153 lemma inv_begin01:

   154   assumes "n > 1"

   155   shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"

   156 using assms by auto                          

   157 

   158 lemma inv_begin02:

   159   assumes "n = 1"

   160   shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"

   161 using assms by auto

   162 

   163 

   164 lemma layout:

   165   shows "layout_of [] = []"

   166   and   "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)"

   167   and   "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)"

   168   and   "layout_of ((Goto l)#is) = 1#(layout_of is)"

   169 by(auto simp add: layout_of.simps length_of.simps)

   170 

   171 

   172 lemma adjust_simps:

   173   shows "adjust0 p = map (\<lambda>(a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"

   174 by(simp add: adjust.simps)

   175 

   176 fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

   177   where

   178   "clear n e = [Dec n e, Goto 0]"

   179 

   180 partial_function (tailrec)

   181   run

   182 where

   183   "run p cf = (if (is_final cf) then cf else run p (step0 cf p))"

   184 

   185 lemma numeral2:

   186   shows "11 = Suc 10"

   187   and   "12 = Suc 11"

   188   and   "13 = Suc 12"

   189   and   "14 = Suc 13"

   190   and   "15 = Suc 14"

   191 apply(arith)+

   192 done

   193 

   194 lemma tm_wf_simps:

   195   "tm_wf0 p = (2 <=length p \<and> is_even(length p) \<and> (\<forall>(a,s) \<in> set p. s <= (length p) div 2))"

   196 apply(simp add: tm_wf.simps)

   197 done

   198 

   199 (*>*)

   200 

   201 section {* Introduction *}

   202 

   203 

   204 

   205 text {*

   206 

   207 %\noindent

   208 %We formalised in earlier work the correctness proofs for two

   209 %algorithms in Isabelle/HOL---one about type-checking in

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

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

   212 %uncovered a gap in the informal correctness proof of the former and

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

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

   215 %formalise in Isabelle/HOL computability arguments about the

   216 %algorithms. 

   217 

   218 %Suppose you want to mechanise a proof for whether a predicate @{term P}, 

   219 %say, is decidable or not. Decidability of @{text P} usually

   220 %amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this

   221 %does \emph{not} work in 

   222 

   223 

   224 %Since Isabelle/HOL and other HOL theorem provers,

   225 %are based on classical logic where the law of excluded

   226 %middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no

   227 %matter whether @{text P} is constructed by computable means. We hit on

   228 %this limitation previously when we mechanised the correctness proofs

   229 %of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but

   230 %were unable to formalise arguments about decidability or undecidability.

   231 

   232 %The same problem would arise if we had formulated

   233 %the algorithms as recursive functions, because internally in

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

   235 %represented as inductively defined predicates too.

   236 

   237 \noindent

   238 We like to enable Isabelle/HOL users to reason about computability

   239 theory.  Reasoning about decidability of predicates, for example, is not as

   240 straightforward as one might think in Isabelle/HOL and other HOL

   241 theorem provers, since they are based on classical logic where the law

   242 of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always

   243 provable no matter whether the predicate @{text P} is constructed by

   244 computable means.

   245 

   246 Norrish formalised computability

   247 theory in HOL4. He choose the $\lambda$-calculus as the starting point

   248 for his formalisation because of its ``simplicity'' \cite[Page

   249 297]{Norrish11}.  Part of his formalisation is a clever infrastructure

   250 for reducing $\lambda$-terms. He also established the computational

   251 equivalence between the $\lambda$-calculus and recursive functions.

   252 Nevertheless he concluded that it would be appealing to have

   253 formalisations for more operational models of computations, such as

   254 Turing machines or register machines.  One reason is that many proofs

   255 in the literature use them.  He noted however that \cite[Page

   256 310]{Norrish11}:

   257 

   258 \begin{quote}

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

   260 general fiddliness,\\ Turing machines are an even more 

   261 daunting prospect.''

   262 \end{quote}

   263 

   264 \noindent

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

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

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

   268 involved with this work, one has to understand that Turing machine

   269 programs (similarly abacus programs) can be completely

   270 \emph{unstructured}, behaving similar to Basic programs containing the

   271 infamous goto \cite{Dijkstra68}. This precludes in the general case a

   272 compositional Hoare-style reasoning about Turing programs.  We provide

   273 such Hoare-rules for when it \emph{is} possible to reason in a

   274 compositional manner (which is fortunately quite often), but also

   275 tackle the more complicated case when we translate abacus programs

   276 into Turing programs.  This reasoning about concrete Turing machine

   277 programs is usually left out in the informal literature,

   278 e.g.~\cite{Boolos87}.

   279 

   280 %To see the difficulties

   281 %involved with this work, one has to understand that interactive

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

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

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

   285 %with convenient reasoning infrastructures (for example induction

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

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

   288 %underlying their definitions are sets of states together with 

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

   290 %means we have to implement our own reasoning infrastructure in order

   291 %to prove properties about them. This leads to annoyingly fiddly

   292 %formalisations.  We noticed first the difference between both,

   293 %structural and non-structural, ``worlds'' when formalising the

   294 %Myhill-Nerode theorem, where regular expressions fared much better

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

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

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

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

   299 %standard proof of this property uses the notion of universal

   300 %Turing machines.

   301 

   302 We are not the first who formalised Turing machines: we are aware of

   303 the work by Asperti and Ricciotti \cite{AspertiRicciotti12}. They

   304 describe a complete formalisation of Turing machines in the Matita

   305 theorem prover, including a universal Turing machine. However, they do

   306 \emph{not} formalise the undecidability of the halting problem since

   307 their main focus is complexity, rather than computability theory. They

   308 also report that the informal proofs from which they started are not

   309 ``sufficiently accurate to be directly usable as a guideline for

   310 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our

   311 formalisation we follow mainly the proofs from the textbook by Boolos

   312 et al \cite{Boolos87} and found that the description there is quite

   313 detailed. Some details are left out however: for example, constructing

   314 the \emph{copy Turing machine} is left as an exercise to the

   315 reader---a corresponding correctness proof is not mentioned at all; also \cite{Boolos87}

   316 only shows how the universal Turing machine is constructed for Turing

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

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

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

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

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

   322 how to do this are clear enough in \cite{Boolos87}.

   323 %However, one

   324 %aspect that is completely left out from the informal description in

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

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

   327 %which help us with such correctness arguments of Turing machines.

   328 

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

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

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

   332 23]{AspertiRicciotti12}:

   333 

   334 \begin{quote}\it

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

   336 different alphabet with respect to the machines it simulates is

   337 annoying.'' 

   338 \end{quote}

   339 

   340 \noindent

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

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

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

   344 Traditionally the content of a cell can be any

   345 character from a finite alphabet. Although computationally equivalent,

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

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

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

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

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

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

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

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

   354 \cite{Boolos87} by translating abacus machines to Turing machines and in

   355 turn recursive functions to abacus machines. The universal Turing

   356 machine can then be constructed by translating from a (universal) recursive function. 

   357 The part of mechanising the translation of recursive function to register 

   358 machines has already been done by Zammit in HOL4 \cite{Zammit99}, 

   359 although his register machines use a slightly different instruction

   360 set than the one described in \cite{Boolos87}.

   361 

   362 \smallskip

   363 \noindent

   364 {\bf Contributions:} We formalised in Isabelle/HOL Turing machines

   365 following the description of Boolos et al \cite{Boolos87} where tapes

   366 only have blank or occupied cells. We mechanise the undecidability of

   367 the halting problem and prove the correctness of concrete Turing

   368 machines that are needed in this proof; such correctness proofs are

   369 left out in the informal literature.  For reasoning about Turing

   370 machine programs we derive Hoare-rules.  We also construct the

   371 universal Turing machine from \cite{Boolos87} by translating recursive

   372 functions to abacus machines and abacus machines to Turing

   373 machines. This works essentially like a small, verified compiler 

   374 from recursive functions to Turing machine programs.

   375 When formalising the universal Turing machine,

   376 we stumbled in \cite{Boolos87} upon an inconsistent use of the definition of

   377 what partial function a Turing machine calculates. 

   378 

   379 %Since we have set up in

   380 %Isabelle/HOL a very general computability model and undecidability

   381 %result, we are able to formalise other results: we describe a proof of

   382 %the computational equivalence of single-sided Turing machines, which

   383 %is not given in \cite{Boolos87}, but needed for example for

   384 %formalising the undecidability proof of Wang's tiling problem

   385 %\cite{Robinson71}.  %We are not aware of any other %formalisation of a

   386 %substantial undecidability problem.

   387 *}

   388 

   389 section {* Turing Machines *}

   390 

   391 text {* \noindent

   392   Turing machines can be thought of as having a \emph{head},

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

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

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

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

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

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

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

   400   the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists

   401   composed of @{term n} elements of @{term Bk}s.  We also have the

   402   convention that the head, abbreviated @{term hd}, of the right list

   403   is the cell on which the head of the Turing machine currently

   404   scans. This can be pictured as follows:

   405   %

   406   \begin{center}

   407   \begin{tikzpicture}[scale=0.9]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   430   \end{tikzpicture}

   431   \end{center}

   432   

   433   \noindent

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

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

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

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

   438   the Turing machine can perform:

   439 

   440   \begin{center}

   441   \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}

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

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

   444   & $\mid$ & @{term L} & (move left)\\

   445   & $\mid$ & @{term R} & (move right)\\

   446   & $\mid$ & @{term Nop} & (do-nothing operation)\\

   447   \end{tabular}

   448   \end{center}

   449 

   450   \noindent

   451   We slightly deviate

   452   from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12}) 

   453   by using the @{term Nop} operation; however its use

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

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

   456   following tape updating function:

   457 

   458   \begin{center}

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

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

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

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

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

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

   465   \end{tabular}

   466   \end{center}

   467 

   468   \noindent

   469   The first two clauses replace the head of the right list

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

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

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

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

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

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

   476   blank cell to the right list; otherwise we have to remove the

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

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

   479   leaves the tape unchanged.

   480 

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

   482   %have the convention that the head of the right list is where the

   483   %head is currently positioned. Asperti and Ricciotti

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

   485   %dismiss it as it complicates their definition for \emph{tape

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

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

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

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

   490   %is on the left edge, respectively right edge, and in the middle

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

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

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

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

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

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

   497   %cover uniformly all cases including corner cases.

   498 

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

   500   %Given

   501   %how little is usually said about how to represent them in informal

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

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

   504   %representation where a Turing machine consists of a finite set of

   505   %states, then we will have difficulties composing two Turing

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

   507   %possibly renaming states apart whenever both machines share

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

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

   510   %quite cumbersome to reason about. 

   511   We follow the choice made in \cite{AspertiRicciotti12} 

   512   by representing a state with a natural number and the states in a Turing

   513   machine program by the initial segment of natural numbers starting from @{text 0}.

   514   In doing so we can compose two Turing machine programs by

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

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

   517 

   518   An \emph{instruction} of a Turing machine is a pair consisting of 

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

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

   521   program, which consists of four instructions

   522   %

   523   \begin{equation}

   524   \begin{tikzpicture}

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

   526   \node [anchor=west] at (-1.5,-0.64) 

   527   {$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm] 

   528   = starting state\end{tabular}}}$};

   529   

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

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

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

   533   \end{tikzpicture}

   534   \label{dither}

   535   \end{equation}

   536   %

   537   \noindent

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

   539   that segments of two pairs belong to a state. The first component of such a

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

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

   542   similarly the second component determines what should be done in

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

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

   545   The @{text 0}-state is special in that it will be used as the

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

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

   548   remain in the @{text 0}-state.  

   549   We have chosen a very concrete

   550   representation for Turing machine programs, because when constructing a universal

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

   552   %This can be directly done for our programs-as-lists, but is

   553   %slightly more difficult for the functions used by Asperti and Ricciotti.

   554 

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

   556   and the cell being scanned by the head, we need to fetch

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

   558   the function @{term fetch}

   559  

   560   \begin{equation}\label{fetch}

   561   \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

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

   563   @{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\

   564   \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\

   565   @{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\

   566   \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}

   567   \end{tabular}}

   568   \end{equation}

   569 

   570   \noindent

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

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

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

   574   (@{term None}-case). We often have to restrict Turing machine programs 

   575   to be well-formed: a program @{term p} is \emph{well-formed} if it 

   576   satisfies the following three properties:

   577 

   578   \begin{center}

   579   @{thm tm_wf_simps[where p="p", THEN eq_reflection]}

   580   \end{center}

   581 

   582   \noindent

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

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

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

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

   587 

   588  

   589   A \emph{configuration} @{term c} of a Turing machine is a state

   590   together with a tape. This is written as @{text "(s, (l, r))"}.  We

   591   say a configuration \emph{is final} if @{term "s = (0::nat)"} and we

   592   say a predicate @{text P} \emph{holds for} a configuration if @{text

   593   "P"} holds for the tape @{text "(l, r)"}.  If we have a configuration and a program, we can

   594   calculate what the next configuration is by fetching the appropriate

   595   action and next state from the program, and by updating the state

   596   and tape accordingly.  This single step of execution is defined as

   597   the function @{term step}

   598 

   599   \begin{center}

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

   601   @{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\

   602   & & @{text "in (s', update (l, r) a)"}

   603   \end{tabular}

   604   \end{center}

   605 

   606   \noindent

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

   608   @{text r} is empty it returns @{term Bk}.  

   609   We lift this definition to an evaluation function that performs 

   610   exactly @{text n} steps:

   611 

   612   \begin{center}

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

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

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

   616   \end{tabular}

   617   \end{center}

   618 

   619   \noindent Recall our definition of @{term fetch} (shown in

   620   \eqref{fetch}) with the default value for the @{text 0}-state. In

   621   case a Turing program takes according to the usual textbook

   622   definition, say \cite{Boolos87}, less than @{text n} steps before it

   623   halts, then in our setting the @{term steps}-evaluation does not

   624   actually halt, but rather transitions to the @{text 0}-state (the

   625   final state) and remains there performing @{text Nop}-actions until

   626   @{text n} is reached. 

   627 

   628 

   629   We often need to restrict tapes to be in standard form, which means 

   630   the left list of the tape is either empty or only contains @{text "Bk"}s, and 

   631   the right list contains some ``clusters'' of @{text "Oc"}s separated by single 

   632   blanks. To make this formal we define the following overloaded function

   633   encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s.

   634   % 

   635   \begin{equation}

   636   \mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

   637   @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\

   638   @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\

   639   \end{tabular}\hspace{6mm}

   640   \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

   641   @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\

   642   @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\

   643   @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}

   644   \end{tabular}}\label{standard}

   645   \end{equation}

   646   %

   647   \noindent

   648   A \emph{standard tape} is then of the form @{text "(Bk\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>l)"} for some @{text k}, 

   649   @{text l} 

   650   and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the 

   651   leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0} 

   652   is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on.

   653 

   654 

   655  We need to be able to sequentially compose Turing machine programs. Given our

   656   concrete representation, this is relatively straightforward, if

   657   slightly fiddly. We use the following two auxiliary functions:

   658 

   659   \begin{center}

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

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

   662   @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\

   663   \end{tabular}

   664   \end{center}

   665 

   666   \noindent

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

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

   669   n}; the second adds @{term "Suc(length p div 2)"} to the @{text

   670   0}-state, thus redirecting all references to the ``halting state''

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

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

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

   674 

   675   \begin{center}

   676   @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}

   677   \end{center}

   678 

   679   \noindent

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

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

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

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

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

   685   %an initial segment of the natural numbers.

   686   

   687   \begin{figure}[t]

   688   \begin{center}

   689   \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c}

   690   \begin{tabular}[t]{@ {}l@ {}}

   691   @{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\

   692   \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\

   693   \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>Oc\<^esub>, 3), (L, 4),"}\\

   694   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} 

   695   \end{tabular}

   696   &

   697   \begin{tabular}[t]{@ {}l@ {}}

   698   @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\

   699   \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\

   700   \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Bk\<^esub>, 2), (R, 3), (R, 4),"}\\

   701   \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Oc\<^esub>, 5), (R, 4), (L, 6),"}\\

   702   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} 

   703   \end{tabular}

   704   &

   705   \begin{tabular}[t]{@ {}l@ {}}

   706   @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\

   707   \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>Oc\<^esub>, 3),"}\\

   708   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\

   709   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>Bk\<^esub>, 4), (R, 0),"}\\

   710   \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} 

   711   \end{tabular}

   712   \end{tabular}\\[2mm]

   713 

   714   \begin{tikzpicture}[scale=0.7]

   715   \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};

   716   \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};

   717   \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};

   718   \node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_begin"}}^{}$};

   719   \node [anchor=base] at (5.6,-0.6) {\small$\overbrace{@{term "tcopy_loop"}}^{}$};

   720   \node [anchor=base] at (10.5,-0.6) {\small$\overbrace{@{term "tcopy_end"}}^{}$};

   721 

   722 

   723   \begin{scope}[shift={(0.5,0)}]

   724   \draw[very thick] (-0.25,0)   -- ( 1.25,0);

   725   \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5);

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

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

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

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

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

   731   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

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

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

   734   \end{scope}

   735 

   736   \begin{scope}[shift={(2.9,0)}]

   737   \draw[very thick] (-0.25,0)   -- ( 2.25,0);

   738   \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5);

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

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

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

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

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

   744   \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

   745   \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6);

   746   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

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

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

   749   \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

   750   \end{scope}

   751 

   752   \begin{scope}[shift={(6.8,0)}]

   753   \draw[very thick] (-0.75,0)   -- ( 3.25,0);

   754   \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);

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

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

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

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

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

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

   761   \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

   762   \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);

   763   \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);

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

   765   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

   766   \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);

   767   \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);

   768   \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

   769   \end{scope}

   770 

   771   \begin{scope}[shift={(11.7,0)}]

   772   \draw[very thick] (-0.75,0)   -- ( 3.25,0);

   773   \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5);

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

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

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

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

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

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

   780   \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5);

   781   \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);

   782   \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5);

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

   784   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

   785   \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);

   786   \draw[fill]     ( 2.85,0.1) rectangle (3.15,0.4);

   787   \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

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

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

   790   \end{scope}

   791   \end{tikzpicture}\\[-8mm]\mbox{} 

   792   \end{center}

   793   \caption{The three components of the \emph{copy Turing machine} (above). If started 

   794   (below) with the tape @{term "([], <(2::nat)>)"} the first machine appends @{term "[Bk, Oc]"} at 

   795   the end of the right tape; the second then ``moves'' all @{term Oc}s except the 

   796   first from the beginning of the tape to the end; the third ``refills'' the original 

   797   block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.}

   798   \label{copy}

   799   \end{figure}

   800 

   801 

   802 

   803 

   804   Before we can prove the undecidability of the halting problem for

   805   our Turing machines working on standard tapes, we have to analyse

   806   two concrete Turing machine programs and establish that they are

   807   correct---that means they are ``doing what they are supposed to be

   808   doing''.  Such correctness proofs are usually left out in the

   809   informal literature, for example \cite{Boolos87}.  The first program

   810   we need to prove correct is the @{term dither} program shown in

   811   \eqref{dither} and the second program is @{term "tcopy"} defined as

   812 

   813   \begin{equation}

   814   \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}

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

   816   \end{tabular}}\label{tcopy}

   817   \end{equation}

   818 

   819   \noindent

   820   whose three components are given in Figure~\ref{copy}. For our

   821   correctness proofs, we introduce the notion of total correctness

   822   defined in terms of \emph{Hoare-triples}, written @{term "{P} (p::tprog0)

   823   {Q}"}.  They implement the idea that a program @{term

   824   p} started in state @{term "1::nat"} with a tape satisfying @{term

   825   P} will after some @{text n} steps halt (have transitioned into the

   826   halting state) with a tape satisfying @{term Q}. This idea is very

   827   similar to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. We

   828   also have \emph{Hoare-pairs} of the form @{term "{P} (p::tprog0) \<up>"}

   829   implementing the case that a program @{term p} started with a tape

   830   satisfying @{term P} will loop (never transition into the halting

   831   state). Both notion are formally defined as

   832 

   833   \begin{center}

   834   \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}

   835   \begin{tabular}[t]{@ {}l@ {}}

   836   \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm]

   837   \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\

   838   \hspace{7mm}if @{term "P tp"} holds then\\

   839   \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\

   840   \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\

   841   \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}

   842   \end{tabular} &

   843   \begin{tabular}[t]{@ {}l@ {}}

   844   \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]

   845   \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ 

   846   \hspace{7mm}if @{term "P tp"} holds then\\

   847   \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}

   848   \end{tabular}

   849   \end{tabular}

   850   \end{center}

   851   

   852   \noindent

   853   For our Hoare-triples we can easily prove the following Hoare-consequence rule

   854 

   855   \begin{equation}

   856   @{thm[mode=Rule] Hoare_consequence}

   857   \end{equation}

   858 

   859   \noindent

   860   where

   861   @{term "Turing_Hoare.assert_imp P' P"} stands for the fact that for all tapes @{term "tp"},

   862   @{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}).

   863 

   864   Like Asperti and Ricciotti with their notion of realisability, we

   865   have set up our Hoare-rules so that we can deal explicitly

   866   with total correctness and non-termination, rather than have

   867   notions for partial correctness and termination. Although the latter

   868   would allow us to reason more uniformly (only using Hoare-triples),

   869   we prefer our definitions because we can derive below some simple

   870   Hoare-rules for sequentially composed Turing programs.  In this way

   871   we can reason about the correctness of @{term "tcopy_begin"}, for

   872   example, completely separately from @{term "tcopy_loop"} and @{term

   873   "tcopy_end"}.

   874 

   875   It is relatively straightforward to prove that the Turing program 

   876   @{term "dither"} shown in \eqref{dither} is correct. This program

   877   should be the ``identity'' when started with a standard tape representing 

   878   @{text "1"} but loops when started with the @{text 0}-representation instead, as pictured 

   879   below.

   880 

   881 

   882   \begin{center}

   883   \begin{tabular}{l@ {\hspace{3mm}}lcl}

   884   & \multicolumn{1}{c}{start tape}\\[1mm]

   885   \raisebox{2mm}{halting case:} &

   886   \begin{tikzpicture}[scale=0.8]

   887   \draw[very thick] (-2,0)   -- ( 0.75,0);

   888   \draw[very thick] (-2,0.5) -- ( 0.75,0.5);

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

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

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

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

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

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

   895   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

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

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

   898   \end{tikzpicture} 

   899   & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &

   900   \begin{tikzpicture}[scale=0.8]

   901   \draw[very thick] (-2,0)   -- ( 0.75,0);

   902   \draw[very thick] (-2,0.5) -- ( 0.75,0.5);

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

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

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

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

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

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

   909   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

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

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

   912   \end{tikzpicture}\\

   913 

   914   \raisebox{2mm}{non-halting case:} &

   915   \begin{tikzpicture}[scale=0.8]

   916   \draw[very thick] (-2,0)   -- ( 0.25,0);

   917   \draw[very thick] (-2,0.5) -- ( 0.25,0.5);

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

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

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

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

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

   923   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

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

   925   \end{tikzpicture} 

   926   & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} &

   927   \raisebox{2mm}{loops}

   928   \end{tabular}

   929   \end{center}

   930 

   931   \noindent

   932   We can prove the following two Hoare-statements:

   933  

   934   \begin{center}

   935   \begin{tabular}{l}

   936   @{thm dither_halts}\\

   937   @{thm dither_loops}

   938   \end{tabular}

   939   \end{center}

   940 

   941   \noindent

   942   The first is by a simple calculation. The second is by an induction on the

   943   number of steps we can perform starting from the input tape.

   944 

   945   The program @{term tcopy} defined in \eqref{tcopy} has 15 states;

   946   its purpose is to produce the standard tape @{term "(Bks, <(n,

   947   n::nat)>)"} when started with @{term "(Bks, <(n::nat)>)"}, that is

   948   making a copy of a value @{term n} on the tape.  Reasoning about this program

   949   is substantially harder than about @{term dither}. To ease the

   950   burden, we derive the following two Hoare-rules for sequentially

   951   composed programs.

   952 

   953   \begin{center}

   954   \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}}

   955   $\inferrule*[Right=@{thm (prem 3) HR1}]

   956   {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}

   957   {@{thm (concl) HR1}}

   958   $ &

   959   $

   960   \inferrule*[Right=@{thm (prem 3) HR2}]

   961   {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}

   962   {@{thm (concl) HR2}}

   963   $

   964   \end{tabular}

   965   \end{center}

   966 

   967   \noindent

   968   The first corresponds to the usual Hoare-rule for composition of two

   969   terminating programs. The second rule gives the conditions for when

   970   the first program terminates generating a tape for which the second

   971   program loops.  The side-conditions about @{thm (prem 3) HR2} are

   972   needed in order to ensure that the redirection of the halting and

   973   initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"}, respectively, match

   974   up correctly.  These Hoare-rules allow us to prove the correctness

   975   of @{term tcopy} by considering the correctness of the components

   976   @{term "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"}

   977   in isolation. This simplifies the reasoning considerably, for

   978   example when designing decreasing measures for proving the termination

   979   of the programs.  We will show the details for the program @{term

   980   "tcopy_begin"}. For the two other programs we refer the reader to

   981   our formalisation.

   982 

   983   Given the invariants @{term "inv_begin0"},\ldots,

   984   @{term "inv_begin4"} shown in Figure~\ref{invbegin}, which

   985   correspond to each state of @{term tcopy_begin}, we define the

   986   following invariant for the whole @{term tcopy_begin} program:

   987 

   988   \begin{figure}[t]

   989   \begin{center}

   990   \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}}

   991   \hline

   992   @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\

   993   @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\

   994   @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\

   995   @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\

   996   @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\

   997                                 &             & @{thm (rhs) inv_begin02}\smallskip \\

   998    \hline

   999   @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\

  1000                                &             & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\

  1001   @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\

  1002    \hline

  1003   @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\

  1004   @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\

  1005   \hline

  1006   \end{tabular}

  1007   \end{center}

  1008   \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of 

  1009   @{term tcopy_begin}. Below, the invariants only for the starting and halting states of

  1010   @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant, the parameter 

  1011   @{term n} stands for the number

  1012   of @{term Oc}s with which the Turing machine is started.}\label{invbegin}

  1013   \end{figure}

  1014 

  1015   \begin{center}

  1016   \begin{tabular}{rcl}

  1017   @{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} & 

  1018   @{text "if"} @{thm (prem 1) inv_begin_print(1)} @{text then} @{thm (rhs) inv_begin_print(1)}\\

  1019   & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(2)} @{text then} @{thm (rhs) inv_begin_print(2)} \\

  1020  & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(3)} @{text then} @{thm (rhs) inv_begin_print(3)}\\

  1021   & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(4)} @{text then} @{thm (rhs) inv_begin_print(4)}\\

  1022    & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(5)} @{text then} @{thm (rhs) inv_begin_print(5)}\\

  1023   & & @{text else} @{thm (rhs) inv_begin_print(6)}

  1024   \end{tabular}

  1025   \end{center}

  1026 

  1027   \noindent

  1028   This invariant depends on @{term n} representing the number of

  1029   @{term Oc}s on the tape. It is not hard (26

  1030   lines of automated proof script) to show that for @{term "n >

  1031   (0::nat)"} this invariant is preserved under the computation rules

  1032   @{term step} and @{term steps}. This gives us partial correctness

  1033   for @{term "tcopy_begin"}. 

  1034 

  1035   We next need to show that @{term "tcopy_begin"} terminates. For this

  1036   we introduce lexicographically ordered pairs @{term "(n, m)"}

  1037   derived from configurations @{text "(s, (l, r))"} whereby @{text n} is

  1038   the state @{text s}, but ordered according to how @{term tcopy_begin} executes

  1039   them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have

  1040   a strictly decreasing measure, @{term m} takes the data on the tape into

  1041   account and is calculated according to the following measure function:

  1042 

  1043   \begin{center}

  1044   \begin{tabular}{rcl}

  1045   @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & 

  1046   @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\

  1047   & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} 

  1048   @{text "("}@{thm (rhs) measure_begin_print(2)}@{text ")"} \\

  1049  & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\

  1050   & & @{text else} @{thm (rhs) measure_begin_print(4)}\\

  1051   \end{tabular}

  1052   \end{center}

  1053   

  1054   \noindent

  1055   With this in place, we can show that for every starting tape of the

  1056   form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing

  1057   machine @{term "tcopy_begin"} will eventually halt (the measure

  1058   decreases in each step). Taking this and the partial correctness

  1059   proof together, we obtain the Hoare-triple shown on the left for @{term tcopy_begin}:

  1060    

  1061 

  1062   \begin{center}

  1063   @{thm (concl) begin_correct}\hspace{6mm}

  1064   @{thm (concl) loop_correct}\hspace{6mm}

  1065   @{thm (concl) end_correct}

  1066   \end{center}

  1067 

  1068   \noindent 

  1069   where we assume @{text "0 < n"} (similar reasoning is needed for

  1070   the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of

  1071   the halting state of @{term tcopy_begin} implies the invariant of

  1072   the starting state of @{term tcopy_loop}, that is @{term "Turing_Hoare.assert_imp (inv_begin0 n)

  1073   (inv_loop1 n)"} holds, and also @{term "inv_loop0 n = inv_end1

  1074   n"}, we can derive the following Hoare-triple for the correctness 

  1075   of @{term tcopy}:

  1076 

  1077   \begin{center}

  1078   @{thm tcopy_correct}

  1079   \end{center}

  1080 

  1081   \noindent

  1082   That means if we start with a tape of the form @{term "([], <n::nat>)"} then 

  1083   @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}, as desired.

  1084 

  1085   Finally, we are in the position to prove the undecidability of the halting problem.

  1086   A program @{term p} started with a standard tape containing the (encoded) numbers

  1087   @{term ns} will \emph{halt} with a standard tape containing a single (encoded) 

  1088   number is defined as

  1089 

  1090   \begin{center}

  1091   @{thm halts_def}

  1092   \end{center}

  1093 

  1094   \noindent

  1095   This roughly means we considering only Turing machine programs

  1096   representing functions that take some numbers as input and produce a

  1097   single number as output. For undecidability, the property we are

  1098   proving is that there is no Turing machine that can decide in

  1099   general whether a Turing machine program halts (answer either @{text

  1100   0} for halting or @{text 1} for looping). Given our correctness

  1101   proofs for @{term dither} and @{term tcopy} shown above, this

  1102   non-existence is now relatively straightforward to establish. We first

  1103   assume there is a coding function, written @{term "code M"}, which

  1104   represents a Turing machine @{term "M"} as a natural number.  No

  1105   further assumptions are made about this coding function. Suppose a

  1106   Turing machine @{term H} exists such that if started with the

  1107   standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0},

  1108   respectively @{text 1}, depending on whether @{text M} halts or not when

  1109   started with the input tape containing @{term "<ns>"}.  This

  1110   assumption is formalised as follows---for all @{term M} and all lists of

  1111   natural numbers @{term ns}:

  1112 

  1113   \begin{center}

  1114   \begin{tabular}{r}

  1115   @{thm (prem 2) uncomputable.h_case} implies

  1116   @{thm (concl) uncomputable.h_case}\\

  1117   

  1118   @{thm (prem 2) uncomputable.nh_case} implies

  1119   @{thm (concl) uncomputable.nh_case}

  1120   \end{tabular}

  1121   \end{center}

  1122 

  1123   \noindent

  1124   The contradiction can be derived using the following Turing machine

  1125 

  1126   \begin{center}

  1127   @{thm tcontra_def}

  1128   \end{center}

  1129 

  1130   \noindent

  1131   Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^isub>1"}\ldots@{text "P\<^isub>3"} 

  1132   shown on the 

  1133   left, we can derive the following Hoare-pair for @{term tcontra} on the right.

  1134 

  1135   \begin{center}\small