tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:b388dceee892
+:816e84ca16d6
 begin
 (*
 hide_const (open) s
 *)
+hide_const (open) Divides.adjust
 abbreviation
 "update2 p a \<equiv> update a p"
 consts DUMMY::'a
 declare [[show_question_marks = false]]
 (*>*)
 section {* Introduction *}
 text {*
 %\noindent
 %We formalised in earlier work the correctness proofs for two
 %algorithms in Isabelle/HOL---one about type-checking in
 %formalise in Isabelle/HOL computability arguments about the
 %algorithms.
 \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
 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
 %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 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
 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 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
 general fiddliness,\\ Turing machines are an even more
 daunting prospect.''
 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'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
 the more complicated case when we translate abacus programs into
 Turing programs.  This aspect of reasoning about computability theory
 \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
+operate on tapes that contain only \emph{blank} or \emph{occupied} cells.
-(represented by @{term Bk} and @{term Oc}, respectively, in our
+Traditionally the content of a cell can be any
-formalisation). 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
 *}
 section {* Turing Machines *}
 text {* \noindent
-Turing machines can be thought of as having a read-write-unit, also
+Turing machines can be thought of as having a \emph{head},
-referred to as \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 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 operates. This can
 be pictured as follows:
+%
 \begin{center}
 \begin{tikzpicture}
 \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);
 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}{rcl@ {\hspace{5mm}}l}
+\begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}
-@{text "a"} & $::=$  & @{term "W0"} & write blank (@{term Bk})\\
+@{text "a"} & $::=$  & @{term "W0"} & (write blank, @{term Bk})\\
-& $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
+& $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\
-& $\mid$ & @{term L} & move left\\
+\end{tabular}
-& $\mid$ & @{term R} & move right\\
+\begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
-& $\mid$ & @{term Nop} & do-nothing operation\\
+& $\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
 \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 in
+list, one has to know that the tail function, @{term tl}, is defined
-Isabelle/HOL
 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
 %head is currently positioned. Asperti and Ricciotti
 %\cite{AspertiRicciotti12} also considered such a representation, but
 %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
+Next we need to define the \emph{states} of a Turing machine.
-how little is usually said about how to represent them in informal
+%Given
-presentations, it might be surprising that in a theorem prover we
+%how little is usually said about how to represent them in informal
-have to select carefully a representation. If we use the naive
+%presentations, it might be surprising that in a theorem prover we
-representation where a Turing machine consists of a finite set of
+%have to select carefully a representation. If we use the naive
-states, then we will have difficulties composing two Turing
+%representation where a Turing machine consists of a finite set of
-machines: we would need to combine two finite sets of states,
+%states, then we will have difficulties composing two Turing
-possibly renaming states apart whenever both machines share
+%machines: we would need to combine two finite sets of states,
-states.\footnote{The usual disjoint union operation in Isabelle/HOL
+%possibly renaming states apart whenever both machines share
-cannot be used as it does not preserve types.} This renaming can be
+%states.\footnote{The usual disjoint union operation in Isabelle/HOL
-quite cumbersome to reason about. Therefore we made the choice of
+%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
+machine by the initial segment of natural numbers starting from @{text 0}.
-numbers starting from @{text 0} up to the number of states of the
+In doing so we can compose two Turing machine by
-machine. 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
 machine is then a list of such pairs. Using as an example the following Turing machine
 program, which consists of four instructions
 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 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
 \cite{AspertiRicciotti12}, we have chosen a very concrete
 representation for programs, because when constructing a universal
 \begin{center}
 \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}
 \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). 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
 the following three properties:
 \noindent
 The first says that @{text p} must have at least an instruction for the starting
 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
 state, and the third that every next-state is one of the states mentioned in
 the program or being the @{text 0}-state.
+}
 A \emph{configuration} @{term c} of a Turing machine is a state together with
 a tape. This is written as @{text "(s, (l, r))"}. If we have a
 configuration and a program, we can calculate
 what the next configuration is by fetching the appropriate action and next state
 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 (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
-\hspace{4mm}@{thm (rhs) shift.simps}\\
+@{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.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"}\\
 \end{tabular}
 \end{center}
 \noindent
 The first adds @{text n} to all states, exept the @{text 0}-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"}
 \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
 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

changeset 50	816e84ca16d6
parent 49	b388dceee892
child 52	2cb1e4499983