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 convenient reasoning infrastructures (for |
63 with 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 fiddly formalisations. We noticed |
70 leads to annoyingly 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 from the literature that use them. |
75 wants to formalise the great many proofs from the literature that use them. |
76 We will analyse one example---undecidability of Wang tilings---in |
76 We will analyse one example---undecidability of Wang tilings---in |
77 detail in Section~\ref{Wang}. The standard proof of this property uses |
77 Section~\ref{Wang}. The standard proof of this property uses |
78 the notion of \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 complete formalisation of Turing |
82 \cite{AspertiRicciotti12}. They describe a complete formalisation of Turing |
83 machines in the Matita theorem prover, including an universal Turing |
83 machines in the Matita theorem prover, including a universal Turing |
84 machine. They report |
84 machine. They report |
85 that the informal proofs from which they started are not |
85 that the informal proofs from which they started are not |
86 ``sufficiently accurate to be directly used as a guideline for |
86 ``sufficiently accurate to be directly used as a guideline for |
87 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation |
87 formalization'' \cite[Page 2]{AspertiRicciotti12}. For our formalisation |
88 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 |
89 is quite detailed. Some details are left out however: for |
89 there is quite detailed. Some details are left out however: for |
90 example, it is only shown how the universal |
90 example, it is only shown how the universal |
91 Turing machine is constructed for Turing machines computing unary |
91 Turing machine is constructed for Turing machines computing unary |
92 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 |
93 $n$-ary functions. Similarly, when compiling recursive functions to |
93 $n$-ary functions. Similarly, when compiling recursive functions to |
94 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 |