tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:eb589fa73fc1
+:2e9881578cb2
 tcopy_init ("copy\<^bsub>begin\<^esub>") and
 tcopy_loop ("copy\<^bsub>loop\<^esub>") and
 tcopy_end ("copy\<^bsub>end\<^esub>") and
 step0 ("step") and
 steps0 ("steps") and
+exponent ("_\<^bsup>_\<^esup>") and
 (*  abc_lm_v ("lookup") and
 abc_lm_s ("set") and*)
 haltP ("stdhalt") and
 tcopy ("copy") and
 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and
 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 head and @{term r} for the tape on the right-hand side.  We use
-the convention that the head, abbreviated @{term hd}, of the
+the notation @{term "Bk \<up> n"} (similarly @{term "Oc \<up> n"}) for lists
-right-list is the cell on which the head of the Turing machine
+composed of @{term n} elements of @{term Bk}.  We also have the
-currently scannes. This can be pictured as follows:
+convention that the head, abbreviated @{term hd}, of the right-list
+is the cell on which the head of the Turing machine currently
+scannes. 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);
 \noindent
 We slightly deviate
 from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
 will become important when we formalise halting computations and also universal Turing
-machines. Given a tape and an action, we can define the
+machines.  Given a tape and an action, we can define the
 following tape updating function:
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{thm (lhs) update.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(1)}\\
 %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 follow the choice made in \cite{AspertiRicciotti12}
-representing a state by a natural number and the states in a Turing
+by representing a state with a natural number and the states in a Turing
 machine program by the initial segment of natural numbers starting from @{text 0}.
 In doing so we can compose two Turing machine programs by
 shifting the states of one by an appropriate amount to a higher
 segment and adjusting some ``next states'' in the other.
 An \emph{instruction} 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
+%
 \begin{equation}
 \begin{tikzpicture}
 \node [anchor=base] at (0,0) {@{thm dither_def}};
 \node [anchor=west] at (-1.5,-0.64)
 {$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm]
 \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};
 \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};
 \end{tikzpicture}
 \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 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};
 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
 Turing machine, we need to define a coding function for programs.
-This can be easily done for our programs-as-lists, but is more
+This can be directly done for our programs-as-lists, but is
-difficult for the functions used by Asperti and Ricciotti.
+slightly more difficult for the functions used by Asperti and Ricciotti.
 Given a program @{term p}, a state
 and the cell being read by the head, we need to fetch
 the corresponding instruction from the program. For this we define
 the function @{term fetch}
 \end{tabular}
 \end{center}
 \caption{Copy machine}\label{copy}
 \end{figure}
-{\it
+We often need to restrict tapes to be in \emph{standard form}, which means
-As in \cite{Boolos87} we often need to restrict tapes to be in standard
+the left list of the tape is either empty or only contains @{text "Bk"}s, and
-form.}
+the right list contains some ``clusters'' of @{text "Oc"}s separted by single
+blanks and can be followed by some blanks. To make this formal we define the
+following function
+\begin{center}
+foo
+\end{center}
+\noindent
+A standard tape is then of the form @{text "(Bk\<^isup>k,\<langle>n\<^isub>1,...,n\<^isub>m\<rangle> @ Bk\<^isup>l)"} for some @{text k},
+@{text l} and @{text "n\<^isub>i"}. Note that the head in a standard tape ``points'' to the
+leftmost @{term "Oc"} on the tape.
 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
 ``doing what they are supposed to be doing''.  Such correctness proofs are usually left
 whose three components are given in Figure~\ref{copy}. To the prove
 correctness of these Turing machine programs, we introduce the
 notion of total correctness defined in terms of
 \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They realise the
 idea that a program @{term p} started in state @{term "1::nat"} with
-a tape satisfying @{term P} will after @{text n} steps halt (have
+a tape satisfying @{term P} will after some @{text n} steps halt (have
 transitioned into the halting state) with a tape satisfying @{term
 Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
 realising 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
 \end{tabular}
 \end{center}
 \noindent
 We have set up our Hoare-style reasoning so that we can deal explicitly
-with looping and total correctness, rather than have notions for partial
+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), we prefer our definitions because
 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"} and @{term "tcopy_end"}.
 \begin{center}
-\begin{tabular}{lcl}
+\begin{tabular}{l@ {\hspace{3mm}}lcl}
-\multicolumn{1}{c}{start tape}\\
+& \multicolumn{1}{c}{start tape}\\[1mm]
+\raisebox{2.5mm}{halting case:} &
 \begin{tikzpicture}
 \draw[very thick] (-2,0)   -- ( 0.75,0);
 \draw[very thick] (-2,0.5) -- ( 0.75,0.5);
 \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
 \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
 \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);
 \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);
 \node [anchor=base] at (-1.7,0.2) {\ldots};
 \end{tikzpicture}\\
-\begin{tikzpicture}
+\raisebox{2.5mm}{non-halting case:} &
+\begin{tikzpicture}
 \draw[very thick] (-2,0)   -- ( 0.25,0);
 \draw[very thick] (-2,0.5) -- ( 0.25,0.5);
 \draw[very thick] (-0.25,0)   -- (-0.25,0.5);
 \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);
 \draw[very thick] (-0.75,0)   -- (-0.75,0.5);

changeset 81	2e9881578cb2
parent 80	eb589fa73fc1
child 84	4c8325c64dab