(*<*)
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
(*>*)