(*<*)
theory Paper
imports "../thys/uncomputable"
begin
(*
hide_const (open) s
*)
hide_const (open) Divides.adjust
abbreviation
"update2 p a \<equiv> update a p"
consts DUMMY::'a
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
(*is_even ("iseven") and*)
tcopy_begin ("cbegin") and
tcopy_loop ("cloop") and
tcopy_end ("cend") and
step0 ("step") and
uncomputable.tcontra ("tcontra") and
steps0 ("steps") and
exponent ("_\<^bsup>_\<^esup>") and
haltP ("halts") and
tcopy ("copy") and
tape_of ("\<langle>_\<rangle>") and
tm_comp ("_ \<oplus> _") 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>")
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 \<Longrightarrow> inv_begin0 n \<mapsto> inv_loop1 n"
unfolding 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]]
(* THEOREMS *)
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" ("_")
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
(*>*)
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.
\noindent
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 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 @{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.
%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.
The only satisfying way out of this problem in a theorem prover based
on classical logic is to formalise a theory of computability. Norrish
provided such a formalisation for 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 can be completely \emph{unstructured}, behaving similar to
Basic programs involving 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 excerise to the
reader---a 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 as a recursive function.
\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. 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
scannes. 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})\\
\end{tabular}
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
& $\mid$ & @{term L} & (move left)\\
& $\mid$ & @{term R} & (move right)\\
\end{tabular}
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}
& $\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 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 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. Unlike Asperti and Riccioti
\cite{AspertiRicciotti12}, we have chosen a very concrete
representation for 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 read 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" and off="0::nat", simplified, 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.
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, exept 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.
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}. It is impossible in
Isabelle/HOL to lift the @{term step}-function in order to realise a
general evaluation function for Turing machines programs. The reason
is that functions in HOL-based provers need to be terminating, and
clearly there are programs that are not. We can however define a
recursive 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 \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.
\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), (W1, 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}
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 separted 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{center}
\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}
\end{center}
\noindent
A \emph{standard tape} is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l}
and @{text "n\<^isub>i"}. 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.
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
{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 \<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 "(l, r)"}.\\
\hspace{7mm}if @{term "P (l, r)"} holds then\\
\hspace{7mm}@{text "\<exists>"} @{term n}. such that\\
\hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\
\hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"}
\end{tabular} &
\begin{tabular}[t]{@ {}l@ {}}
\colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
\hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\
\hspace{7mm}if @{term "P (l, r)"} holds then\\
\hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) 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 "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
@{term "P' tp"} implies @{term "P tp"}.
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-terminantion, 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 realatively 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 @{text 0} 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 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 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 (or encoded number) 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))"}: @{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 meansure, @{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 left-most Hoare-triple 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 resoning is needed 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 "inv_begin0
n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
n"}, we can derive using our Hoare-rules 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)>)"}}.
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 containging a single (encoded)
number is defined as
\begin{center}
@{thm haltP_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 and @{text 1} for looping). Given our correctness
proofs for @{term dither} and @{term tcopy} shown above, this
non-existence is 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 when
started with the input tape containing @{term "<ns>"}. This
assumption is formalised as follows---for all @{term M} and 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}
@{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
\end{center}
\noindent
Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"}
Proof
\begin{center}
$\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 {P\<^isub>3}"}
}
{@{term "{P\<^isub>1} tcontra {P\<^isub>3}"}}
$
\end{center}
\begin{center}
$\inferrule*{
\inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {Q\<^isub>3}"}}
{@{term "{P\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
\\ @{term "{Q\<^isub>3} dither \<up>"}
}
{@{term "{P\<^isub>1} tcontra \<up>"}}
$
\end{center}
Magnus: invariants -- Section 5.4.5 on page 75.
*}
section {* Abacus Machines *}
text {*
\noindent
Boolos et al \cite{Boolos87} use abacus machines as a
stepping stone for making it less laborious to write
programs for Turing machines. Abacus machines operate
over an unlimited number of registers $R_0$, $R_1$, \ldots
each being able to hold an arbitrary large natural number.
We use natural numbers to refer to registers, but also
to refer to \emph{opcodes} of abacus
machines. Obcodes are given by the datatype
\begin{center}
\begin{tabular}{rcll}
@{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\
& $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
& & & then decrement it by one\\
& & & otherwise jump to opcode $o$\\
& $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$
\end{tabular}
\end{center}
\noindent
A \emph{program} of an abacus machine is a list of such
obcodes. For example the program clearing the register
$R$ (setting it to 0) can be defined as follows:
\begin{center}
%@ {thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
\end{center}
\noindent
The second opcode @{term "Goto 0"} in this program means we
jump back to the first opcode, namely @{text "Dec R o"}.
The \emph{memory} $m$ of an abacus machine holding the values
of the registers is represented as a list of natural numbers.
We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
which looks up the content of register $R$; if $R$
is not in this list, then we return 0. Similarly we
have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which
sets the value of $R$ to $n$, and if $R$ was not yet in $m$
it pads it approriately with 0s.
Abacus machine halts when it jumps out of range.
*}
section {* Recursive Functions *}
section {* Wang Tiles\label{Wang} *}
text {*
Used in texture mapings - graphics
*}
section {* Related Work *}
text {*
The most closely related work is by Norrish \cite{Norrish11}, and Asperti and
Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on
lambda-terms. For this he introduced a clever rewriting technology
based on combinators and de-Bruijn indices for
rewriting modulo $\beta$-equivalence (to keep it manageable)
Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program
@{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"}
\begin{center}
\begin{tabular}{l}
@{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
\hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
\end{tabular}
\end{center}
\noindent
where @{text 1} stands for the starting state and @{text 0} for our final state.
A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
\begin{center}
@{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
\<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
\end{center}
\noindent
Later on we need to consider specific Turing machines that
start with a tape in standard form and halt the computation
in standard form. To define a tape in standard form, it is
useful to have an operation %@{ term "tape_of_nat_list DUMMY"}
that translates lists of natural numbers into tapes.
\begin{center}
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
%@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
%@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
%@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
\end{tabular}
\end{center}
By this we mean
\begin{center}
%@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
\end{center}
\noindent
This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
and the head pointing to the first one; the Turing machine
halts with a tape consisting of some @{term Bk}s, followed by a
``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
The head in the output is pointing again at the first @{term Oc}.
The intuitive meaning of this definition is to start the Turing machine with a
tape corresponding to a value @{term n} and producing
a new tape corresponding to the value @{term l} (the number of @{term Oc}s
clustered on the output tape).
*}
(*
Questions:
Can this be done: Ackerman function is not primitive
recursive (Nora Szasz)
Tape is represented as two lists (finite - usually infinite tape)?
*)
(*<*)
end
(*>*)