# HG changeset patch # User Christian Urban # Date 1357339742 0 # Node ID a7ec585d7f20c8c247da50718f1d21a4c026afaa # Parent dd400b5797e1118cf625d971116c103102dae849 updated diff -r dd400b5797e1 -r a7ec585d7f20 Paper.thy --- a/Paper.thy Fri Jan 04 13:10:30 2013 +0000 +++ b/Paper.thy Fri Jan 04 22:49:02 2013 +0000 @@ -53,42 +53,62 @@ \end{quote} \noindent -In this paper we took on this daunting prospect and provide a formalisation -of Turing machines, as well as Abacus machines (a kind of register machine) -and recursive functions. To see the difficulties involved with this work one -has to understantd that interactive 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). For them, they come with a convenient reasoning -infrastructure (for example induction principles, recursion combinators and so on). -But this is not the case with Turing machines (and also 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. This often -leads to annoyingly lengthy and detailed formalisations. We noticed first -the difference between both ``worlds'' when formalising the Myhill-Nerode -theorem ??? where regular expressions fared much better than automata. -However, with Turing machines there seems to be no alternative, because they -feature frequently in proofs. We will analyse one case, Wang tilings, at the end -of the paper, which uses also the notion of a Universal Turing Machine. +In this paper we took on this daunting prospect and provide a +formalisation of Turing machines, as well as abacus machines (a kind +of register machines) and recursive functions. To see the difficulties +involved with this work, one has to understand that interactive +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 +in theorem provers 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 lengthy and detailed 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 that use them. We give as +example one proof---undecidability of Wang tilings---in Section +\ref{Wang}. The standard proof of this property uses the notion of +\emph{universal Turing machines}. -The reason why reasoning about Turing machines -is challenging is because they are essentially ... +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 formalisation of Turing +machines in the Matita theorem prover. 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 +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 +function. But the general ideas for how to do this are clear enough in +\cite{Boolos87}. +The main difference between our formalisation and the one by Asperti and +Ricciotti is -For this we followed mainly the informal -proof given in the textbook \cite{Boolos87}. +that their universal machines + +\begin{quote} +``In particular, the fact that the universal machine operates with a +different alphabet with respect to the machines it simulates is +annoying.'' +\end{quote} -``In particular, the fact that the universal machine operates with a -different alphabet with respect to the machines it simulates is -annoying.'' he writes it is preliminary work \cite{AspertiRicciotti12} - - -Our formalisation follows \cite{Boolos87} - \noindent {\bf Contributions:} @@ -101,7 +121,7 @@ *} -section {* Wang Tiles *} +section {* Wang Tiles\label{Wang} *} text {* Used in texture mapings - graphics diff -r dd400b5797e1 -r a7ec585d7f20 document/root.bib --- a/document/root.bib Fri Jan 04 13:10:30 2013 +0000 +++ b/document/root.bib Fri Jan 04 22:49:02 2013 +0000 @@ -42,4 +42,15 @@ title = {{C}omputability and {L}ogic (2.~ed.)}, publisher = {Cambridge University Press}, year = {1987} -} \ No newline at end of file +} + +@inproceedings{WuZhangUrban11, + author = {C.~Wu and X.~Zhang and C.~Urban}, + title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions + ({P}roof {P}earl)}, + booktitle = {Proc.~of the 2nd Conference on Interactive Theorem Proving}, + year = {2011}, + pages = {341--356}, + series = {LNCS}, + volume = {6898} +} diff -r dd400b5797e1 -r a7ec585d7f20 paper.pdf Binary file paper.pdf has changed