tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:2669235c4b1e
+:bc54c5e648d7
 %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
+Suppose you want to mechanise a proof for whether a predicate @{term
-decidable or not. Decidability of @{text P} usually amounts to showing
+P}, say, is decidable or not. Decidability of @{text P} usually
-whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work
+amounts to showing whether \mbox{@{term "P \<or> \<not>P"}} holds. But this
-in Isabelle/HOL and other HOL theorem provers, since they are based on classical logic
+does \emph{not} work in Isabelle/HOL and other HOL theorem provers,
-where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
+since they are based on classical logic where the law of excluded
-is always provable no matter whether @{text P} is constructed by
+middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no
-computable means. We hit this limitation previously when we mechanised the correctness
+matter whether @{text P} is constructed by computable means. We hit on
-proofs of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12},
+this limitation previously when we mechanised the correctness proofs
-but were unable to formalise arguments about decidability.
+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.
 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.  These difficulties when reasoning about computability theory
+Turing programs.  This reasoning about Turing machine programs is
-are usually completely left out in the informal literature, e.g.~\cite{Boolos87}.
+usually completely 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,
 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
-relating recursive functions to abacus machines and abacus machines to
+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 formalising the undecidability proof of Wang's tiling problem. {\it citation}
 \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}, @{text a}
+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})\\
 \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 the
+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.
 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"}
+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}
 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 (l, r)"} holds.  If we have a configuration and a program, we can
+"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}
 \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 realising
+It is impossible in Isabelle/HOL to lift the @{term step}-function to realise
 a general evaluation function for Turing machines. The reason is that functions in HOL-based
 provers need to be terminating, and clearly there are Turing machine
 programs that are not. We can however define an evaluation
-function so that it performs exactly @{text n} steps:
+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}
 \caption{Copy machine}\label{copy}
 \end{figure}
-Before we can prove the undecidability of the halting problem for
+{\it tapes in standard form}
+Before we can prove the undecidability of the halting problem for our
 Turing machines, we need to analyse two concrete Turing machine
-programs and establish that they are correct, that means they are
+programs and establish that they are correct---that means they are
-``doing what they are supposed to be doing''.  This is usually left
+``doing what they are supposed to be doing''.  Such correctness proofs are usually left
 out in the informal literature, for example \cite{Boolos87}.  One program
 we need to prove correct is the @{term dither} program shown in \eqref{dither}
-and the other program @{term "tcopy"} is defined as
+and the other program is @{term "tcopy"} is defined as
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
 \end{tabular}
 \end{center}
 \noindent
-whose three components are given in Figure~\ref{copy}. To prove correctness,
+whose three components are given in Figure~\ref{copy}. To the prove
-we introduce the notion of total correctness defined in terms of
+correctness of these Turing machine programs, we introduce the
-\emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the idea
+notion of total correctness defined in terms of
-that a program @{term p} started in state @{term "1::nat"} with a tape
+\emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the
-satisfying @{term P} will after @{text n} steps halt (have transitioned into
+idea that a program @{term p} started in state @{term "1::nat"} with
-the halting state) with a tape satisfying @{term Q}. We also have
+a tape satisfying @{term P} will after @{text n} steps halt (have
-\emph{Hoare-pairs} of the form @{term "{P} p \<up>"} realising the case that a
+transitioned into the halting state) with a tape satisfying @{term
-program @{term p} started with a tape satisfying @{term P} will loop
+Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
-(never transition into the halting state). Both notion are formally
+realising the case that a program @{term p} started with a tape
-defined as
+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@ {}}
 @{thm (lhs) Hoare_halt_def} @{text "\<equiv>"}\\[1mm]
 \end{tabular}
 \end{tabular}
 \end{center}
 \noindent
-We have set up our Hoare-style reasoning to deal explicitly with
+We have set up our Hoare-style reasoning so that we can deal explicitly
-looping and total correctness, rather separate notions for partial
+with looping and total correctness, rather than have notions for partial
-correctness and termination, is because we can derive simple rules
+correctness and termination. Although the latter would allow us to reason
-for sequentially composed Turing programs. They allow us to reason
+more uniformly (only using Hoare-triples), we prefer our definitions because
-about correctness of components completely separately.
+we can derive simple Hoare-rules for sequentially composed Turing programs.
+In this way we can reason about the correctness of @{term "tcopy_init"},
+for example, completely separately from @{term "tcopy_loop"}.
 It is rather straightforward to prove that the Turing program
 @{term "dither"} satisfies the following correctness properties
 \begin{center}

changeset 79	bc54c5e648d7
parent 78	2669235c4b1e
child 80	eb589fa73fc1