--- a/Paper.thy Wed Jan 09 13:35:09 2013 +0000
+++ b/Paper.thy Thu Jan 10 01:46:51 2013 +0000
@@ -3,6 +3,50 @@
imports UTM
begin
+hide_const (open) s
+
+abbreviation
+ "update p a == new_tape a p"
+
+
+lemma fetch_def2:
+ shows "fetch p 0 b = (Nop, 0)"
+ and "fetch p (Suc s) Bk =
+ (case nth_of p (2 * s) of
+ Some i \<Rightarrow> i
+ | None \<Rightarrow> (Nop, 0))"
+ and "fetch p (Suc s) Oc =
+ (case nth_of p ((2 * s) + 1) of
+ Some i \<Rightarrow> i
+ | None \<Rightarrow> (Nop, 0))"
+by (auto split: block.splits simp add: fetch.simps)
+
+lemma new_tape_def2:
+ shows "new_tape W0 (l, r) == (l, Bk#(tl r))"
+ and "new_tape W1 (l, r) == (l, Oc#(tl r))"
+ and "new_tape L (l, r) ==
+ (if l = [] then ([], Bk#r) else (tl l, (hd l) # r))"
+ and "new_tape R (l, r) ==
+ (if r = [] then (Bk#l,[]) else ((hd r)#l, tl r))"
+ and "new_tape Nop (l, r) == (l, r)"
+apply -
+apply(rule_tac [!] eq_reflection)
+apply(auto split: taction.splits simp add: new_tape.simps)
+done
+
+lemma tstep_def2:
+ shows "tstep (s, l, []) p = (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))"
+ and "tstep (s, l, x#xs) p = (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))"
+by (auto split: prod.split list.split simp add: tstep.simps)
+
+consts DUMMY::'a
+
+notation (latex output)
+ Cons ("_::_" [78,77] 73) and
+ W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
+ W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
+ DUMMY ("\<^raw:\mbox{$\_$}>")
+
declare [[show_question_marks = false]]
(*>*)
@@ -82,9 +126,9 @@
\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 not ``sufficiently accurate to be directly used as a
+started are not ``sufficiently accurate to be directly useable as a
guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
-our formalisation we followed the proofs from the textbook
+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
@@ -113,18 +157,22 @@
\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 blank or filled cells (represented
-by @{term Bk} and @{term Oc}, respectively, in our
+operate on tapes that contain only \emph{blank} or \emph{filled} 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
-equivalennt, the more restrictive notion of Turing machines make
-the reasoning more uniform. Unfortunately, it also makes it
-harder to design programs for 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.
+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
+Turing machines---if the Turing machines are simpler, then the coding
+functions are simpler. 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.
-\medskip
+\smallskip
\noindent
{\bf Contributions:}
@@ -133,16 +181,51 @@
section {* Turing Machines *}
text {*
-
- Tapes
+ \noindent
+ 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
+ constructors, namely @{text Bk} and @{text Oc}. One easy 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
+ read-write-unit and @{term r} for the tape on the right. 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}
- %\begin{tikzpicture}
- %%
- %\end{tikzpicture}
- %\end{center}
+ \begin{center}
+ \begin{tikzpicture}
+ \draw[very thick] (-3.0,0) -- ( 3.0,0);
+ \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
+ \draw[very thick] (-0.25,0) -- (-0.25,0.5);
+ \draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
+ \draw[very thick] (-0.75,0) -- (-0.75,0.5);
+ \draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
+ \draw[very thick] (-1.25,0) -- (-1.25,0.5);
+ \draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
+ \draw[very thick] (-1.75,0) -- (-1.75,0.5);
+ \draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
+ \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
+ \draw[fill] (1.35,0.1) rectangle (1.65,0.4);
+ \draw[fill] (0.85,0.1) rectangle (1.15,0.4);
+ \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4);
+ \draw (-0.25,0.8) -- (-0.25,-0.8);
+ \draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
+ \node [anchor=base] at (-0.8,-0.5) {\small left list};
+ \node [anchor=base] at (0.35,-0.5) {\small right list};
+ \node [anchor=base] at (0.1,0.7) {\small head};
+ \node [anchor=base] at (-2.2,0.2) {\ldots};
+ \node [anchor=base] at ( 2.3,0.2) {\ldots};
+ \end{tikzpicture}
+ \end{center}
- An action is defined as
+ \noindent
+ Note that by using lists each side of the tape is only finite. The
+ potential infinity is achieved by adding an appropriate blank cell
+ whenever the read-write unit goes over the ``edge'' of the tape. To
+ make this formal we define five possible \emph{actions}
+ the Turing machine can perform:
\begin{center}
\begin{tabular}{rcll}
@@ -150,10 +233,93 @@
& $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\
& $\mid$ & @{term L} & move left\\
& $\mid$ & @{term R} & move right\\
- & $\mid$ & @{term Nop} & do nothing\\
+ & $\mid$ & @{term Nop} & do-nothing operation\\
+ \end{tabular}
+ \end{center}
+
+ \noindent
+ By using the @{term Nop} operation, we slightly deviate
+ from the presentation in \cite{Boolos87}; however its use
+ will become important when we formalise universal Turing
+ machines. 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)}}\\
+ @{thm (lhs) new_tape_def2(4)} & @{text "\<equiv>"} & \\
+ \multicolumn{3}{p{2cm}}{\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
+ The first two clauses replace the head of the right-list
+ with new @{term Bk} or @{term Oc}, repsectively. To see that
+ these clauses make sense in case where @{text r} is the empty
+ list, one has to know that the tail function, @{term tl}, is defined
+ such that @{term "tl [] == []"} holds. The third clause
+ implements the move of the read-write unit to the left: we need
+ to test if the left-list is empty; if yes, then we just add a
+ blank cell to the right-list; otherwise we have to remove the
+ head from the left-list and add it to the right-list. Similarly
+ in the clause for the right move. The @{term Nop} operation
+ 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 read-write unit is currently possitioned. 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 to the left and then back
+ to the right can change the tape (in case of going
+ over the ``edge''). Therefore they distinguish four
+ cases where the tape is empty as well as the read-write unit
+ on the left edge, respectively right edge, or in the
+ middle. The reading and moving of the tape is then
+ defined in terms of these four cases. Since we are not
+ going to use the notion of tape equality, we can
+ get away with the definition above and be done with
+ all corner cases.
+
+ Next we need to define the \emph{states} of a Turing machine. Given
+ how little is usually said about how to represent states in informal
+ presentaions, it might be surprising that in a theorem prover we have
+ to select carfully a representation. If we use the naive representation
+ as a Turing machine consiting of a finite set of states, then we
+ will have difficulties composing two Turing machines. We would need
+ to somehow combine the two finite sets of states, possibly renaming
+ states apart if both machines share states. 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 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.
+
+ An \emph{instruction} of a Turing machine is a pair consisting of a
+ natural number (the next state) and an action. A \emph{program} of a Turing
+ machine is then a list of such pairs. Given a program @{term p}, a state
+ and a cell being read by the read-write unnit, we need to fetch
+ the corresponding instruction in the program. For this we define
+ the function @{term fetch}
+
+ \begin{center}
+ \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{thm (lhs) fetch_def2(1)[where b=DUMMY]} & @{text "\<equiv>"} & @{thm (rhs) fetch_def2(1)}\\
+ @{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\
+ \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(2)}}\\
+ @{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\
+ \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(3)}}\\
+ \end{tabular}
+ \end{center}
+
+
For showing the undecidability of the halting problem, we need to consider
two specific Turing machines.