--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/Paper.thy Sat Jul 27 08:17:54 2013 +0200
@@ -0,0 +1,1695 @@
+(*<*)
+theory Paper
+imports "../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.adjust
+
+abbreviation
+ "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 uncomputable
+begin
+
+notation (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\<^isub>0") and
+ inv_begin1 ("I\<^isub>1") and
+ inv_begin2 ("I\<^isub>2") and
+ inv_begin3 ("I\<^isub>3") and
+ inv_begin4 ("I\<^isub>4") and
+ inv_begin ("I\<^bsub>cbegin\<^esub>") and
+ inv_loop1 ("J\<^isub>1") and
+ inv_loop0 ("J\<^isub>0") and
+ inv_end1 ("K\<^isub>1") and
+ inv_end0 ("K\<^isub>0") and
+ measure_begin_step ("M\<^bsub>cbegin\<^esub>") and
+ layout_of ("layout") and
+ findnth ("find'_nth") and
+ recf.id ("id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
+ Pr ("Pr\<^isup>_") and
+ Cn ("Cn\<^isup>_") and
+ Mn ("Mn\<^isup>_") 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_def
+unfolding inv_loop1.simps inv_begin0.simps
+apply(auto)
+apply(rule_tac x="1" in exI)
+apply(auto simp add: replicate.simps)
+done
+
+lemma inv2:
+ shows "0 < n \<Longrightarrow> inv_loop0 n = inv_end1 n"
+apply(rule ext)
+apply(case_tac x)
+apply(simp add: inv_end1.simps)
+done
+
+
+lemma 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\<^isub>1" and B="p\<^isub>2"]
+
+lemmas HR2 =
+ Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>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 auto
+
+
+lemma 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)
+ run
+where
+ "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)+
+done
+
+lemma 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.
+
+\noindent
+We like to enable Isabelle/HOL users to reason about computability
+theory. Reasoning about decidability of predicates, for example, is not as
+straightforward as one might think in Isabelle/HOL and other HOL
+theorem provers, since they 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 the predicate @{text P} is constructed by
+computable means.
+
+Norrish formalised computability
+theory in HOL4. He choose the $\lambda$-calculus as the starting point
+for his formalisation because of its ``simplicity'' \cite[Page
+297]{Norrish11}. Part of his formalisation is a clever infrastructure
+for reducing $\lambda$-terms. He also established the computational
+equivalence between the $\lambda$-calculus and recursive functions.
+Nevertheless he concluded that it would be appealing to have
+formalisations for more operational models of computations, such as
+Turing machines or register machines. One reason is that many proofs
+in the literature use them. He noted however that \cite[Page
+310]{Norrish11}:
+
+\begin{quote}
+\it``If register machines are unappealing because of their
+general fiddliness,\\ Turing machines are an even more
+daunting prospect.''
+\end{quote}
+
+\noindent
+In this paper we take on this daunting prospect and provide a
+formalisation of Turing machines, as well as abacus machines (a kind
+of register machines) and recursive functions. To see the difficulties
+involved with this work, one has to understand that Turing machine
+programs (similarly abacus programs) can be completely
+\emph{unstructured}, behaving similar to Basic programs containing the
+infamous goto \cite{Dijkstra68}. This precludes in the general case a
+compositional Hoare-style reasoning about Turing programs. We provide
+such Hoare-rules for when it \emph{is} possible to reason in a
+compositional manner (which is fortunately quite often), but also
+tackle the more complicated case when we translate abacus programs
+into Turing programs. This reasoning about concrete Turing machine
+programs 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 of
+the work by Asperti and Ricciotti \cite{AspertiRicciotti12}. They
+describe a complete formalisation of Turing machines in the Matita
+theorem prover, including a universal Turing machine. However, they do
+\emph{not} formalise the undecidability of the halting problem since
+their main focus is complexity, rather than computability theory. They
+also report that the informal proofs from which they started are not
+``sufficiently accurate to be directly usable as a guideline for
+formalization'' \cite[Page 2]{AspertiRicciotti12}. For our
+formalisation we follow mainly the proofs from the textbook by Boolos
+et al \cite{Boolos87} and found that the description there is quite
+detailed. Some details are left out however: for example, constructing
+the \emph{copy Turing machine} is left as an exercise to the
+reader---a corresponding correctness proof is not mentioned at all; also \cite{Boolos87}
+only shows how the universal Turing machine is constructed for Turing
+machines computing unary functions. We had to figure out a way to
+generalise this result to $n$-ary functions. Similarly, when compiling
+recursive functions to abacus machines, the textbook again only shows
+how it can be done for 2- and 3-ary functions, but in the
+formalisation we need arbitrary functions. But the general ideas for
+how to do this are clear enough in \cite{Boolos87}.
+%However, one
+%aspect that is completely left out from the informal description in
+%\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing
+%machines are correct. We will introduce Hoare-style proof rules
+%which help us with such correctness arguments of Turing machines.
+
+The main difference between our formalisation and the one by Asperti
+and Ricciotti is that their universal Turing machine uses a different
+alphabet than the machines it simulates. They write \cite[Page
+23]{AspertiRicciotti12}:
+
+\begin{quote}\it
+``In particular, the fact that the universal machine operates with a
+different alphabet with respect to the machines it simulates is
+annoying.''
+\end{quote}
+
+\noindent
+In this paper we follow the approach by Boolos et al \cite{Boolos87},
+which goes back to Post \cite{Post36}, where all Turing machines
+operate on tapes that contain only \emph{blank} or \emph{occupied} cells.
+Traditionally the content of a cell can be any
+character from a finite alphabet. Although computationally equivalent,
+the more restrictive notion of Turing machines in \cite{Boolos87} makes
+the reasoning more uniform. In addition some proofs \emph{about} Turing
+machines are simpler. The reason is that one often needs to encode
+Turing machines---consequently if the Turing machines are simpler, then the coding
+functions are simpler too. Unfortunately, the restrictiveness also makes
+it harder to design programs for these Turing machines. In order
+to construct a universal Turing machine we therefore do not follow
+\cite{AspertiRicciotti12}, instead follow the proof in
+\cite{Boolos87} by translating abacus machines to Turing machines and in
+turn recursive functions to abacus machines. The universal Turing
+machine 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 instruction
+set than the one described in \cite{Boolos87}.
+
+\smallskip
+\noindent
+{\bf Contributions:} We formalised in Isabelle/HOL Turing machines
+following the description of Boolos et al \cite{Boolos87} where tapes
+only have blank or occupied cells. We mechanise the undecidability of
+the halting problem and prove the correctness of concrete Turing
+machines that are needed in this proof; such correctness proofs are
+left out in the informal literature. For reasoning about Turing
+machine programs we derive Hoare-rules. We also construct the
+universal Turing machine from \cite{Boolos87} by translating recursive
+functions to abacus machines and abacus machines to Turing
+machines. 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 of
+what 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\<^isup>k,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle> @ Bk\<^isup>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\<^isub>1"} and @{text "p\<^isub>2"} as
+
+ \begin{center}
+ @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
+ \end{center}
+
+ \noindent
+ %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+ %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
+ %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+ %have been shifted in order to make sure that the states of the composed
+ %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
+ %an initial segment of the natural numbers.
+
+ \begin{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\<^isub>1"} and @{term "p\<^isub>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\<^isub>1"}\ldots@{text "P\<^isub>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\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+ @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+ @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
+ \end{tabular}
+ &
+ \begin{tabular}[b]{@ {}l@ {}}
+ \raisebox{-20mm}{$\inferrule*{
+ \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
+ {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
+ \\ @{term "{P\<^isub>3} dither \<up>"}
+ }
+ {@{term "{P\<^isub>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\<^isub>1"}\ldots@{text "Q\<^isub>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\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+ @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+ @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{@ {}l@ {}}
+ \raisebox{-20mm}{$\inferrule*{
+ \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
+ {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
+ \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
+ }
+ {@{term "{Q\<^isub>1} tcontra {Q\<^isub>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\<^isub>0"},
+ @{text "R\<^isub>1"}, \ldots{}, @{text "R\<^isub>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\<^isub>1 f\<^isub>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 are
+represented initially on the tape, then the machine either will never halt, or will
+halt 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.
+*}
+
+
+
+(*<*)
+end
+end
+(*>*)
\ No newline at end of file