# HG changeset patch # User Christian Urban # Date 1357782411 0 # Node ID a961c2e4dcea9bf2d9d8e4f7685d2f9afb25897d # Parent 66cebc19ef18e1f7cda42c803032dae8a8ea8130 updated diff -r 66cebc19ef18 -r a961c2e4dcea Paper.thy --- 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 \ i + | None \ (Nop, 0))" + and "fetch p (Suc s) Oc = + (case nth_of p ((2 * s) + 1) of + Some i \ i + | None \ (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 "\"} & @{thm (rhs) new_tape_def2(1)}\\ + @{thm (lhs) new_tape_def2(2)} & @{text "\"} & @{thm (rhs) new_tape_def2(2)}\\ + @{thm (lhs) new_tape_def2(3)} & @{text "\"} & \\ + \multicolumn{3}{p{3cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\ + @{thm (lhs) new_tape_def2(4)} & @{text "\"} & \\ + \multicolumn{3}{p{2cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\ + @{thm (lhs) new_tape_def2(5)} & @{text "\"} & @{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 "\"} & @{thm (rhs) fetch_def2(1)}\\ + @{thm (lhs) fetch_def2(2)} & @{text "\"} & \\ + \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(2)}}\\ + @{thm (lhs) fetch_def2(3)} & @{text "\"} & \\ + \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. diff -r 66cebc19ef18 -r a961c2e4dcea document/root.tex --- a/document/root.tex Wed Jan 09 13:35:09 2013 +0000 +++ b/document/root.tex Thu Jan 10 01:46:51 2013 +0000 @@ -5,6 +5,8 @@ \usepackage{amssymb} \usepackage{mathpartir} \usepackage{pdfsetup} +\usepackage{tikz} +\usepackage{pgf} % urls in roman style, theory text in math-similar italics \urlstyle{rm} @@ -13,6 +15,10 @@ % for uniform font size %\renewcommand{\isastyle}{\isastyleminor} +\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} +\renewcommand{\isasymequiv}{$\dn$} +\renewcommand{\isasymemptyset}{$\varnothing$} +\renewcommand{\isacharunderscore}{\mbox{$\_$}} \begin{document} diff -r 66cebc19ef18 -r a961c2e4dcea paper.pdf Binary file paper.pdf has changed