58 of register machines) and recursive functions. To see the difficulties |
58 of register machines) and recursive functions. To see the difficulties |
59 involved with this work, one has to understand that interactive |
59 involved with this work, one has to understand that interactive |
60 theorem provers, like Isabelle/HOL, are at their best when the |
60 theorem provers, like Isabelle/HOL, are at their best when the |
61 data-structures at hand are ``structurally'' defined, like lists, |
61 data-structures at hand are ``structurally'' defined, like lists, |
62 natural numbers, regular expressions, etc. Such data-structures come |
62 natural numbers, regular expressions, etc. Such data-structures come |
63 in theorem provers with convenient reasoning infrastructures (for |
63 convenient reasoning infrastructures (for |
64 example induction principles, recursion combinators and so on). But |
64 example induction principles, recursion combinators and so on). But |
65 this is \emph{not} the case with Turing machines (and also not with |
65 this is \emph{not} the case with Turing machines (and also not with |
66 register machines): underlying their definition is a set of states |
66 register machines): underlying their definition is a set of states |
67 together with a transition function, both of which are not |
67 together with a transition function, both of which are not |
68 structurally defined. This means we have to implement our own |
68 structurally defined. This means we have to implement our own |
69 reasoning infrastructure in order to prove properties about them. This |
69 reasoning infrastructure in order to prove properties about them. This |
70 leads to annoyingly lengthy and detailed formalisations. We noticed |
70 leads to annoyingly lengthy and fiddly formalisations. We noticed |
71 first the difference between both structural and non-structural |
71 first the difference between both structural and non-structural |
72 ``worlds'' when formalising the Myhill-Nerode theorem, where regular |
72 ``worlds'' when formalising the Myhill-Nerode theorem, where regular |
73 expressions fared much better than automata \cite{WuZhangUrban11}. |
73 expressions fared much better than automata \cite{WuZhangUrban11}. |
74 However, with Turing machines there seems to be no alternative if one |
74 However, with Turing machines there seems to be no alternative if one |
75 wants to formalise the great many proofs that use them. We give as |
75 wants to formalise the great many proofs from the literature that use them. |
76 example one proof---undecidability of Wang tilings---in Section |
76 We will analyse one example---undecidability of Wang tilings---in |
77 \ref{Wang}. The standard proof of this property uses the notion of |
77 detail in Section~\ref{Wang}. The standard proof of this property uses |
78 \emph{universal Turing machines}. |
78 the notion of \emph{universal Turing machines}. |
79 |
79 |
80 We are not the first who formalised Turing machines in a theorem |
80 We are not the first who formalised Turing machines in a theorem |
81 prover: we are aware of the preliminary work by Asperti and Ricciotti |
81 prover: we are aware of the preliminary work by Asperti and Ricciotti |
82 \cite{AspertiRicciotti12}. They describe a formalisation of Turing |
82 \cite{AspertiRicciotti12}. They describe a complete formalisation of Turing |
83 machines in the Matita theorem prover. They report |
83 machines in the Matita theorem prover, including an universal Turing |
|
84 machine. They report |
84 that the informal proofs from which they started are not |
85 that the informal proofs from which they started are not |
85 ``sufficiently accurate to be directly used as a guideline for |
86 ``sufficiently accurate to be directly used as a guideline for |
86 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation |
87 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation |
87 we followed the proofs from the textbook \cite{Boolos87} and found that the description |
88 we followed the proofs from the textbook \cite{Boolos87} and found that the description |
88 is quite detailed. Some details are left out however: for |
89 is quite detailed. Some details are left out however: for |
90 Turing machine is constructed for Turing machines computing unary |
91 Turing machine is constructed for Turing machines computing unary |
91 functions. We had to figure out a way to generalize this result to |
92 functions. We had to figure out a way to generalize this result to |
92 $n$-ary functions. Similarly, when compiling recursive functions to |
93 $n$-ary functions. Similarly, when compiling recursive functions to |
93 abacus machines, the textbook again only shows how it can be done for |
94 abacus machines, the textbook again only shows how it can be done for |
94 2- and 3-ary functions, but in the formalisation we need arbitrary |
95 2- and 3-ary functions, but in the formalisation we need arbitrary |
95 function. But the general ideas for how to do this are clear enough in |
96 functions. But the general ideas for how to do this are clear enough in |
96 \cite{Boolos87}. |
97 \cite{Boolos87}. |
97 |
98 |
98 The main difference between our formalisation and the one by Asperti and |
99 The main difference between our formalisation and the one by Asperti and |
99 Ricciotti is |
100 Ricciotti is that their universal Turing |
|
101 machine uses a different alphabet than the machines it simulates. They |
|
102 write \cite[Page XXX]{AspertiRicciotti12}: |
100 |
103 |
101 that their universal machines |
104 \begin{quote}\it |
102 |
|
103 \begin{quote} |
|
104 ``In particular, the fact that the universal machine operates with a |
105 ``In particular, the fact that the universal machine operates with a |
105 different alphabet with respect to the machines it simulates is |
106 different alphabet with respect to the machines it simulates is |
106 annoying.'' |
107 annoying.'' |
107 \end{quote} |
108 \end{quote} |
108 |
109 |
|
110 \noindent |
|
111 In this paper we follow the approach by Boolos et al \cite{Boolos87} |
|
112 where Turing machines (and our |
|
113 universal Turing machine) operates on tapes that contain only blank |
|
114 or filled cells (respectively represented by 0 and 1---or in our |
|
115 formalisation by @{term Bk} or @{term Oc}). |
109 |
116 |
110 |
117 |
111 |
118 |
112 \noindent |
119 \noindent |
113 {\bf Contributions:} |
120 {\bf Contributions:} |