(*<*)+ −
theory Paper+ −
imports "../thys/abacus"+ −
begin+ −
+ −
(*+ −
hide_const (open) s + −
*)+ −
+ −
+ −
hide_const (open) Divides.adjust+ −
+ −
abbreviation+ −
"update2 p a \<equiv> update a p"+ −
+ −
consts DUMMY::'a+ −
+ −
+ −
(* 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" ("_")+ −
+ −
+ −
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+ −
(*is_even ("iseven") 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+ −
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]]+ −
+ −
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 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.+ −
+ −
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, 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. + −
+ −
\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"} (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-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+ −
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 "inv_begin0+ −
n \<mapsto> 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 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 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 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"}. Given the invariants 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"}. Again given the invariants on the + −
left, we can derive the Hoare-triple for @{term tcontra} on the right.+ −
+ −
\begin{center}\small+ −
\begin{tabular}{@ {}c@ {\hspace{-17mm}}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 case we come+ −
to an contradiction, which means we have to abondon our assumption + −
that there exists a Turing machine @{term H} which can 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+ −
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{statements} of abacus programs. Statements + −
are given by the datatype+ −
+ −
\begin{center}+ −
\begin{tabular}{rcl@ {\hspace{10mm}}l}+ −
@{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 statement $o$\\+ −
& $\mid$ & @{term "Goto o\<iota>"} & jump to statement $o$+ −
\end{tabular}+ −
\end{center}+ −
+ −
\noindent+ −
A \emph{program} of an abacus machine is a list of such+ −
statements. 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).+ −
+ −
+ −
+ −
Magnus: invariants -- Section 5.4.5 on page 75.+ −
*}+ −
+ −
+ −
(*+ −
Questions:+ −
+ −
Can this be done: Ackerman function is not primitive + −
recursive (Nora Szasz)+ −
+ −
Tape is represented as two lists (finite - usually infinite tape)?+ −
+ −
*)+ −
+ −
+ −
(*<*)+ −
end+ −
end+ −
(*>*)+ −