tm: comparison Paper.thy

equal deleted inserted replaced

-:7971da47e8c4
+:ae3d568b887b
 structural and non-structural, ``worlds'' when formalising the
 Myhill-Nerode theorem, where regular expressions fared much better
 than automata \cite{WuZhangUrban11}.  However, with Turing machines
 there seems to be no alternative if one wants to formalise the great
 many proofs from the literature that use them.  We will analyse one
-example---undecidability of Wang tilings---in Section~\ref{Wang}. The
+example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The
 standard proof of this property uses the notion of \emph{universal
 Turing machines}.
 We are not the first who formalised Turing machines in a theorem
 prover: we are aware of the preliminary work by Asperti and Ricciotti
 \end{quote}
 \noindent
 In this paper we follow the approach by Boolos et al \cite{Boolos87},
 which goes back to Post \cite{Post36}, where all Turing machines
-operate on tapes that contain only \emph{blank} or \emph{filled} cells
+operate on tapes that contain only \emph{blank} or \emph{occupied} cells
 (represented by @{term Bk} and @{term Oc}, respectively, in our
 formalisation). Traditionally the content of a cell can be any
 character from a finite alphabet. Although computationally equivalent,
 the more restrictive notion of Turing machines in \cite{Boolos87} makes
 the reasoning more uniform. In addition some proofs \emph{about} Turing
-machines will be simpler.  The reason is that one often need to encode
+machines will be simpler.  The reason is that one often needs to encode
-Turing machines---if the Turing machines are simpler, then the coding
+Turing machines---consequently if the Turing machines are simpler, then the coding
-functions are simpler. Unfortunately, the restrictiveness also makes
+functions are simpler too. Unfortunately, the restrictiveness also makes
 it harder to design programs for these Turing machines. Therefore in order
 to construct a \emph{universal Turing machine} we follow the proof in
 \cite{Boolos87} by relating abacus machines to Turing machines and in
 turn recursive functions to abacus machines. The universal Turing
-machine can then be constructed as recursive function.
+machine can then be constructed as a recursive function.
 \smallskip
 \noindent
 {\bf Contributions:}
 *}
 section {* Turing Machines *}
-text {*
+text {* \noindent
-\noindent
+Turing machines can be thought of as having a read-write-unit
-Turing machines can be thought of as having read-write-unit
 ``gliding'' over a potentially infinite tape. Boolos et
 al~\cite{Boolos87} only consider tapes with cells being either blank
-or occupied, which we represent with a datatype having two
+or occupied, which we represent by a datatype having two
-constructors, namely @{text Bk} and @{text Oc}.  One easy way to
+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 of the
+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. We have the
+read-write-unit 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
 be pictured as follows:
 \begin{center}
 & $\mid$ & @{term Nop} & do-nothing operation\\
 \end{tabular}
 \end{center}
 \noindent
-By using the @{term Nop} operation, we slightly deviate
+We slightly deviate
-from the presentation in \cite{Boolos87}; however its use
+from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
 will become important when we formalise universal Turing
-machines. Given a tape and an action, we can define the
+machines later. Given a tape and an action, we can define the
 following 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)}\\
 @{thm (lhs) new_tape_def2(3)} & @{text "\<equiv>"} & \\
-\multicolumn{3}{p{3cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\
+\multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\
 @{thm (lhs) new_tape_def2(4)} & @{text "\<equiv>"} & \\
-\multicolumn{3}{p{2cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\
+\multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\
 @{thm (lhs) new_tape_def2(5)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(5)}\\
 \end{tabular}
 \end{center}
 \noindent

changeset 20	ae3d568b887b
parent 19	7971da47e8c4
child 21	c5e3007fed2a