tm: comparison Paper.thy

equal deleted inserted replaced

-:1569a56bd81b
+:ba789a0768a2
 *}
 section {* Turing Machines *}
 text {* \noindent
-Turing machines can be thought of as having a read-write-unit
+Turing machines can be thought of as having a read-write-unit, also
+referred to as \emph{head},
 ``gliding'' over a potentially infinite tape. Boolos et
 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
-read-write-unit 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 have the
 convention that the head, written @{term hd}, of the right-list is
-the cell on which the read-write-unit currently operates. This can
+the cell on which the head of the Turing machine currently operates. This can
 be pictured as follows:
 \begin{center}
 \begin{tikzpicture}
 \draw[very thick] (-3.0,0)   -- ( 3.0,0);
 \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 universal Turing
 machines later. Given a tape and an action, we can define the
-following updating function:
+following tape updating function:
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{thm (lhs) new_tape_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(1)}\\
 @{thm (lhs) new_tape_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(2)}\\
 \end{tabular}
 \end{center}
 \noindent
 The first two clauses replace the head of the right-list
-with new a @{term Bk} or @{term Oc}, repsectively. To see that
+with a new @{term Bk} or @{term Oc}, repsectively. To see that
-these tow clauses make sense in case where @{text r} is the empty
+these two clauses make sense in case where @{text r} is the empty
-list, one has to know that the tail function, @{term tl}, is defined
+list, one has to know that the tail function, @{term tl}, is in
+Isabelle/HOL defined
 such that @{term "tl [] == []"} holds. The third clause
-implements the move of the read-write unit one step to the left: we need
+implements the move of the head one step to the left: we need
 to test if the left-list @{term l} is empty; if yes, then we just prepend a
 blank cell to the right-list; otherwise we have to remove the
 head from the left-list and prepend it to the right-list. Similarly
 in the clause for a right move action. The @{term Nop} operation
 leaves the the tape unchanged.
 Note that our treatment of the tape is rather ``unsymmetric''---we
 have the convention that the head of the right-list is where the
-read-write unit is currently positioned. Asperti and Ricciotti
+head is currently positioned. Asperti and Ricciotti
 \cite{AspertiRicciotti12} also consider such a representation, but
 dismiss it as it complicates their definition for \emph{tape
-equality}. The reason is that moving the read-write unit one step to
+equality}. The reason is that moving the head one step to
 the left and then back to the right might change the tape (in case
 of going over the ``edge''). Therefore they distinguish four types
-of tapes: one where the tape is empty; another where the read-write
+of tapes: one where the tape is empty; another where the head
-unit is on the left edge, respectively right edge, and in the middle
+is on the left edge, respectively right edge, and in the middle
 of the tape. The reading, writing and moving of the tape is then
 defined in terms of these four cases.  In this way they can keep the
 tape in a ``normalised'' form, and thus making a left-move followed
 by a right-move being the identity on tapes. Since we are not using
 the notion of tape equality, we can get away with the unsymmetric
-definition above and by using the @{term update} function
+definition above, and by using the @{term update} function
-cover uniformely all cases including the corner cases.
+cover uniformely all cases including corner cases.
 Next we need to define the \emph{states} of a Turing machine.  Given
 how little is usually said about how to represent them in informal
-presentaions, it might be surprising that in a theorem prover we have
+presentations, it might be surprising that in a theorem prover we have
 to select carfully a representation. If we use the naive representation
 where a Turing machine consists of a finite set of states, then we
 will have difficulties composing two Turing machines. In this case we
 would need to combine two finite sets of states, possibly requiring
 renaming states apart whenever both machines share states. This
 the choice of representing a state by a natural number and the states
 of a Turing machine will always consist of the initial segment
 of natural numbers starting from @{text 0} up to number of states
 of the machine minus @{text 1}. In doing so we can compose
 two Turing machine by ``shifting'' the states of one by an appropriate
-amount to a higher segment.
+amount to a higher segment and adjust some ``next states''.
-An \emph{instruction} @{term i} of a Turing machine is a pair consisting of a
+An \emph{instruction} @{term i} of a Turing machine is a pair consisting of
-natural number (the next state) and an action. A \emph{program} @{term p} of a Turing
+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. We have organised our programs
+machine is then a list of such pairs. Using the following Turing machine
-such that
+program (consisting of four instructions) as an example
 \begin{center}
-XXX
+\begin{tikzpicture}
-\end{center}
+\node [anchor=base] at (0,0) {@{thm dither_def}};
+\node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};
-\noindent
+\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}
+\end{center}
+\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 segment determines what action should be taken and which next
+state should be transitioned to in case the head read 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.
+The 0-state is special in that it will be used as \emph{halting state}.
+There are no instructions for the 0-state, but it will always
+perform a @{term Nop}-operation and remain in the 0-state.
 Given a program @{term p}, a state
-and the cell being read by the read-write unit, we need to fetch
+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}
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\
 \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}
 \end{tabular}
 \end{center}
-start state 1 final state 0
+\noindent
-\begin{center}
-@{thm dither_def}
-\end{center}
 A \emph{configuration} @{term c} of a Turing machine is a state together with
 a tape. This is written as the triple @{term "(s, l, r)"}. If we have a
 configuration and a program, we can calculate
 what the next configuration is by fetching the appropriate next state
 and action from the program. Such a single step of execution can be defined as
 \begin{center}
-@{thm tstep_def2(1)}\\
+\begin{tabular}{l}
+@{thm (lhs) tstep_def2(1)} @{text "\<equiv>"}\\
+\hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\
+\hspace{10mm}@{text "in (s', update (l, r) a)"}
+\end{tabular}
 \end{center}
 No evaluator in HOL, because of totality.
 \begin{center}
-@{thm steps.simps(1)}\\
+\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-@{thm steps.simps(2)}\\
+@{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}
 \emph{well-formedness} of a Turing program
 programs halts

changeset 30	ba789a0768a2
parent 29	1569a56bd81b
child 31	4ef4b25e2997