tm: comparison Paper.thy

equal deleted inserted replaced

-:2557d2946354
+:284468a61346
 general fiddliness, Turing machines are an even more
 daunting prospect.''
 \end{quote}
 \noindent
-In this paper we took on this daunting prospect and provide a
+In this paper we take on this daunting prospect and provide a
 formalisation of Turing machines, as well as abacus machines (a kind
 of register machines) and recursive functions. To see the difficulties
 involved with this work, one has to understand that interactive
 theorem provers, like Isabelle/HOL, are at their best when the
 data-structures at hand are ``structurally'' defined, like lists,
 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
-convention that the head, written @{term hd}, of the right-list is
+convention that the head, abbreviated @{term hd}, of the right-list is
 the cell on which the head of the Turing machine currently operates. This can
 be pictured as follows:
 \begin{center}
 \begin{tikzpicture}
 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
 head is currently positioned. Asperti and Ricciotti
-\cite{AspertiRicciotti12} also consider such a representation, but
+\cite{AspertiRicciotti12} also considered such a representation, but
 dismiss it as it complicates their definition for \emph{tape
 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 head
 renaming states apart whenever both machines share
 states.\footnote{The usual disjoint union operation does not preserve types, unfortunately.} This
 renaming can be quite cumbersome to reason about. Therefore we made
 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 natural numbers starting from @{text 0} up to the number of states
 of the machine. In doing so we can compose
 two Turing machine by ``shifting'' the states of one by an appropriate
-amount to a higher segment and adjust some ``next states''.
+amount to a higher segment and adjust some ``next states'' in the other.
 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
 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 the \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.
-A \emph{well-formed} Turing machine program @{term p} is one that satisfies
-the following three properties
-\begin{center}
-\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-@{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
-& @{text "\<and>"} & @{term "iseven (length p)"}\\
-& @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
-\end{tabular}
-\end{center}
-\noindent
-The first says that @{text p} must have at least an instruction for the starting
-state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
-state, and the third that every next-state is one of the states mentioned in
-the program or being the 0-state.
 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}
 from a list, if it exists (@{term Some}-case), or if it does not, it
 returns the default action @{term Nop} and the default state 0
 (@{term None}-case). In doing so we slightly deviate from the description
 in \cite{Boolos87}: if their Turing machines transition to a non-existing
 state, then the computation is halted. We will transition in such cases
-to the 0th state with the @{term Nop}-action.
+to the 0th state with the @{term Nop}-action. However, with introducing the
+notion of \emph{well-formed} Turing machine programs we will exclude such
+cases. A program @{term p} is said to be well-formed if it satisfies
+the following three properties
+\begin{center}
+\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+@{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
+& @{text "\<and>"} & @{term "iseven (length p)"}\\
+& @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
+\end{tabular}
+\end{center}
+\noindent
+The first says that @{text p} must have at least an instruction for the starting
+state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
+state, and the third that every next-state is one of the states mentioned in
+the program or being the 0-state.
 A \emph{configuration} @{term c} of a Turing machine is a state together with
 a tape. This is written as @{text "(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
 \hspace{10mm}@{text "in (s', update (l, r) a)"}
 \end{tabular}
 \end{center}
 \noindent
-It is impossible in Isabelle/HOL to lift this function in order to realise
+It is impossible in Isabelle/HOL to lift this function realising
 a general evaluation function for Turing machines. The reason is that functions in HOL-based
 provers need to be terminating, and clearly there are Turing machine
-programs for which this does not hold. We can however define an evaluation
+programs which are not. We can however define an evaluation
-function so that it performs exactly @{text n}:
+function so that it performs exactly @{text n} steps:
 \begin{center}
 \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)}\\
 @{term p} halts generating an output tape @{text "(l\<^isub>o,r\<^isub>o)"}:
 \begin{center}
 \begin{tabular}{l}
 @{term "halt p (l\<^isub>i,r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
-\hspace{6mm}@{text "\<exists> n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n= (0, (l\<^isub>o,r\<^isub>o))"}
+\hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
 \end{tabular}
 \end{center}
 \noindent
+where 1 stands for the starting state and 0 for the halting state, or
+in our settin it should better be called the final state.
 Later on we need to consider specific Turing machines that
 start with a tape in standard form and halt the computation
 in standard form. By this we mean
 \begin{center}
 @{thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
 \end{center}
 \noindent
-the Turing machine starts with a tape containg @{text n} @{term Oc}s
+This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
 and the head pointing to the first one; the Turing machine
 halts with a tape consisting of some @{term Bk}s, followed by a
 ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
-The head in the output is at the first @{term Oc}.
+The head in the output is pointing again at the first @{term Oc}.
-The intuitive meaning of this definition is to start Turing machine with a
+The intuitive meaning of this definition is to start the Turing machine with a
 tape corresponding to a value @{term n} and producing
 a new tape corresponding to the value @{term l} (the number of @{term Oc}s
-clustered on the tape).
+clustered on the output tape).
+Before we can prove the undecidability of the halting problem for Turing machines,
+we have to define how to compose them. Given our setup, this is relatively straightforward,
+if slightly fiddly.
 shift and change of a p
 composition of two ps
 two specific Turing machines. copying TM and dithering TM
 correctness of the copying TM
 measure for the copying TM, which we however omit.
 halting problem
 *}
 section {* Abacus Machines *}

changeset 33	284468a61346
parent 32	2557d2946354
child 34	22e5804b135c