tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:06db15939b7c
+:cdef5b1072fe
 Turing machines, 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 other program is @{term "tcopy"} defined as
+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}. We introduce
+whose three components are given in Figure~\ref{copy}. For our
-the notion of total correctness defined in terms of
+correctness proofs, we introduce the notion of total correctness
-\emph{Hoare-triples}, written @{term "{P} p {Q}"} (this notion is
+defined in terms of \emph{Hoare-triples}, written @{term "{P} p
-very similar to \emph{realisability} in \cite{AspertiRicciotti12}).
+{Q}"}.  They implement the idea that a program @{term
-The Hoare-triples implement the idea that a program @{term p}
+p} started in state @{term "1::nat"} with a tape satisfying @{term
-started in state @{term "1::nat"} with a tape satisfying @{term P}
+P} will after some @{text n} steps halt (have transitioned into the
-will after some @{text n} steps halt (have transitioned into the
+halting state) with a tape satisfying @{term Q}. This idea is very
-halting state) with a tape satisfying @{term Q}. We also have
+similar to \emph{realisability} in \cite{AspertiRicciotti12}. We
-\emph{Hoare-pairs} of the form @{term "{P} p \<up>"} implementing the
+also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
-case that a program @{term p} started with a tape satisfying @{term
+implementing the case that a program @{term p} started with a tape
-P} will loop (never transition into the halting state). Both notion
+satisfying @{term P} will loop (never transition into the halting
-are formally defined as
+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]
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
-For our Hoare-triples we can easily prove the following consequence rule
+For our Hoare-triples we can easily prove the following Hoare-consequence rule
 \begin{equation}
 @{thm[mode=Rule] Hoare_consequence}
 \end{equation}
 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 small Turing program
+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 loop when started with @{text 0} instead, as pictured
+@{text "1"} but loops when started with @{text 0} instead, as pictured
 below.
 \begin{center}
 \begin{tabular}{l@ {\hspace{3mm}}lcl}
 @{thm dither_loops}
 \end{tabular}
 \end{center}
 \noindent
-The first is by a simple calculation. The second is by induction on the
+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 "(DUMMY, <(n,
 n::nat)>)"} when started with @{term "(DUMMY, <(n::nat)>)"}, that is
 \end{tabular}
 \end{center}
 \noindent
 The first corresponds to the usual Hoare-rule for composition of two
-terminating programs. The second rule is for cases where the first program
+terminating programs. The second rule gives the conditions for when
-terminates generating a tape for which the second program loops.
+the first program terminates generating a tape for which the second
-The side-condition about @{thm (prem 3) HR2} is needed in both rules
+program loops.  The side-conditions about @{thm (prem 3) HR2} are
-in order to ensure that the redirection of the halting and initial
+needed in order to ensure that the redirection of the halting and
-state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
+initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
-The Hoare-rules above allow us to prove the correctness of @{term tcopy}
+The Hoare-rules allow us to prove the correctness of @{term
-by considering the correctness of the components @{term "tcopy_begin"}, @{term "tcopy_loop"}
+tcopy} by considering the correctness of the components @{term
-and @{term "tcopy_end"} in isolation. We will show the details for
+"tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in
-the program @{term "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, @{term "inv_begin4"}
+isolation. We will show the details for the program @{term
-shown in Figure~\ref{invbegin},
+"tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots,
-we define the following invariant for @{term "tcopy_begin"}.
+@{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to
+each state of @{term tcopy_begin}, we define the
+following invariant for the whole program:
 \begin{figure}
 \begin{center}
 \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
 @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
 & & @{text else} @{thm (rhs) inv_begin_print(6)}
 \end{tabular}
 \end{center}
 \noindent
-This definition depends on @{term n}, which represents the number
+This invariant depends on @{term n} representing the number of
-of @{term Oc}s on the tape. It is not hard (26 lines of automated proof script)
+@{term Oc}s on the tape. It is not hard (26 lines of automated proof
-to show that for @{term "n > (0::nat)"} this invariant is preserved under @{term step} and @{term steps}.
+script) to show that for @{term "n > (0::nat)"} this invariant is
+preserved under computation rules @{term step} and @{term steps}.
 measure for the copying TM, which we however omit.
 \begin{center}

changeset 102	cdef5b1072fe
parent 100	dfe852aacae6
child 103	294576baaeed