(*<*)
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\<^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_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\<^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 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\<^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 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
(*>*)