--- a/Paper.thy Thu Jan 10 13:13:27 2013 +0000
+++ b/Paper.thy Fri Jan 11 05:45:40 2013 +0000
@@ -192,16 +192,17 @@
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}
@@ -252,7 +253,7 @@
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}
@@ -268,11 +269,12 @@
\noindent
The first two clauses replace the head of the right-list
- with new a @{term Bk} or @{term Oc}, repsectively. To see that
- these tow clauses make sense in case where @{text r} is the empty
- list, one has to know that the tail function, @{term tl}, is defined
+ with a new @{term Bk} or @{term Oc}, repsectively. To see that
+ 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 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
@@ -281,25 +283,25 @@
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
- unit is on the left edge, respectively right edge, and in the middle
+ of tapes: one where the tape is empty; another where the head
+ 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
- cover uniformely all cases including the corner cases.
+ definition above, and by using the @{term update} function
+ 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
@@ -311,20 +313,37 @@
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
- natural number (the next state) and an action. A \emph{program} @{term p} of a Turing
- machine is then a list of such pairs. We have organised our programs
- such that
+ An \emph{instruction} @{term i} 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 the following Turing machine
+ program (consisting of four instructions) as an example
\begin{center}
- XXX
+ \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.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}
@@ -342,11 +361,7 @@
\end{tabular}
\end{center}
- start state 1 final state 0
-
- \begin{center}
- @{thm dither_def}
- \end{center}
+ \noindent
A \emph{configuration} @{term c} of a Turing machine is a state together with
@@ -356,14 +371,20 @@
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)}\\
- @{thm steps.simps(2)}\\
+ \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}
\emph{well-formedness} of a Turing program