tm: comparison Paper.thy

equal deleted inserted replaced

-:4b35e0e0784b
+:c9b689bb4156
 steps ("nsteps") and
 abc_lm_v ("lookup") and
 abc_lm_s ("set") and
 haltP ("stdhalt") and
 tshift ("shift") and
+tcopy ("copy") and
 change_termi_state ("adjust") and
 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and
 t_add ("_ \<oplus> _") and
 DUMMY  ("\<^raw:\mbox{$\_$}>")
 We are not the first who formalised Turing machines in a theorem
 prover: we are aware of the preliminary work by Asperti and Ricciotti
 \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 useable as a
+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
 \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
-generalize this result to $n$-ary functions. Similarly, when compiling
+generalise this result to $n$-ary functions. Similarly, when compiling
 recursive functions to abacus machines, the textbook again only shows
 how it can be done for 2- and 3-ary functions, but in the
 formalisation we need arbitrary functions. But the general ideas for
 how to do this are clear enough in \cite{Boolos87}. However, one
 aspect that is completely left out from the informal description in
 \end{tabular}
 \end{center}
 \noindent
 The first two clauses replace the head of the right-list
-with a new @{term Bk} or @{term Oc}, repsectively. To see that
+with a new @{term Bk} or @{term Oc}, respectively. 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 defined in
 Isabelle/HOL
 such that @{term "tl [] == []"} holds. The third clause
 implements the move of the head one step to the left: we need
 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 corner cases.
+cover uniformly 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
 presentations, it might be surprising that in a theorem prover we
-have to select carfully a representation. If we use the naive
+have to select carefully 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: 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
 a new tape corresponding to the value @{term l} (the number of @{term Oc}s
 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 two Turing machines. Given our setup, this is
-relatively straightforward, if slightly fiddly. We have the following two
+relatively straightforward, if slightly fiddly. We use the following two
 auxiliary functions:
 \begin{center}
 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
 @{thm (lhs) tshift_def2} @{text "\<equiv>"}\\
 \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\
 \end{tabular}
 \end{center}
 \noindent
-With this we can define the \emph{sequential composition} of two
+The first adds @{text n} to all states, exept the @{text 0}-state,
-Turing machines @{text "M\<^isub>1"} and @{text "M\<^isub>2"}
+thus moving all ``regular'' states to the segment starting at @{text
+n}; the second adds @{term "length p div 2 + 1"} to the @{text
-\begin{center}
+0}-state, thus ridirecting all references to the ``halting state''
-@{thm t_add.simps[where ?t1.0="M\<^isub>1" and ?t2.0="M\<^isub>2", THEN eq_reflection]}
+to the first state after the program @{text p}.  With these two
-\end{center}
+functions in place, we can define the \emph{sequential composition}
+of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}
+\begin{center}
+@{thm t_add.simps[where ?t1.0="p\<^isub>1" and ?t2.0="p\<^isub>2", THEN eq_reflection]}
+\end{center}
+\noindent
+This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+transitioned to the @{text 0}-state, it will in the composed program transition to the starting
+state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+have been shifted in order to make sure that the states of the composed
+program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
+an initial segment of the natural numbers.
+\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

changeset 37	c9b689bb4156
parent 36	4b35e0e0784b
child 38	8f8db701f69f