(*<*)theory Paperimports "../thys/UTM" "../thys/Abacus_Defs"begin(*value "map (steps (1,[],[Oc]) ([(L,0),(L,2),(R,2),(R,0)],0)) [0 ..< 4]"*)hide_const (open) s hide_const (open) Divides.adjustabbreviation "update2 p a \<equiv> update a p"consts DUMMY::'a(* Theorems as inference rules from LaTeXsugar.thy *)notation (Rule output) "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")syntax (Rule output) "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}\\>/ _") "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")notation (Axiom output) "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")notation (IfThen output) "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")syntax (IfThen output) "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")notation (IfThenNoBox output) "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")syntax (IfThenNoBox output) "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") "_asm" :: "prop \<Rightarrow> asms" ("_")context uncomputablebeginnotation (latex output) Cons ("_::_" [48,47] 48) and set ("") and W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and update2 ("update") and tm_wf0 ("wf") and tcopy_begin ("cbegin") and tcopy_loop ("cloop") and tcopy_end ("cend") and step0 ("step") and tcontra ("contra") and code_tcontra ("code contra") and steps0 ("steps") and adjust0 ("adjust") and exponent ("_\<^bsup>_\<^esup>") and tcopy ("copy") and tape_of ("\<langle>_\<rangle>") and tm_comp ("_ ; _") and DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") and inv_begin0 ("I\<^sub>0") and inv_begin1 ("I\<^sub>1") and inv_begin2 ("I\<^sub>2") and inv_begin3 ("I\<^sub>3") and inv_begin4 ("I\<^sub>4") and inv_begin ("I\<^bsub>cbegin\<^esub>") and inv_loop1 ("J\<^sub>1") and inv_loop0 ("J\<^sub>0") and inv_end1 ("K\<^sub>1") and inv_end0 ("K\<^sub>0") and measure_begin_step ("M\<^bsub>cbegin\<^esub>") and layout_of ("layout") and findnth ("find'_nth") and recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^sup>_\<^raw:}>\<^sub>_") and Pr ("Pr\<^sup>_") and Cn ("Cn\<^sup>_") and Mn ("Mn\<^sup>_") and rec_exec ("eval") and tm_of_rec ("translate") and listsum ("\<Sigma>")lemma inv_begin_print: shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and "s = 2 \<Longrightarrow> inv_begin n (s, tp) = inv_begin2 n tp" and "s = 3 \<Longrightarrow> inv_begin n (s, tp) = inv_begin3 n tp" and "s = 4 \<Longrightarrow> inv_begin n (s, tp) = inv_begin4 n tp" and "s \<notin> {0,1,2,3,4} \<Longrightarrow> inv_begin n (s, l, r) = False"apply(case_tac [!] tp)by (auto)lemma inv1: shows "0 < (n::nat) \<Longrightarrow> Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"unfolding Turing_Hoare.assert_imp_defunfolding inv_loop1.simps inv_begin0.simpsapply(auto)apply(rule_tac x="1" in exI)apply(auto simp add: replicate.simps)donelemma inv2: shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"apply(rule ext)apply(case_tac x)apply(simp add: inv_end1.simps)donelemma measure_begin_print: shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"by (simp_all)declare [[show_question_marks = false]]lemma nats2tape: shows "<([]::nat list)> = []" and "<[n]> = <n>" and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>" and "<(n, m)> = <n> @ [Bk] @ <m>" and "<[n, m]> = <(n, m)>" and "<n> = Oc \<up> (n + 1)" apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)apply(case_tac ns)apply(auto simp add: tape_of_nat_pair tape_of_nat_abv)done lemmas HR1 = Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^sub>1" and B="p\<^sub>2"]lemmas HR2 = Hoare_plus_unhalt[where ?A="p\<^sub>1" and B="p\<^sub>2"]lemma inv_begin01: assumes "n > 1" shows "inv_begin0 n (l, r) = (n > 1 \<and> (l, r) = (Oc \<up> (n - 2), [Oc, Oc, Bk, Oc]))"using assms by auto lemma inv_begin02: assumes "n = 1" shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"using assms by autolemma layout: shows "layout_of [] = []" and "layout_of ((Inc R\<iota>)#is) = (2 * R\<iota> + 9)#(layout_of is)" and "layout_of ((Dec R\<iota> l)#is) = (2 * R\<iota> + 16)#(layout_of is)" and "layout_of ((Goto l)#is) = 1#(layout_of is)"by(auto simp add: layout_of.simps length_of.simps)lemma adjust_simps: shows "adjust0 p = map (\<lambda>(a, s). (a, if s = 0 then (Suc (length p div 2)) else s)) p"by(simp add: adjust.simps)fun clear :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" where "clear n e = [Dec n e, Goto 0]"partial_function (tailrec) runwhere "run p cf = (if (is_final cf) then cf else run p (step0 cf p))"lemma numeral2: shows "11 = Suc 10" and "12 = Suc 11" and "13 = Suc 12" and "14 = Suc 13" and "15 = Suc 14"apply(arith)+donelemma tm_wf_simps: "tm_wf0 p = (2 <=length p \<and> is_even(length p) \<and> (\<forall>(a,s) \<in> set p. s <= (length p) div 2))"apply(simp add: tm_wf.simps)done(*>*)section {* Introduction *}text {*%\noindent%We formalised in earlier work the correctness proofs for two%algorithms in Isabelle/HOL---one about type-checking in%LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests%in access control~\cite{WuZhangUrban12}. The formalisations%uncovered a gap in the informal correctness proof of the former and%made us realise that important details were left out in the informal%model for the latter. However, in both cases we were unable to%formalise in Isabelle/HOL computability arguments about the%algorithms. %Suppose you want to mechanise a proof for whether a predicate @{term P}, %say, is decidable or not. Decidability of @{text P} usually%amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this%does \emph{not} work in %Since Isabelle/HOL and other HOL theorem provers,%are based on classical logic where the law of excluded%middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no%matter whether @{text P} is constructed by computable means. We hit on%this limitation previously when we mechanised the correctness proofs%of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but%were unable to formalise arguments about decidability or undecidability.%The same problem would arise if we had formulated%the algorithms as recursive functions, because internally in%Isabelle/HOL, like in all HOL-based theorem provers, functions are%represented as inductively defined predicates too.\noindentWe like to enable Isabelle/HOL users to reason about computabilitytheory. Reasoning about decidability of predicates, for example, is not asstraightforward as one might think in Isabelle/HOL and other HOLtheorem provers, since they are based on classical logic where the lawof excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} is alwaysprovable no matter whether the predicate @{text P} is constructed bycomputable means.Norrish formalised computabilitytheory in HOL4. He choose the $\lambda$-calculus as the starting pointfor his formalisation because of its ``simplicity'' \cite[Page297]{Norrish11}. Part of his formalisation is a clever infrastructurefor reducing $\lambda$-terms. He also established the computationalequivalence between the $\lambda$-calculus and recursive functions.Nevertheless he concluded that it would be appealing to haveformalisations for more operational models of computations, such asTuring machines or register machines. One reason is that many proofsin the literature use them. He noted however that \cite[Page310]{Norrish11}:\begin{quote}\it``If register machines are unappealing because of their general fiddliness,\\ Turing machines are an even more daunting prospect.''\end{quote}\noindentIn this paper we take on this daunting prospect and provide aformalisation of Turing machines, as well as abacus machines (a kindof register machines) and recursive functions. To see the difficultiesinvolved with this work, one has to understand that Turing machineprograms (similarly abacus programs) can be completely\emph{unstructured}, behaving similar to Basic programs containing theinfamous goto \cite{Dijkstra68}. This precludes in the general case acompositional Hoare-style reasoning about Turing programs. We providesuch Hoare-rules for when it \emph{is} possible to reason in acompositional manner (which is fortunately quite often), but alsotackle the more complicated case when we translate abacus programsinto Turing programs. This reasoning about concrete Turing machineprograms is usually left out in the informal literature,e.g.~\cite{Boolos87}.%To see the difficulties%involved with this work, one has to understand that interactive%theorem provers, like Isabelle/HOL, are at their best when the%data-structures at hand are ``structurally'' defined, like lists,%natural numbers, regular expressions, etc. Such data-structures come%with convenient reasoning infrastructures (for example induction%principles, recursion combinators and so on). But this is \emph{not}%the case with Turing machines (and also not with register machines):%underlying their definitions are sets of states together with %transition functions, all of which are not structurally defined. This%means we have to implement our own reasoning infrastructure in order%to prove properties about them. This leads to annoyingly fiddly%formalisations. We noticed first the difference between both,%structural and non-structural, ``worlds'' when formalising the%Myhill-Nerode theorem, where regular expressions fared much better%than automata \cite{WuZhangUrban11}. However, with Turing machines%there seems to be no alternative if one wants to formalise the great%many proofs from the literature that use them. We will analyse one%example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The%standard proof of this property uses the notion of universal%Turing machines.We are not the first who formalised Turing machines: we are aware ofthe work by Asperti and Ricciotti \cite{AspertiRicciotti12}. Theydescribe a complete formalisation of Turing machines in the Matitatheorem prover, including a universal Turing machine. However, they do\emph{not} formalise the undecidability of the halting problem sincetheir main focus is complexity, rather than computability theory. Theyalso report that the informal proofs from which they started are not``sufficiently accurate to be directly usable as a guideline forformalization'' \cite[Page 2]{AspertiRicciotti12}. For ourformalisation we follow mainly the proofs from the textbook by Booloset al \cite{Boolos87} and found that the description there is quitedetailed. Some details are left out however: for example, constructingthe \emph{copy Turing machine} is left as an exercise to thereader---a corresponding correctness proof is not mentioned at all; also \cite{Boolos87}only shows how the universal Turing machine is constructed for Turingmachines computing unary functions. We had to figure out a way togeneralise this result to $n$-ary functions. Similarly, when compilingrecursive functions to abacus machines, the textbook again only showshow it can be done for 2- and 3-ary functions, but in theformalisation we need arbitrary functions. But the general ideas forhow to do this are clear enough in \cite{Boolos87}.%However, one%aspect that is completely left out from the informal description in%\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing%machines are correct. We will introduce Hoare-style proof rules%which help us with such correctness arguments of Turing machines.The main difference between our formalisation and the one by Aspertiand Ricciotti is that their universal Turing machine uses a differentalphabet than the machines it simulates. They write \cite[Page23]{AspertiRicciotti12}:\begin{quote}\it``In particular, the fact that the universal machine operates with adifferent alphabet with respect to the machines it simulates isannoying.'' \end{quote}\noindentIn this paper we follow the approach by Boolos et al \cite{Boolos87},which goes back to Post \cite{Post36}, where all Turing machinesoperate on tapes that contain only \emph{blank} or \emph{occupied} cells. Traditionally the content of a cell can be anycharacter from a finite alphabet. Although computationally equivalent,the more restrictive notion of Turing machines in \cite{Boolos87} makesthe reasoning more uniform. In addition some proofs \emph{about} Turingmachines are simpler. The reason is that one often needs to encodeTuring machines---consequently if the Turing machines are simpler, then the codingfunctions are simpler too. Unfortunately, the restrictiveness also makesit harder to design programs for these Turing machines. In orderto construct a universal Turing machine we therefore do not follow \cite{AspertiRicciotti12}, instead follow the proof in\cite{Boolos87} by translating abacus machines to Turing machines and inturn recursive functions to abacus machines. The universal Turingmachine can then be constructed by translating from a (universal) recursive function. The part of mechanising the translation of recursive function to register machines has already been done by Zammit in HOL4 \cite{Zammit99}, although his register machines use a slightly different instructionset than the one described in \cite{Boolos87}.\smallskip\noindent{\bf Contributions:} We formalised in Isabelle/HOL Turing machinesfollowing the description of Boolos et al \cite{Boolos87} where tapesonly have blank or occupied cells. We mechanise the undecidability ofthe halting problem and prove the correctness of concrete Turingmachines that are needed in this proof; such correctness proofs areleft out in the informal literature. For reasoning about Turingmachine programs we derive Hoare-rules. We also construct theuniversal Turing machine from \cite{Boolos87} by translating recursivefunctions to abacus machines and abacus machines to Turingmachines. This works essentially like a small, verified compiler from recursive functions to Turing machine programs.When formalising the universal Turing machine,we stumbled in \cite{Boolos87} upon an inconsistent use of the definition ofwhat partial function a Turing machine calculates. %Since we have set up in%Isabelle/HOL a very general computability model and undecidability%result, we are able to formalise other results: we describe a proof of%the computational equivalence of single-sided Turing machines, which%is not given in \cite{Boolos87}, but needed for example for%formalising the undecidability proof of Wang's tiling problem%\cite{Robinson71}. %We are not aware of any other %formalisation of a%substantial undecidability problem.*}section {* Turing Machines *}text {* \noindent Turing machines can be thought of as having a \emph{head}, ``gliding'' over a potentially infinite tape. Boolos et al~\cite{Boolos87} only consider tapes with cells being either blank or occupied, which we represent by a datatype having two constructors, namely @{text Bk} and @{text Oc}. One way to represent such tapes is to use a pair of lists, written @{term "(l, r)"}, where @{term l} stands for the tape on the left-hand side of the head and @{term r} for the tape on the right-hand side. We use the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists composed of @{term n} elements of @{term Bk}s. We also have the convention that the head, abbreviated @{term hd}, of the right list is the cell on which the head of the Turing machine currently scans. This can be pictured as follows: % \begin{center} \begin{tikzpicture}[scale=0.9] \draw[very thick] (-3.0,0) -- ( 3.0,0); \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5); \draw[very thick] (-0.25,0) -- (-0.25,0.5); \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); \draw[very thick] (-0.75,0) -- (-0.75,0.5); \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); \draw[very thick] (-1.25,0) -- (-1.25,0.5); \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); \draw[very thick] (-1.75,0) -- (-1.75,0.5); \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); \draw[fill] (1.35,0.1) rectangle (1.65,0.4); \draw[fill] (0.85,0.1) rectangle (1.15,0.4); \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); \draw[fill] (-1.65,0.1) rectangle (-1.35,0.4); \draw (-0.25,0.8) -- (-0.25,-0.8); \draw[<->] (-1.25,-0.7) -- (0.75,-0.7); \node [anchor=base] at (-0.85,-0.5) {\small left list}; \node [anchor=base] at (0.40,-0.5) {\small right list}; \node [anchor=base] at (0.1,0.7) {\small head}; \node [anchor=base] at (-2.2,0.2) {\ldots}; \node [anchor=base] at ( 2.3,0.2) {\ldots}; \end{tikzpicture} \end{center} \noindent Note that by using lists each side of the tape is only finite. The potential infinity is achieved by adding an appropriate blank or occupied cell whenever the head goes over the ``edge'' of the tape. To make this formal we define five possible \emph{actions} the Turing machine can perform: \begin{center} \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l} @{text "a"} & $::=$ & @{term "W0"} & (write blank, @{term Bk})\\ & $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\ & $\mid$ & @{term L} & (move left)\\ & $\mid$ & @{term R} & (move right)\\ & $\mid$ & @{term Nop} & (do-nothing operation)\\ \end{tabular} \end{center} \noindent We slightly deviate from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12}) by using the @{term Nop} operation; however its use will become important when we formalise halting computations and also universal Turing machines. Given a tape and an action, we can define the following tape updating function: \begin{center} \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} @{thm (lhs) update.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(1)}\\ @{thm (lhs) update.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(2)}\\ @{thm (lhs) update.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(3)}\\ @{thm (lhs) update.simps(4)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(4)}\\ @{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(5)}\\ \end{tabular} \end{center} \noindent The first two clauses replace the head of the right list with a new @{term Bk} or @{term Oc}, respectively. To see that these two clauses make sense in case where @{text r} is the empty list, one has to know that the tail function, @{term tl}, is defined such that @{term "tl [] == []"} holds. The third clause implements the move of the head one step to the left: we need to test if the left-list @{term l} is empty; if yes, then we just prepend a blank cell to the right list; otherwise we have to remove the head from the left-list and prepend it to the right list. Similarly in the fourth clause for a right move action. The @{term Nop} operation leaves the tape unchanged. %Note that our treatment of the tape is rather ``unsymmetric''---we %have the convention that the head of the right list is where the %head is currently positioned. Asperti and Ricciotti %\cite{AspertiRicciotti12} also considered such a representation, but %dismiss it as it complicates their definition for \emph{tape %equality}. The reason is that moving the head one step to %the left and then back to the right might change the tape (in case %of going over the ``edge''). Therefore they distinguish four types %of tapes: one where the tape is empty; another where the head %is on the left edge, respectively right edge, and in the middle %of the tape. The reading, writing and moving of the tape is then %defined in terms of these four cases. In this way they can keep the %tape in a ``normalised'' form, and thus making a left-move followed %by a right-move being the identity on tapes. Since we are not using %the notion of tape equality, we can get away with the unsymmetric %definition above, and by using the @{term update} function %cover uniformly all cases including corner cases. Next we need to define the \emph{states} of a Turing machine. %Given %how little is usually said about how to represent them in informal %presentations, it might be surprising that in a theorem prover we %have to select carefully a representation. If we use the naive %representation where a Turing machine consists of a finite set of %states, then we will have difficulties composing two Turing %machines: we would need to combine two finite sets of states, %possibly renaming states apart whenever both machines share %states.\footnote{The usual disjoint union operation in Isabelle/HOL %cannot be used as it does not preserve types.} This renaming can be %quite cumbersome to reason about. We follow the choice made in \cite{AspertiRicciotti12} by representing a state with a natural number and the states in a Turing machine program by the initial segment of natural numbers starting from @{text 0}. In doing so we can compose two Turing machine programs by shifting the states of one by an appropriate amount to a higher segment and adjusting some ``next states'' in the other. An \emph{instruction} of a Turing machine is a pair consisting of an action and a natural number (the next state). A \emph{program} @{term p} of a Turing machine is then a list of such pairs. Using as an example the following Turing machine program, which consists of four instructions % \begin{equation} \begin{tikzpicture} \node [anchor=base] at (0,0) {@{thm dither_def}}; \node [anchor=west] at (-1.5,-0.64) {$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm] = starting state\end{tabular}}}$}; \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$}; \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$}; \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$}; \end{tikzpicture} \label{dither} \end{equation} % \noindent the reader can see we have organised our Turing machine programs so that segments of two pairs belong to a state. The first component of such a segment determines what action should be taken and which next state should be transitioned to in case the head reads a @{term Bk}; similarly the second component determines what should be done in case of reading @{term Oc}. We have the convention that the first state is always the \emph{starting state} of the Turing machine. The @{text 0}-state is special in that it will be used as the ``halting state''. There are no instructions for the @{text 0}-state, but it will always perform a @{term Nop}-operation and remain in the @{text 0}-state. We have chosen a very concrete representation for Turing machine programs, because when constructing a universal Turing machine, we need to define a coding function for programs. %This can be directly done for our programs-as-lists, but is %slightly more difficult for the functions used by Asperti and Ricciotti. Given a program @{term p}, a state and the cell being scanned by the head, we need to fetch the corresponding instruction from the program. For this we define the function @{term fetch} \begin{equation}\label{fetch} \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} \multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\ @{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\ \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\ @{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\ \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}} \end{tabular}} \end{equation} \noindent In this definition the function @{term nth_of} returns the @{text n}th element from a list, provided it exists (@{term Some}-case), or if it does not, it returns the default action @{term Nop} and the default state @{text 0} (@{term None}-case). We often have to restrict Turing machine programs to be well-formed: a program @{term p} is \emph{well-formed} if it satisfies the following three properties: \begin{center} @{thm tm_wf_simps[where p="p", THEN eq_reflection]} \end{center} \noindent The first states that @{text p} must have at least an instruction for the starting state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every state, and the third that every next-state is one of the states mentioned in the program or being the @{text 0}-state. A \emph{configuration} @{term c} of a Turing machine is a state together with a tape. This is written as @{text "(s, (l, r))"}. We say a configuration \emph{is final} if @{term "s = (0::nat)"} and we say a predicate @{text P} \emph{holds for} a configuration if @{text "P"} holds for the tape @{text "(l, r)"}. If we have a configuration and a program, we can calculate what the next configuration is by fetching the appropriate action and next state from the program, and by updating the state and tape accordingly. This single step of execution is defined as the function @{term step} \begin{center} \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} @{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\ & & @{text "in (s', update (l, r) a)"} \end{tabular} \end{center} \noindent where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is empty it returns @{term Bk}. We lift this definition to an evaluation function that performs exactly @{text n} steps: \begin{center} \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\ @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\ \end{tabular} \end{center} \noindent Recall our definition of @{term fetch} (shown in \eqref{fetch}) with the default value for the @{text 0}-state. In case a Turing program takes according to the usual textbook definition, say \cite{Boolos87}, less than @{text n} steps before it halts, then in our setting the @{term steps}-evaluation does not actually halt, but rather transitions to the @{text 0}-state (the final state) and remains there performing @{text Nop}-actions until @{text n} is reached. We often need to restrict tapes to be in standard form, which means the left list of the tape is either empty or only contains @{text "Bk"}s, and the right list contains some ``clusters'' of @{text "Oc"}s separated by single blanks. To make this formal we define the following overloaded function encoding natural numbers into lists of @{term "Oc"}s and @{term Bk}s. % \begin{equation} \mbox{\begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{thm (lhs) nats2tape(6)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(6)}\\ @{thm (lhs) nats2tape(4)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(4)}\\ \end{tabular}\hspace{6mm} \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{thm (lhs) nats2tape(1)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(1)}\\ @{thm (lhs) nats2tape(2)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(2)}\\ @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)} \end{tabular}}\label{standard} \end{equation} % \noindent A \emph{standard tape} is then of the form @{text "(Bk\<^sup>k,\<langle>[n\<^sub>1,...,n\<^sub>m]\<rangle> @ Bk\<^sup>l)"} for some @{text k}, @{text l} and @{text "n\<^bsub>1...m\<^esub>"}. Note that the head in a standard tape ``points'' to the leftmost @{term "Oc"} on the tape. Note also that the natural number @{text 0} is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on. We need to be able to sequentially compose Turing machine programs. Given our concrete representation, this is relatively straightforward, if slightly fiddly. We use the following two auxiliary functions: \begin{center} \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\ @{thm (lhs) adjust_simps} @{text "\<equiv>"} @{thm (rhs) adjust_simps}\\ \end{tabular} \end{center} \noindent The first adds @{text n} to all states, except the @{text 0}-state, thus moving all ``regular'' states to the segment starting at @{text n}; the second adds @{term "Suc(length p div 2)"} to the @{text 0}-state, thus redirecting all references to the ``halting state'' to the first state after the program @{text p}. With these two functions in place, we can define the \emph{sequential composition} of two Turing machine programs @{text "p\<^sub>1"} and @{text "p\<^sub>2"} as \begin{center} @{thm tm_comp.simps[where ?p1.0="p\<^sub>1" and ?p2.0="p\<^sub>2", THEN eq_reflection]} \end{center} \noindent %This means @{text "p\<^sub>1"} is executed first. Whenever it originally %transitioned to the @{text 0}-state, it will in the composed program transition to the starting %state of @{text "p\<^sub>2"} instead. All the states of @{text "p\<^sub>2"} %have been shifted in order to make sure that the states of the composed %program @{text "p\<^sub>1 \<oplus> p\<^sub>2"} still only ``occupy'' %an initial segment of the natural numbers. \begin{figure}[t] \begin{center} \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} \begin{tabular}[t]{@ {}l@ {}} @{thm (lhs) tcopy_begin_def} @{text "\<equiv>"}\\ \hspace{2mm}@{text "["}@{text "(W\<^bsub>Bk\<^esub>, 0), (R, 2), (R, 3),"}\\ \hspace{2mm}\phantom{@{text "["}}@{text "(R, 2), (W\<^bsub>Oc\<^esub>, 3), (L, 4),"}\\ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (L, 0)"}@{text "]"} \end{tabular} & \begin{tabular}[t]{@ {}l@ {}} @{thm (lhs) tcopy_loop_def} @{text "\<equiv>"}\\ \hspace{2mm}@{text "["}@{text "(R, 0), (R, 2), (R, 3),"}\\ \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Bk\<^esub>, 2), (R, 3), (R, 4),"}\\ \hspace{2mm}\phantom{@{text "["}}@{text "(W\<^bsub>Oc\<^esub>, 5), (R, 4), (L, 6),"}\\ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (L, 6), (L, 1)"}@{text "]"} \end{tabular} & \begin{tabular}[t]{@ {}l@ {}} @{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\ \hspace{2mm}@{text "["}@{text "(L, 0), (R, 2), (W\<^bsub>Oc\<^esub>, 3),"}\\ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 4), (R, 2), (R, 2),"}\\ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5), (W\<^bsub>Bk\<^esub>, 4), (R, 0),"}\\ \hspace{2mm}\phantom{@{text "["}}@{text "(L, 5)"}@{text "]"} \end{tabular} \end{tabular}\\[2mm] \begin{tikzpicture}[scale=0.7] \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$}; \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$}; \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$}; \node [anchor=base] at (2.2,-0.6) {\small$\overbrace{@{term "tcopy_begin"}}^{}$}; \node [anchor=base] at (5.6,-0.6) {\small$\overbrace{@{term "tcopy_loop"}}^{}$}; \node [anchor=base] at (10.5,-0.6) {\small$\overbrace{@{term "tcopy_end"}}^{}$}; \begin{scope}[shift={(0.5,0)}] \draw[very thick] (-0.25,0) -- ( 1.25,0); \draw[very thick] (-0.25,0.5) -- ( 1.25,0.5); \draw[very thick] (-0.25,0) -- (-0.25,0.5); \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); \end{scope} \begin{scope}[shift={(2.9,0)}] \draw[very thick] (-0.25,0) -- ( 2.25,0); \draw[very thick] (-0.25,0.5) -- ( 2.25,0.5); \draw[very thick] (-0.25,0) -- (-0.25,0.5); \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); \draw[rounded corners=1mm] (0.15,-0.1) rectangle (0.85,0.6); \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); \end{scope} \begin{scope}[shift={(6.8,0)}] \draw[very thick] (-0.75,0) -- ( 3.25,0); \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5); \draw[very thick] (-0.75,0) -- (-0.75,0.5); \draw[very thick] (-0.25,0) -- (-0.25,0.5); \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); \draw[very thick] ( 2.75,0) -- ( 2.75,0.5); \draw[very thick] ( 3.25,0) -- ( 3.25,0.5); \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4); \draw[fill] ( 2.85,0.1) rectangle (3.15,0.4); \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); \end{scope} \begin{scope}[shift={(11.7,0)}] \draw[very thick] (-0.75,0) -- ( 3.25,0); \draw[very thick] (-0.75,0.5) -- ( 3.25,0.5); \draw[very thick] (-0.75,0) -- (-0.75,0.5); \draw[very thick] (-0.25,0) -- (-0.25,0.5); \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); \draw[very thick] ( 2.25,0) -- ( 2.25,0.5); \draw[very thick] ( 2.75,0) -- ( 2.75,0.5); \draw[very thick] ( 3.25,0) -- ( 3.25,0.5); \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); \draw[fill] ( 2.35,0.1) rectangle (2.65,0.4); \draw[fill] ( 2.85,0.1) rectangle (3.15,0.4); \draw[fill] ( 1.85,0.1) rectangle (2.15,0.4); \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); \draw[fill] ( 0.85,0.1) rectangle (1.15,0.4); \end{scope} \end{tikzpicture}\\[-8mm]\mbox{} \end{center} \caption{The three components of the \emph{copy Turing machine} (above). If started (below) with the tape @{term "([], <(2::nat)>)"} the first machine appends @{term "[Bk, Oc]"} at the end of the right tape; the second then ``moves'' all @{term Oc}s except the first from the beginning of the tape to the end; the third ``refills'' the original block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.} \label{copy} \end{figure} Before we can prove the undecidability of the halting problem for our Turing machines working on standard tapes, we have to analyse two concrete Turing machine programs and establish that they are correct---that means they are ``doing what they are supposed to be doing''. Such correctness proofs are usually left out in the informal literature, for example \cite{Boolos87}. The first program we need to prove correct is the @{term dither} program shown in \eqref{dither} and the second program is @{term "tcopy"} defined as \begin{equation} \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} \end{tabular}}\label{tcopy} \end{equation} \noindent whose three components are given in Figure~\ref{copy}. For our correctness proofs, we introduce the notion of total correctness defined in terms of \emph{Hoare-triples}, written @{term "{P} (p::tprog0) {Q}"}. They implement the idea that a program @{term p} started in state @{term "1::nat"} with a tape satisfying @{term P} will after some @{text n} steps halt (have transitioned into the halting state) with a tape satisfying @{term Q}. This idea is very similar to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. We also have \emph{Hoare-pairs} of the form @{term "{P} (p::tprog0) \<up>"} implementing the case that a program @{term p} started with a tape satisfying @{term P} will loop (never transition into the halting state). Both notion are formally defined as \begin{center} \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} \begin{tabular}[t]{@ {}l@ {}} \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm] \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ \hspace{7mm}if @{term "P tp"} holds then\\ \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\ \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\ \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"} \end{tabular} & \begin{tabular}[t]{@ {}l@ {}} \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm] \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ \hspace{7mm}if @{term "P tp"} holds then\\ \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"} \end{tabular} \end{tabular} \end{center} \noindent For our Hoare-triples we can easily prove the following Hoare-consequence rule \begin{equation} @{thm[mode=Rule] Hoare_consequence} \end{equation} \noindent where @{term "Turing_Hoare.assert_imp P' P"} stands for the fact that for all tapes @{term "tp"}, @{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}). Like Asperti and Ricciotti with their notion of realisability, we have set up our Hoare-rules so that we can deal explicitly with total correctness and non-termination, rather than have notions for partial correctness and termination. Although the latter would allow us to reason more uniformly (only using Hoare-triples), we prefer our definitions because we can derive below some simple Hoare-rules for sequentially composed Turing programs. In this way we can reason about the correctness of @{term "tcopy_begin"}, for example, completely separately from @{term "tcopy_loop"} and @{term "tcopy_end"}. It is relatively straightforward to prove that the Turing program @{term "dither"} shown in \eqref{dither} is correct. This program should be the ``identity'' when started with a standard tape representing @{text "1"} but loops when started with the @{text 0}-representation instead, as pictured below. \begin{center} \begin{tabular}{l@ {\hspace{3mm}}lcl} & \multicolumn{1}{c}{start tape}\\[1mm] \raisebox{2mm}{halting case:} & \begin{tikzpicture}[scale=0.8] \draw[very thick] (-2,0) -- ( 0.75,0); \draw[very thick] (-2,0.5) -- ( 0.75,0.5); \draw[very thick] (-0.25,0) -- (-0.25,0.5); \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); \draw[very thick] (-0.75,0) -- (-0.75,0.5); \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); \draw[very thick] (-1.25,0) -- (-1.25,0.5); \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); \node [anchor=base] at (-1.7,0.2) {\ldots}; \end{tikzpicture} & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} & \begin{tikzpicture}[scale=0.8] \draw[very thick] (-2,0) -- ( 0.75,0); \draw[very thick] (-2,0.5) -- ( 0.75,0.5); \draw[very thick] (-0.25,0) -- (-0.25,0.5); \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); \draw[very thick] (-0.75,0) -- (-0.75,0.5); \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); \draw[very thick] (-1.25,0) -- (-1.25,0.5); \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); \draw[fill] ( 0.35,0.1) rectangle (0.65,0.4); \node [anchor=base] at (-1.7,0.2) {\ldots}; \end{tikzpicture}\\ \raisebox{2mm}{non-halting case:} & \begin{tikzpicture}[scale=0.8] \draw[very thick] (-2,0) -- ( 0.25,0); \draw[very thick] (-2,0.5) -- ( 0.25,0.5); \draw[very thick] (-0.25,0) -- (-0.25,0.5); \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); \draw[very thick] (-0.75,0) -- (-0.75,0.5); \draw[very thick] (-1.25,0) -- (-1.25,0.5); \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); \draw[fill] (-0.15,0.1) rectangle (0.15,0.4); \node [anchor=base] at (-1.7,0.2) {\ldots}; \end{tikzpicture} & \raisebox{2mm}{$\;\;\large\Rightarrow\;\;$} & \raisebox{2mm}{loops} \end{tabular} \end{center} \noindent We can prove the following two Hoare-statements: \begin{center} \begin{tabular}{l} @{thm dither_halts}\\ @{thm dither_loops} \end{tabular} \end{center} \noindent The first is by a simple calculation. The second is by an induction on the number of steps we can perform starting from the input tape. The program @{term tcopy} defined in \eqref{tcopy} has 15 states; its purpose is to produce the standard tape @{term "(Bks, <(n, n::nat)>)"} when started with @{term "(Bks, <(n::nat)>)"}, that is making a copy of a value @{term n} on the tape. Reasoning about this program is substantially harder than about @{term dither}. To ease the burden, we derive the following two Hoare-rules for sequentially composed programs. \begin{center} \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{14mm}}c@ {}} $\inferrule*[Right=@{thm (prem 3) HR1}] {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}} {@{thm (concl) HR1}} $ & $ \inferrule*[Right=@{thm (prem 3) HR2}] {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}} {@{thm (concl) HR2}} $ \end{tabular} \end{center} \noindent The first corresponds to the usual Hoare-rule for composition of two terminating programs. The second rule gives the conditions for when the first program terminates generating a tape for which the second program loops. The side-conditions about @{thm (prem 3) HR2} are needed in order to ensure that the redirection of the halting and initial state in @{term "p\<^sub>1"} and @{term "p\<^sub>2"}, respectively, match up correctly. These Hoare-rules allow us to prove the correctness of @{term tcopy} by considering the correctness of the components @{term "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in isolation. This simplifies the reasoning considerably, for example when designing decreasing measures for proving the termination of the programs. We will show the details for the program @{term "tcopy_begin"}. For the two other programs we refer the reader to our formalisation. Given the invariants @{term "inv_begin0"},\ldots, @{term "inv_begin4"} shown in Figure~\ref{invbegin}, which correspond to each state of @{term tcopy_begin}, we define the following invariant for the whole @{term tcopy_begin} program: \begin{figure}[t] \begin{center} \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}} \hline @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\ @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\ @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\ @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\ & & @{thm (rhs) inv_begin02}\smallskip \\ \hline @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\ & & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\ @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\ \hline @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\ @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ \hline \end{tabular} \end{center} \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of @{term tcopy_begin}. Below, the invariants only for the starting and halting states of @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant, the parameter @{term n} stands for the number of @{term Oc}s with which the Turing machine is started.}\label{invbegin} \end{figure} \begin{center} \begin{tabular}{rcl} @{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} & @{text "if"} @{thm (prem 1) inv_begin_print(1)} @{text then} @{thm (rhs) inv_begin_print(1)}\\ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(2)} @{text then} @{thm (rhs) inv_begin_print(2)} \\ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(3)} @{text then} @{thm (rhs) inv_begin_print(3)}\\ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(4)} @{text then} @{thm (rhs) inv_begin_print(4)}\\ & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(5)} @{text then} @{thm (rhs) inv_begin_print(5)}\\ & & @{text else} @{thm (rhs) inv_begin_print(6)} \end{tabular} \end{center} \noindent This invariant depends on @{term n} representing the number of @{term Oc}s on the tape. It is not hard (26 lines of automated proof script) to show that for @{term "n > (0::nat)"} this invariant is preserved under the computation rules @{term step} and @{term steps}. This gives us partial correctness for @{term "tcopy_begin"}. We next need to show that @{term "tcopy_begin"} terminates. For this we introduce lexicographically ordered pairs @{term "(n, m)"} derived from configurations @{text "(s, (l, r))"} whereby @{text n} is the state @{text s}, but ordered according to how @{term tcopy_begin} executes them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have a strictly decreasing measure, @{term m} takes the data on the tape into account and is calculated according to the following measure function: \begin{center} \begin{tabular}{rcl} @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\ & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} @{text "("}@{thm (rhs) measure_begin_print(2)}@{text ")"} \\ & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\ & & @{text else} @{thm (rhs) measure_begin_print(4)}\\ \end{tabular} \end{center} \noindent With this in place, we can show that for every starting tape of the form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing machine @{term "tcopy_begin"} will eventually halt (the measure decreases in each step). Taking this and the partial correctness proof together, we obtain the Hoare-triple shown on the left for @{term tcopy_begin}: \begin{center} @{thm (concl) begin_correct}\hspace{6mm} @{thm (concl) loop_correct}\hspace{6mm} @{thm (concl) end_correct} \end{center} \noindent where we assume @{text "0 < n"} (similar reasoning is needed for the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of the halting state of @{term tcopy_begin} implies the invariant of the starting state of @{term tcopy_loop}, that is @{term "Turing_Hoare.assert_imp (inv_begin0 n) (inv_loop1 n)"} holds, and also @{term "inv_loop0 n = inv_end1 n"}, we can derive the following Hoare-triple for the correctness of @{term tcopy}: \begin{center} @{thm tcopy_correct} \end{center} \noindent That means if we start with a tape of the form @{term "([], <n::nat>)"} then @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}, as desired. Finally, we are in the position to prove the undecidability of the halting problem. A program @{term p} started with a standard tape containing the (encoded) numbers @{term ns} will \emph{halt} with a standard tape containing a single (encoded) number is defined as \begin{center} @{thm halts_def} \end{center} \noindent This roughly means we considering only Turing machine programs representing functions that take some numbers as input and produce a single number as output. For undecidability, the property we are proving is that there is no Turing machine that can decide in general whether a Turing machine program halts (answer either @{text 0} for halting or @{text 1} for looping). Given our correctness proofs for @{term dither} and @{term tcopy} shown above, this non-existence is now relatively straightforward to establish. We first assume there is a coding function, written @{term "code M"}, which represents a Turing machine @{term "M"} as a natural number. No further assumptions are made about this coding function. Suppose a Turing machine @{term H} exists such that if started with the standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0}, respectively @{text 1}, depending on whether @{text M} halts or not when started with the input tape containing @{term "<ns>"}. This assumption is formalised as follows---for all @{term M} and all lists of natural numbers @{term ns}: \begin{center} \begin{tabular}{r} @{thm (prem 2) uncomputable.h_case} implies @{thm (concl) uncomputable.h_case}\\ @{thm (prem 2) uncomputable.nh_case} implies @{thm (concl) uncomputable.nh_case} \end{tabular} \end{center} \noindent The contradiction can be derived using the following Turing machine \begin{center} @{thm tcontra_def} \end{center} \noindent Suppose @{thm (prem 1) "tcontra_halt"} holds. Given the invariants @{text "P\<^sub>1"}\ldots@{text "P\<^sub>3"} shown on the left, we can derive the following Hoare-pair for @{term tcontra} on the right. \begin{center}\small \begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}} \begin{tabular}[t]{@ {}l@ {}} @{term "P\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ @{term "P\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ @{term "P\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"} \end{tabular} & \begin{tabular}[b]{@ {}l@ {}} \raisebox{-20mm}{$\inferrule*{ \inferrule*{@{term "{P\<^sub>1} tcopy {P\<^sub>2}"} \\ @{term "{P\<^sub>2} H {P\<^sub>3}"}} {@{term "{P\<^sub>1} (tcopy |+| H) {P\<^sub>3}"}} \\ @{term "{P\<^sub>3} dither \<up>"} } {@{term "{P\<^sub>1} tcontra \<up>"}} $} \end{tabular} \end{tabular} \end{center} \noindent This Hoare-pair contradicts our assumption that @{term tcontra} started with @{term "<(code tcontra)>"} halts. Suppose @{thm (prem 1) "tcontra_unhalt"} holds. Again, given the invariants @{text "Q\<^sub>1"}\ldots@{text "Q\<^sub>3"} shown on the left, we can derive the Hoare-triple for @{term tcontra} on the right. \begin{center}\small \begin{tabular}{@ {}c@ {\hspace{-18mm}}c@ {}} \begin{tabular}[t]{@ {}l@ {}} @{term "Q\<^sub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ @{term "Q\<^sub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ @{term "Q\<^sub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"} \end{tabular} & \begin{tabular}[t]{@ {}l@ {}} \raisebox{-20mm}{$\inferrule*{ \inferrule*{@{term "{Q\<^sub>1} tcopy {Q\<^sub>2}"} \\ @{term "{Q\<^sub>2} H {Q\<^sub>3}"}} {@{term "{Q\<^sub>1} (tcopy |+| H) {Q\<^sub>3}"}} \\ @{term "{Q\<^sub>3} dither {Q\<^sub>3}"} } {@{term "{Q\<^sub>1} tcontra {Q\<^sub>3}"}} $} \end{tabular} \end{tabular} \end{center} \noindent This time the Hoare-triple states that @{term tcontra} terminates with the ``output'' @{term "<(1::nat)>"}. In both cases we come to a contradiction, which means we have to abandon our assumption that there exists a Turing machine @{term H} which can in general decide whether Turing machines terminate.*}section {* Abacus Machines *}text {* \noindent Boolos et al \cite{Boolos87} use abacus machines as a stepping stone for making it less laborious to write Turing machine programs. Abacus machines operate over a set of registers @{text "R\<^sub>0"}, @{text "R\<^sub>1"}, \ldots{}, @{text "R\<^sub>n"} each being able to hold an arbitrary large natural number. We use natural numbers to refer to registers; we also use a natural number to represent a program counter and to represent jumping ``addresses'', for which we use the letter @{text l}. An abacus program is a list of \emph{instructions} defined by the datatype: \begin{center} \begin{tabular}{rcl@ {\hspace{10mm}}l} @{text "i"} & $::=$ & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\ & $\mid$ & @{term "Dec R\<iota> l"} & if content of @{text R} is non-zero, then decrement it by one\\ & & & otherwise jump to instruction @{text l}\\ & $\mid$ & @{term "Goto l"} & jump to instruction @{text l} \end{tabular} \end{center} \noindent For example the program clearing the register @{text R} (that is setting it to @{term "(0::nat)"}) can be defined as follows: \begin{center} @{thm clear.simps[where n="R\<iota>" and e="l", THEN eq_reflection]} \end{center} \noindent Running such a program means we start with the first instruction then execute one instructions after the other, unless there is a jump. For example the second instruction @{term "Goto 0"} above means we jump back to the first instruction thereby closing the loop. Like with our Turing machines, we fetch instructions from an abacus program such that a jump out of ``range'' behaves like a @{term "Nop"}-action. In this way it is again easy to define a function @{term steps} that executes @{term n} instructions of an abacus program. A \emph{configuration} of an abacus machine is the current program counter together with a snapshot of all registers. By convention the value calculated by an abacus program is stored in the last register (the one with the highest index in the program). The main point of abacus programs is to be able to translate them to Turing machine programs. Registers and their content are represented by standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it is impossible to build Turing machine programs out of components using our @{text ";"}-operation shown in the previous section. To overcome this difficulty, we calculate a \emph{layout} of an abacus program as follows \begin{center} \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{thm (lhs) layout(1)} & @{text "\<equiv>"} & @{thm (rhs) layout(1)}\\ @{thm (lhs) layout(2)} & @{text "\<equiv>"} & @{thm (rhs) layout(2)}\\ @{thm (lhs) layout(3)} & @{text "\<equiv>"} & @{thm (rhs) layout(3)}\\ @{thm (lhs) layout(4)} & @{text "\<equiv>"} & @{thm (rhs) layout(4)}\\ \end{tabular} \end{center} \noindent This gives us a list of natural numbers specifying how many states are needed to translate each abacus instruction. This information is needed in order to calculate the state where the Turing machine program of an abacus instruction starts. This can be defined as \begin{center} @{thm address.simps[where x="n"]} \end{center} \noindent where @{text p} is an abacus program and @{term "take n"} takes the first @{text n} elements from a list. The @{text Goto} instruction is easiest to translate requiring only one state, namely the Turing machine program: \begin{center} @{text "translate_Goto l"} @{text "\<equiv>"} @{thm (rhs) tgoto.simps[where n="l"]} \end{center} \noindent where @{term "l"} is the state in the Turing machine program to jump to. For translating the instruction @{term "Inc R\<iota>"}, one has to remember that the content of the registers are encoded in the Turing machine as a standard tape. Therefore the translated Turing machine needs to first find the number corresponding to the content of register @{text "R"}. This needs a machine with @{term "(2::nat) * R\<iota>"} states and can be constructed as follows: \begin{center} \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{thm (lhs) findnth.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) findnth.simps(1)}\\ @{thm (lhs) findnth.simps(2)} & @{text "\<equiv>"}\\ \multicolumn{3}{@ {}l@ {}}{\hspace{6mm}@{thm (rhs) findnth.simps(2)}}\\ \end{tabular} \end{center} \noindent Then we need to increase the ``number'' on the tape by one, and adjust the following ``registers''. For adjusting we only need to change the first @{term Oc} of each number to @{term Bk} and the last one from @{term Bk} to @{term Oc}. Finally, we need to transition the head of the Turing machine back into the standard position. This requires a Turing machine with 9 states (we omit the details). Similarly for the translation of @{term "Dec R\<iota> l"}, where the translated Turing machine needs to first check whether the content of the corresponding register is @{text 0}. For this we have a Turing machine program with @{text 16} states (again the details are omitted). Finally, having a Turing machine for each abacus instruction we need to ``stitch'' the Turing machines together into one so that each Turing machine component transitions to next one, just like in the abacus programs. One last problem to overcome is that an abacus program is assumed to calculate a value stored in the last register (the one with the highest register). That means we have to append a Turing machine that ``mops up'' the tape (cleaning all @{text Oc}s) except for the @{term Oc}s of the last register represented on the tape. This needs a Turing machine program with @{text "2 * R + 6"} states, assuming @{text R} is the number of registers to be ``cleaned''. While generating the Turing machine program for an abacus program is not too difficult to formalise, the problem is that it contains @{text Goto}s all over the place. The unfortunate result is that we cannot use our Hoare-rules for reasoning about sequentially composed programs (for this each component needs to be completely independent). Instead we have to treat the translated Turing machine as one ``big block'' and prove as invariant that it performs the same operations as the abacus program. For this we have to show that for each configuration of an abacus machine the @{term step}-function is simulated by zero or more steps in our translated Turing machine. This leads to a rather large ``monolithic'' correctness proof (4600 loc and 380 sublemmas) that on the conceptual level is difficult to break down into smaller components. %We were able to simplify the proof somewhat*}section {* Recursive Functions and a Universal Turing Machine *}text {* The main point of recursive functions is that we can relatively easily construct a universal Turing machine via a universal function. This is different from Norrish \cite{Norrish11} who gives a universal function for the lambda-calculus, and also from Asperti and Ricciotti \cite{AspertiRicciotti12} who construct a universal Turing machine directly, but for simulating Turing machines with a more restricted alphabet. Unlike Norrish \cite{Norrish11}, we need to represent recursive functions ``deeply'' because we want to translate them to abacus programs. Thus \emph{recursive functions} are defined as the datatype \begin{center} \begin{tabular}{c@ {\hspace{4mm}}c} \begin{tabular}{rcl@ {\hspace{4mm}}l} @{term r} & @{text "::="} & @{term z} & (zero-function)\\ & @{text "|"} & @{term s} & (successor-function)\\ & @{text "|"} & @{term "id n m"} & (projection)\\ \end{tabular} & \begin{tabular}{cl@ {\hspace{4mm}}l} @{text "|"} & @{term "Cn n f fs"} & (composition)\\ @{text "|"} & @{term "Pr n f\<^sub>1 f\<^sub>2"} & (primitive recursion)\\ @{text "|"} & @{term "Mn n f"} & (minimisation)\\ \end{tabular} \end{tabular} \end{center} \noindent where @{text n} indicates the function expects @{term n} arguments (in \cite{Boolos87} both @{text z} and @{term s} expect one argument), and @{text fs} stands for a list of recursive functions. Since we know in each case the arity, say @{term l}, we can define an evaluation function, called @{term rec_exec}, that takes a recursive function @{text f} and a list @{term ns} of natural numbers of length @{text l} as arguments. Since this evaluation function uses the minimisation operator from HOL, this function might not terminate always. As a result we also need to inductively characterise when @{term rec_exec} terminates. We omit the definitions for @{term "rec_exec f ns"} and @{term "terminate f ns"}. Because of space reasons, we also omit the definition of translating recursive functions into abacus programs. We can prove, however, the following theorem about the translation: If @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="f" and args="ns"]} holds for the recursive function @{text f} and arguments @{term ns}, then the following Hoare-triple holds \begin{center} @{thm (concl) recursive_compile_to_tm_correct3[where recf="f" and args="ns"]} \end{center} \noindent for the Turing machine generated by @{term "translate f"}. This means the translated Turing machine if started with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate with the standard tape @{term "(Bk \<up> k, <(rec_exec f ns)::nat> @ Bk \<up> l)"} for some @{text k} and @{text l}. Having recursive functions under our belt, we can construct a universal function, written @{text UF}. This universal function acts like an interpreter for Turing machines. It takes two arguments: one is the code of the Turing machine to be interpreted and the other is the ``packed version'' of the arguments of the Turing machine. We can then consider how this universal function is translated to a Turing machine and from this construct the universal Turing machine, written @{term UTM}. It is defined as the composition of the Turing machine that packages the arguments and the translated recursive function @{text UF}: \begin{center} @{text "UTM \<equiv> arg_coding ; (translate UF)"} \end{center} \noindent Suppose a Turing program @{term p} is well-formed and when started with the standard tape containing the arguments @{term args}, will produce a standard tape with ``output'' @{term n}. This assumption can be written as the Hoare-triple \begin{center} @{thm (prem 3) UTM_halt_lemma2} \end{center} \noindent where we require that the @{term args} stand for a non-empty list. Then the universal Turing machine @{term UTM} started with the code of @{term p} and the arguments @{term args}, calculates the same result, namely \begin{center} @{thm (concl) UTM_halt_lemma2} \end{center} \noindent Similarly, if a Turing program @{term p} started with the standard tape containing @{text args} loops, which is represented by the Hoare-pair \begin{center} @{thm (prem 2) UTM_unhalt_lemma2} \end{center} \noindent then the universal Turing machine started with the code of @{term p} and the arguments @{term args} will also loop \begin{center} @{thm (concl) UTM_unhalt_lemma2} \end{center} %Analysing the universal Turing machine constructed in \cite{Boolos87} more carefully %we can strengthen this result slightly by observing that @{text m} is at most %2 in the output tape. This observation allows one to construct a universal Turing machine that works %entirely on the left-tape by composing it with a machine that drags the tape %two cells to the right. A corollary is that one-sided Turing machines (where the %tape only extends to the right) are computationally as powerful as our two-sided %Turing machines. So our undecidability proof for the halting problem extends %also to one-sided Turing machines, which is needed for example in order to %formalise the undecidability of Wang's tiling problem \cite{Robinson71}. While formalising the chapter in \cite{Boolos87} about universal Turing machines, an unexpected outcome of our work is that we identified an inconsistency in their use of a definition. This is unexpected since \cite{Boolos87} is a classic textbook which has undergone several editions (we used the fifth edition; the material containing the inconsistency was introduced in the fourth edition of this book). The central idea about Turing machines is that when started with standard tapes they compute a partial arithmetic function. The inconsistency arises when they define the case when this function should \emph{not} return a result. Boolos at al write in Chapter 3, Page 32: \begin{quote}\it ``If the function that is to be computed assigns no value to the arguments that are represented initially on the tape, then the machine either will never halt, \colorbox{mygrey}{or} will halt in some nonstandard configuration\ldots'' \end{quote} \noindent Interestingly, they do not implement this definition when constructing their universal Turing machine. In Chapter 8, on page 93, a recursive function @{term stdh} is defined as: \begin{equation}\label{stdh_def} @{text "stdh(m, x, t) \<equiv> stat(conf(m, x, t)) + nstd(conf(m, x, t))"} \end{equation} \noindent where @{text "stat(conf(m, x, t))"} computes the current state of the simulated Turing machine, and @{text "nstd(conf(m, x, t))"} returns @{text 1} if the tape content is non-standard. If either one evaluates to something that is not zero, then @{text "stdh(m, x, t)"} will be not zero, because of the $+$-operation. On the same page, a function @{text "halt(m, x)"} is defined in terms of @{text stdh} for computing the steps the Turing machine needs to execute before it halts (in case it halts at all). According to this definition, the simulated Turing machine will continue to run after entering the @{text 0}-state with a non-standard tape. The consequence of this inconsistency is that there exist Turing machines that given some arguments do not compute a value according to Chapter 3, but return a proper result according to the definition in Chapter 8. One such Turing machine is: %This means that if you encode the plus function but only give one argument, %then the TM will either loop {\bf or} stop with a non-standard tape %But in the definition of the universal function the TMs will never stop %with non-standard tapes. %SO the following TM calculates something according to def from chap 8, %but not with chap 3. For example: \begin{center} @{term "counter_example \<equiv> [(L, (0::nat)), (L, 2), (R, 2), (R, 0)]"} \end{center} \noindent If started with standard tape @{term "([], [Oc])"}, it halts with the non-standard tape @{term "([Oc, Bk], [])"} according to the definition in Chapter 3---so no result is calculated; but with the standard tape @{term "([Bk], [Oc])"} according to the definition in Chapter 8. We solve this inconsistency in our formalisation by setting up our definitions so that the @{text counter_example} Turing machine does not produce any result by looping forever fetching @{term Nop}s in state @{text 0}. This solution implements essentially the definition in Chapter 3; it differs from the definition in Chapter 8, where perplexingly the instruction from state @{text 1} is fetched.*}(*section {* XYZ *}text {*One of the main objectives of the paper is the construction and verification of Universal Turing machine (UTM). A UTM takes the code of any Turing machine $M$ and its arguments $a_1, a_2, \ldots, a_n$ as input and computes to the same effect as $M$ does on $a_1, a_2, \ldots, a_n$. That is to say:\begin{enumerate} \item If $M$ terminates and gives a result on $a_1, a_2, \ldots, a_n$, so does $UTM$ on input $ code(M), a_1, a_1, a_2, \ldots, a_n $. \item If $M$ loops forever on $a_1, a_2, \ldots, a_n$, then $UTM$ does the same on $code (M), a_1, a_1, a_2, \ldots, a_n$.\end{enumerate}The existence of UTM is the cornerstone of {\em Turing Thesis}, which says: any effectively computable function can be computed by a Turing Machine. The evaluation of Turing machine is obviously effective computable (otherwise, Turing machine is not an effect computation model). So, if the evaluation function of Turing machine can not be implemented by a Turing machine, the {\em Turing Thesis} would fail. Although people believe that UTM exists, few have gave one in close form and prove its correctness with the only exception of Asperti.The method to obtain Universal Turing machine (UTM), as hinted by Boolos's book, is first constructing a recursive function recF (named Universal Function), which serves as an interpreter for Turing machine program, and then the UTM is obtained by $translate(recF)$. However, since any particular recursive function only takes fixed number of arguments determined by its construction, no matter how recF is constructed, it can only server as interpret for Turing machines which take the fixed number of arguments as input. Our solution is to precede the $translate(recF)$ with a Turing machine which compacts multiple arguments into one argument using Wang's coding. Now, $recF$ is defined as a function taking two arguments, where the first is the code of Turing machine to be interpreted and the second is the packed arguments.The construction of recF roughly follows the idea in the book. Since the book gives no correctness proof of the construction (not even an informal one), we have to formulate the correctness statements and as well as their formal proofs explicitly. As an unexpected outcome of this formulation, we identified one inconsistency in Boolos' book. Every Turing machine is supposed to compute an arithmetic function which is possibly partial. When the TM is started with an argument where the function is undefined, the definition on Chapter 3 (page 32) says:\begin{quote}(e) If the function that is to be computed assigns no value to the arguments that arerepresented initially on the tape, then the machine either will never halt, or willhalt in some nonstandard configuration such as $B_n11111$ or $B11_n111$ or $B11111_n$.\end{quote}According to this definition, a TM can signify a non-result either by looping forever or get into state 0 with a nonstandard tape. However, when we were trying to formalize the universal function in Chapter 8, we found the definition given there is not in accordance. On page 93, an recursive function $stdh$ is defined as: \begin{equation}\label{stdh_def}stdh(m, x, t) = stat(conf(m, x, t)) + nstd(conf(m, x, t))\end{equation}Where $ stat(conf(m, x, t)) $ computes the current state of the simulated Turing machine, and the $nstd(conf(m, x, t))$ returns $1$ if the tape content is nonstandard. If either one evaluates to nonzero, stdh(m, x, t) will be nonzero, because of the $+$ operation. One the same page, a function $halt(m, x)$ is defined to in terms of $stdh$ to computes the steps the Turing machine needs to execute before halt, which stipulates the TM halts when nstd(conf(m, x, t)) returns $0$. According to this definition, the simulated Turing machine will continue to run after getting into state $0$ with a nonstandard tape. The consequence of this inconsistency is that: there exists Turing machines which computes non-value according to Chapter 3, but returns a proper result according to Chapter 8. One such Truing machine is: \begin{equation}\label{contrived_tm} [(L, 0), (L, 2), (R, 2), (R, 0)] \end{equation}Starting in a standard configuration (1, [], [Oc]), it goes through the following series of configurations leading to state 0:\[(1, [], [Oc]) \rightsquigarrow (L, 2) \rightsquigarrow (2, [], [Bk, Oc]) \rightsquigarrow (R, 2)\rightsquigarrow (2, [Bk], [Oc]) \rightsquigarrow (R, 0)\rightsquigarrow (0, [Bk, Oc], [])\]According to Chapter 3, this Turing machine halts and gives a non-result. According to Chapter 8, it will continue to fetch and execute the next instruction. The fetching function $actn$ and $newstat$ in \eqref{fetch-def} (taken from page 92) takes $q$ as current state and $r$ as the currently scanned cell.\begin{equation}\label{fetch-def}\begin{aligned} actn(m, q, r ) &= ent(m, 4(q - 1) + 2 \cdot scan(r )) \\newstat(m, q, r ) & = ent(m, (4(q - 1) + 2 \cdot scan(r )) + 1)\end{aligned}\end{equation}For our instance, $q=0$ and $r = 1$. Because $q - 1 = 0 - 1 = 1 - 1 = 0$, the instruction fetched by \eqref{fetch-def} at state $0$ will be the same as if the machine is at state $0$. So the Turing machine will go through the follow execution and halt with a standard tape:\[(0, [Bk, Oc], []) \rightsquigarrow (L, 0) \rightsquigarrow (0, [Bk], [Oc])\]In summary, according to Chapter 3, the Turing machine in \eqref{contrived_tm} computes non-result and according to Chapter 8, it computes an identify function. *}*)(*section {* Wang Tiles\label{Wang} *}text {* Used in texture mapings - graphics*}*)section {* Conclusion *}text {* In previous works we were unable to formalise results about computability because in Isabelle/HOL we cannot, for example, represent the decidability of a predicate @{text P}, say, as the formula @{term "P \<or> \<not>P"}. For reasoning about computability we need to formalise a concrete model of computations. We could have followed Norrish \cite{Norrish11} using the $\lambda$-calculus as the starting point for formalising computability theory, but then we would have to reimplement on the ML-level his infrastructure for rewriting $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that can rewrite terms modulo an arbitrary equivalence relation, which Isabelle unfortunately does not yet have. Even though, we would still need to connect $\lambda$-terms somehow to Turing machines for proofs that make essential use of them (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}). We therefore have formalised Turing machines in the first place and the main computability results from Chapters 3 to 8 in the textbook by Boolos et al \cite{Boolos87}. For this we did not need to implement anything on the ML-level of Isabelle/HOL. While formalising the six chapters of \cite{Boolos87} we have found an inconsistency in Boolos et al's definitions of what function a Turing machine calculates. In Chapter 3 they use a definition that states a function is undefined if the Turing machine loops \emph{or} halts with a non-standard tape. Whereas in Chapter 8 about the universal Turing machine, the Turing machines will \emph{not} halt unless the tape is in standard form. Like Nipkow \cite{Nipkow98} observed with his formalisation of a textbook, we found that Boolos et al are (almost) right. We have not attempted to formalise everything precisely as Boolos et al present it, but use definitions that make our mechanised proofs manageable. For example our definition of the halting state performing @{term Nop}-operations seems to be non-standard, but very much suited to a formalisation in a theorem prover where the @{term steps}-function needs to be total. Norrish mentions that formalising Turing machines would be a ``\emph{daunting prospect}'' \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to some slick mechanised proofs, our experience is that Turing machines are not too daunting if one is only concerned with formalising the undecidability of the halting problem for Turing machines. As a point of comparison, the halting problem took us around 1500 loc of Isar-proofs, which is just one-and-a-half times of a mechanised proof pearl about the Myhill-Nerode theorem. So our conclusion is that this part is not as daunting as we estimated when reading the paper by Norrish \cite{Norrish11}. The work involved with constructing a universal Turing machine via recursive functions and abacus machines, we agree, is not a project one wants to undertake too many times (our formalisation of abacus machines and their correct translation is approximately 4600 loc; recursive functions 2800 loc and the universal Turing machine 10000 loc). Our work is also very much inspired by the formalisation of Turing machines of Asperti and Ricciotti \cite{AspertiRicciotti12} in the Matita theorem prover. It turns out that their notion of realisability and our Hoare-triples are very similar, however we differ in some basic definitions for Turing machines. Asperti and Ricciotti are interested in providing a mechanised foundation for complexity theory. They formalised a universal Turing machine (which differs from ours by using a more general alphabet), but did not describe an undecidability proof. Given their definitions and infrastructure, we expect however this should not be too difficult for them. For us the most interesting aspects of our work are the correctness proofs for Turing machines. Informal presentations of computability theory often leave the constructions of particular Turing machines as exercise to the reader, for example \cite{Boolos87}, deeming it to be just a chore. However, as far as we are aware all informal presentations leave out any arguments why these Turing machines should be correct. This means the reader is left with the task of finding appropriate invariants and measures for showing the correctness and termination of these Turing machines. Whenever we can use Hoare-style reasoning, the invariants are relatively straightforward and again as a point of comparison much smaller than for example the invariants used by Myreen in a correctness proof of a garbage collector written in machine code \cite[Page 76]{Myreen09}. However, the invariant needed for the abacus proof, where Hoare-style reasoning does not work, is similar in size as the one by Myreen and finding a sufficiently strong one took us, like Myreen, something on the magnitude of weeks. Our reasoning about the invariants is not much supported by the automation beyond the standard automation tools available in Isabelle/HOL. There is however a tantalising connection between our work and very recent work by Jensen et al \cite{Jensen13} on verifying X86 assembly code that might change that. They observed a similar phenomenon with assembly programs where Hoare-style reasoning is sometimes possible, but sometimes it is not. In order to ease their reasoning, they introduced a more primitive specification logic, on which Hoare-rules can be provided for special cases. It remains to be seen whether their specification logic for assembly code can make it easier to reason about our Turing programs. That would be an attractive result, because Turing machine programs are very much like assembly programs and it would connect some very classic work on Turing machines to very cutting-edge work on machine code verification. In order to try out such ideas, our formalisation provides the ``playground''. The code of our formalisation is available from the Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}. \medskip \noindent {\bf Acknowledgements:} We are very grateful for the extremely helpful comments by the anonymous reviewers.*}(*<*)endend(*>*)