--- a/Paper/Paper.thy Fri Jan 18 13:03:09 2013 +0000
+++ b/Paper/Paper.thy Fri Jan 18 13:56:35 2013 +0000
@@ -7,6 +7,9 @@
hide_const (open) s
*)
+
+hide_const (open) Divides.adjust
+
abbreviation
"update2 p a \<equiv> update a p"
@@ -31,6 +34,8 @@
section {* Introduction *}
+
+
text {*
%\noindent
@@ -46,7 +51,7 @@
\noindent
-Suppose you want to mechanise a proof whether a predicate @{term P}, say, is
+Suppose you want to mechanise a proof about 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
@@ -61,7 +66,7 @@
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 the HOL4 theorem prover. He choose
+provided such a formalisation for the HOL4. He choose
the $\lambda$-calculus as the starting point for his formalisation of
computability theory, because of its ``simplicity'' \cite[Page
297]{Norrish11}. Part of his formalisation is a clever infrastructure
@@ -71,7 +76,7 @@
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 in the context of theorem provers \cite[Page 310]{Norrish11}:
+however that \cite[Page 310]{Norrish11}:
\begin{quote}
\it``If register machines are unappealing because of their
@@ -85,7 +90,7 @@
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's infamous goto. This precludes in the
+similar to Basic's 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 is possible to
reason in a compositional manner (which is fortunately quite often), but also tackle
@@ -152,9 +157,8 @@
\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
-(represented by @{term Bk} and @{term Oc}, respectively, in our
-formalisation). Traditionally the content of a cell can be any
+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
@@ -186,8 +190,7 @@
section {* Turing Machines *}
text {* \noindent
- Turing machines can be thought of as having a read-write-unit, also
- referred to as \emph{head},
+ 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
@@ -198,7 +201,7 @@
convention that the head, abbreviated @{term hd}, of the right-list is
the cell on which the head of the Turing machine currently operates. This can
be pictured as follows:
-
+ %
\begin{center}
\begin{tikzpicture}
\draw[very thick] (-3.0,0) -- ( 3.0,0);
@@ -233,12 +236,16 @@
the Turing machine can perform:
\begin{center}
- \begin{tabular}{rcl@ {\hspace{5mm}}l}
- @{text "a"} & $::=$ & @{term "W0"} & write blank (@{term Bk})\\
- & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
- & $\mid$ & @{term L} & move left\\
- & $\mid$ & @{term R} & move right\\
- & $\mid$ & @{term Nop} & do-nothing operation\\
+ \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}
@@ -263,15 +270,14 @@
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 in
- Isabelle/HOL
+ 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 (last clause).
+ 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
@@ -291,23 +297,24 @@
%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. Therefore we made the choice of
+ 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 followed the choice made by \cite{AspertiRicciotti12}
representing a state by a natural number and the states of a Turing
- machine will always consist of the initial segment of natural
- numbers starting from @{text 0} up to the number of states of the
- machine. In doing so we can compose two Turing machine by
+ machine by the initial segment of natural numbers starting from @{text 0}.
+ In doing so we can compose two Turing machine by
shifting the states of one by an appropriate amount to a higher
- segment and adjusting some ``next states'' in the other.
+ segment and adjusting some ``next states'' in the other. {\it composition here?}
An \emph{instruction} @{term i} 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
@@ -333,7 +340,7 @@
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 zeroth state is special in that it will be used as the
+ 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
@@ -352,9 +359,9 @@
\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{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\
+ \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{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
+ \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
\end{tabular}
\end{center}
@@ -365,7 +372,7 @@
(@{term None}-case). In doing so we slightly deviate from the description
in \cite{Boolos87}: if their Turing machines transition to a non-existing
state, then the computation is halted. We will transition in such cases
- to the @{text 0}-state. However, with introducing the
+ to the @{text 0}-state.\footnote{\it However, with introducing the
notion of \emph{well-formed} Turing machine programs we will later exclude such
cases and make the @{text 0}-state the only ``halting state''. A program
@{term p} is said to be well-formed if it satisfies
@@ -384,6 +391,7 @@
state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
state, and the third that every next-state is one of the states mentioned in
the program or being the @{text 0}-state.
+ }
A \emph{configuration} @{term c} of a Turing machine is a state together with
a tape. This is written as @{text "(s, (l, r))"}. If we have a
@@ -485,11 +493,8 @@
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
- @{thm (lhs) shift.simps} @{text "\<equiv>"}\\
- \hspace{4mm}@{thm (rhs) shift.simps}\\
- @{thm (lhs) adjust.simps} @{text "\<equiv>"}\\
- \hspace{4mm}@{text "map (\<lambda> (a, s)."}\\
- \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\
+ @{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
+ @{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
\end{tabular}
\end{center}
@@ -503,7 +508,7 @@
of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}
\begin{center}
- @{thm tm_comp.simps[THEN eq_reflection]}
+ @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
\end{center}
\noindent