# HG changeset patch # User Christian Urban # Date 1357883140 0 # Node ID ba789a0768a2fa5b8a1438030948107816a4bfdc # Parent 1569a56bd81b037ad70011c4466fc0912ac7e247 update diff -r 1569a56bd81b -r ba789a0768a2 Paper.thy --- 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 "\"}\\ + \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 "\"} & @{thm (rhs) steps.simps(1)}\\ + @{thm (lhs) steps.simps(2)} & @{text "\"} & @{thm (rhs) steps.simps(2)}\\ + \end{tabular} \end{center} \emph{well-formedness} of a Turing program diff -r 1569a56bd81b -r ba789a0768a2 document/root.tex --- a/document/root.tex Thu Jan 10 13:13:27 2013 +0000 +++ b/document/root.tex Fri Jan 11 05:45:40 2013 +0000 @@ -3,6 +3,7 @@ \usepackage{isabellesym} \usepackage{times} \usepackage{amssymb} +\usepackage{amsmath} \usepackage{mathpartir} \usepackage{pdfsetup} \usepackage{tikz} diff -r 1569a56bd81b -r ba789a0768a2 paper.pdf Binary file paper.pdf has changed