tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:294576baaeed
+:01f688735b9b
 \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
+formalisation we follow mainly the proofs from the textbook by Boolos
-\cite{Boolos87} and found that the description there is quite
+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} and its correctness proof are left as
+the \emph{copy Turing machine} is left as an excerise to the
-an excerise to the reader; also \cite{Boolos87} only shows how the
+reader---a correctness proof is not mentioned at all; also \cite{Boolos87}
-universal Turing machine is constructed for Turing machines computing
+only shows how the universal Turing machine is constructed for Turing
-unary functions. We had to figure out a way to generalise this result
+machines computing unary functions. We had to figure out a way to
-to $n$-ary functions. Similarly, when compiling recursive functions to
+generalise this result to $n$-ary functions. Similarly, when compiling
-abacus machines, the textbook again only shows how it can be done for
+recursive functions to abacus machines, the textbook again only shows
-2- and 3-ary functions, but in the formalisation we need arbitrary
+how it can be done for 2- and 3-ary functions, but in the
-functions. But the general ideas for how to do this are clear enough
+formalisation we need arbitrary functions. But the general ideas for
-in \cite{Boolos87}.
+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.
 & & @{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
+where @{term "read r"} returns the head of the list @{text r}, or if
-empty it returns @{term Bk}.
+@{text r} is empty it returns @{term Bk}.  It is impossible in
-It is impossible in Isabelle/HOL to lift the @{term step}-function to realise
+Isabelle/HOL to lift the @{term step}-function in order to realise a
-a general evaluation function for Turing machines. The reason is that functions in HOL-based
+general evaluation function for Turing machines programs. The reason
-provers need to be terminating, and clearly there are Turing machine
+is that functions in HOL-based provers need to be terminating, and
-programs that are not. We can however define an evaluation
+clearly there are programs that are not. We can however define a
-function that performs exactly @{text n} steps:
+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)}\\
 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 \emph{standard form}, which means
+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)}\\
 @{thm (lhs) nats2tape(3)} & @{text "\<equiv>"} & @{thm (rhs) nats2tape(3)}
 \end{tabular}
 \end{center}
 \noindent
-A standard tape is then of the form @{text "(Bk\<^isup>l,\<langle>[n\<^isub>1,...,n\<^isub>m]\<rangle>)"} for some @{text l}
+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
+Before we can prove the undecidability of the halting problem for
-Turing machines, we have to analyse two concrete Turing machine
+our Turing machines working on standard tapes, we have to analyse
-programs and establish that they are correct---that means they are
+two concrete Turing machine programs and establish that they are
-``doing what they are supposed to be doing''.  Such correctness proofs are usually left
+correct---that means they are ``doing what they are supposed to be
-out in the informal literature, for example \cite{Boolos87}.  The first program
+doing''.  Such correctness proofs are usually left out in the
-we need to prove correct is the @{term dither} program shown in \eqref{dither}
+informal literature, for example \cite{Boolos87}.  The first program
-and the second program is @{term "tcopy"} defined as
+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}
 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 \emph{realisability} in \cite{AspertiRicciotti12}. We
+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{equation}
 @{thm[mode=Rule] Hoare_consequence}
 \end{equation}
+\noindent
-\noindent
+where
+@{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
+@{term "P' tp"} implies @{term "P tp"}.
 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),
 \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 "(DUMMY, <(n,
+its purpose is to produce the standard tape @{term "(Bks, <(n,
-n::nat)>)"} when started with @{term "(DUMMY, <(n::nat)>)"}, that is
+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.
 The 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. We will show the details for the program @{term
 "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots,
-@{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to
+@{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}
+\begin{figure}[t]
 \begin{center}
 \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
 @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
 &             & @{thm (rhs) inv_begin02} \\
 @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
 \end{tabular}
 \end{center}
 \noindent
 This invariant depends on @{term n} representing the number of
-@{term Oc}s on the tape. It is not hard (26 lines of automated proof
+@{term Oc}s (or encoded number) on the tape. It is not hard (26
-script) to show that for @{term "n > (0::nat)"} this invariant is
+lines of automated proof script) to show that for @{term "n >
-preserved under computation rules @{term step} and @{term steps}.
+(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 104	01f688735b9b
parent 103	294576baaeed
child 105	2cae8a39803e