# HG changeset patch # User Christian Urban # Date 1357738509 0 # Node ID 66cebc19ef18e1f7cda42c803032dae8a8ea8130 # Parent a959398693b5659367aaf05af9d7524194e43f28 updated diff -r a959398693b5 -r 66cebc19ef18 Literature/document.pdf Binary file Literature/document.pdf has changed diff -r a959398693b5 -r 66cebc19ef18 Paper.thy --- a/Paper.thy Tue Jan 08 01:21:02 2013 +0000 +++ b/Paper.thy Wed Jan 09 13:35:09 2013 +0000 @@ -60,46 +60,49 @@ theorem provers, like Isabelle/HOL, are at their best when the data-structures at hand are ``structurally'' defined, like lists, natural numbers, regular expressions, etc. Such data-structures come -with convenient reasoning infrastructures (for -example induction principles, recursion combinators and so on). But -this is \emph{not} the case with Turing machines (and also not with -register machines): underlying their definition is a set of states -together with a transition function, both of which are not -structurally defined. This means we have to implement our own -reasoning infrastructure in order to prove properties about them. This -leads to annoyingly fiddly formalisations. We noticed -first the difference between both, 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 standard proof of this property uses -the notion of \emph{universal Turing machines}. +with convenient reasoning infrastructures (for example induction +principles, recursion combinators and so on). But this is \emph{not} +the case with Turing machines (and also not with register machines): +underlying their definition is a set of states together with a +transition function, both of which are not structurally defined. This +means we have to implement our own reasoning infrastructure in order +to prove properties about them. This leads to annoyingly fiddly +formalisations. We noticed first the difference between both, +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 +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 -\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 guideline for -formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation -we followed 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 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}. +\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 +guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For +our formalisation we followed 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 +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 +\cite{Boolos87}, and similar ones we are aware of, are arguments why certain Turing +machines are correct. We will introduce Hoare-style proof rules +which help us with such correctness arguments of Turing machines. -The main difference between our formalisation and the one by Asperti and -Ricciotti is that their universal Turing -machine uses a different alphabet than the machines it simulates. They -write \cite[Page 23]{AspertiRicciotti12}: +The main difference between our formalisation and the one by Asperti +and Ricciotti is that their universal Turing machine uses a different +alphabet than the machines it simulates. They write \cite[Page +23]{AspertiRicciotti12}: \begin{quote}\it ``In particular, the fact that the universal machine operates with a @@ -108,25 +111,57 @@ \end{quote} \noindent -In this paper we follow the approach by Boolos et al \cite{Boolos87} -where Turing machines (and our -universal Turing machine) operates on tapes that contain only blank -or filled cells (respectively represented by 0 and 1---or in our -formalisation by @{term Bk} and @{term Oc}). +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 +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. - - +\medskip \noindent {\bf Contributions:} *} -section {* Formalisation *} +section {* Turing Machines *} text {* + + Tapes + + %\begin{center} + %\begin{tikzpicture} + %% + %\end{tikzpicture} + %\end{center} + + An action is defined as + + \begin{center} + \begin{tabular}{rcll} + @{text "a"} & $::=$ & @{term "W0"} & write blank (@{term Bk})\\ + & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\ + & $\mid$ & @{term L} & move left\\ + & $\mid$ & @{term R} & move right\\ + & $\mid$ & @{term Nop} & do nothing\\ + \end{tabular} + \end{center} + + For showing the undecidability of the halting problem, we need to consider + two specific Turing machines. *} +section {* Abacus Machines *} + +section {* Recursive Functions *} section {* Wang Tiles\label{Wang} *} @@ -138,7 +173,8 @@ section {* Related Work *} text {* - The most closely related work is by Norrish. He bases his approach on + The most closely related work is by Norrish \cite{Norrish11}, and Asperti and + Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on lambda-terms. For this he introduced a clever rewriting technology based on combinators and de-Bruijn indices for rewriting modulo $\beta$-equivalence (to keep it manageable) diff -r a959398693b5 -r 66cebc19ef18 document/root.bib --- a/document/root.bib Tue Jan 08 01:21:02 2013 +0000 +++ b/document/root.bib Wed Jan 09 13:35:09 2013 +0000 @@ -54,3 +54,15 @@ series = {LNCS}, volume = {6898} } + + +@Article{Post36, + author = {E.~Post}, + title = {{F}inite {C}ombinatory {P}rocesses-{F}ormulation 1}, + journal = {Journal of Symbolic Logic}, + year = {1936}, + volume = {1}, + number = {3}, + pages = {103--105} +} + diff -r a959398693b5 -r 66cebc19ef18 paper.pdf Binary file paper.pdf has changed