tm: comparison Paper/Paper.thy

equal deleted inserted replaced

-:49f8e5cf82c5
+:a673539f2f75
 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
 update2 ("update") and
 tm_wf0 ("wf") and
 is_even ("iseven") and
+tcopy_init ("copy\<^bsub>begin\<^esub>") and
+tcopy_loop ("copy\<^bsub>loop\<^esub>") and
+tcopy_end ("copy\<^bsub>end\<^esub>") and
 (*  abc_lm_v ("lookup") and
 abc_lm_s ("set") and*)
 haltP ("stdhalt") and
 tcopy ("copy") and
 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and
 \cite{AspertiRicciotti12}. They describe a complete formalisation of
 Turing machines in the Matita theorem prover, including a universal
 Turing machine. They report that the informal proofs from which they
 started are \emph{not} ``sufficiently accurate to be directly usable as a
 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
-our formalisation we followed mainly the proofs from the textbook
+our formalisation we follow mainly the proofs from the textbook
 \cite{Boolos87} and found that the description there is quite
 detailed. Some details are left out however: for example, it is only
 shown how the universal Turing machine is constructed for Turing
 machines computing unary functions. We had to figure out a way to
 generalise this result to $n$-ary functions. Similarly, when compiling
 %machines: we would need to combine two finite sets of states,
 %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 followed the choice made in \cite{AspertiRicciotti12}
+We follow the choice made in \cite{AspertiRicciotti12}
 representing a state by a natural number and the states in a Turing
-machine programme by the initial segment of natural numbers starting from @{text 0}.
+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
 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.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};
+\node [anchor=west] at (-1.5,-0.64)
+{$\underbrace{\hspace{21mm}}_{\text{\begin{tabular}{@ {}l@ {}}1st state\\[-2mm]
+= starting state\end{tabular}}}$};
 \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};
 \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}
 %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
 %an initial segment of the natural numbers.
 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 is \emph{final} if @{term "s = (0::nat)"} and 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
 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
 @{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}
-\noindent
+\noindent Recall our definition of @{term fetch} (shown in
-Recall our definition of @{term fetch} (shown in \ref{fetch}) with the default value for
+\eqref{fetch}) with the default value for the @{text 0}-state. In
-the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less
+case a Turing program takes according to the usual textbook
-then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation
+definition \cite{Boolos87} less than @{text n} steps before it
-does not actually halt, but rather transitions to the @{text 0}-state and
+halts, then in our setting the @{term steps}-evaluation does not
-remains there performing @{text Nop}-actions until @{text n} is reached.
+actually halt, but rather transitions to the @{text 0}-state (the
+final state) and remains there performing @{text Nop}-actions until
-Before we can prove the undecidability of the halting problem for Turing machines,
+@{text n} is reached.
-we need to analyse two concrete Turing machine programs and establish that
-they ``doing what they are supposed to be doing''. To do so we will derive
+\begin{figure}[t]
-some Hoare-style reasoning rules for Turing machine programs. A \emph{Hoare-triple}
+\begin{center}
-for a terminating Turing machine program is defined as
+\begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
+@{thm (lhs) tcopy_init_def} @{text "\<equiv>"} &
+@{thm (lhs) tcopy_loop_def} @{text "\<equiv>"} &
+@{thm (lhs) tcopy_end_def} @{text "\<equiv>"}\\
+@{thm (rhs) tcopy_init_def} &
+@{thm (rhs) tcopy_loop_def} &
+@{thm (rhs) tcopy_end_def}
+\end{tabular}
+\end{center}
+\caption{Copy machine}\label{copy}
+\end{figure}
+Before we can prove the undecidability of the halting problem for
+Turing machines, we need to analyse two concrete Turing machine
+programs and establish that they are correct, that is they are
+``doing what they are supposed to be doing''.  This is usually left
+out in the informal computability literature, for example
+\cite{Boolos87}.  One program we prove correct is the @{term dither}
+program shown in \eqref{dither} and the other program @{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 the correctness, we derive some Hoare-style reasoning rules for
+Turing machine programs. A \emph{Hoare-triple} for a terminating Turing
+machine program is defined as
 \begin{center}
 @{thm Hoare_halt_def}
 \end{center}
 \end{center}
 In the following we will consider the following Turing machine program
 that makes a copies a value on the tape.
-\begin{figure}
-\begin{center}
-\begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
-@{thm tcopy_init_def} &
-@{thm tcopy_loop_def} &
-@{thm tcopy_end_def}
-\end{tabular}
-\end{center}
-\end{figure}
-\begin{center}
-\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
-@{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
-\end{tabular}
-\end{center}
 assertion holds for all tapes
 Hoare rule for composition
 \begin{center}
 %@ {thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
 \end{center}
 \noindent
-The second opcode @{term "Goto 0"} in this programm means we
+The second opcode @{term "Goto 0"} in this program means we
 jump back to the first opcode, namely @{text "Dec R o"}.
 The \emph{memory} $m$ of an abacus machine holding the values
 of the registers is represented as a list of natural numbers.
 We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
 which looks up the content of register $R$; if $R$

changeset 73	a673539f2f75
parent 72	49f8e5cf82c5
child 75	97eaf7514988