31 |
31 |
32 section {* Introduction *} |
32 section {* Introduction *} |
33 |
33 |
34 text {* |
34 text {* |
35 |
35 |
|
36 %\noindent |
|
37 %We formalised in earlier work the correctness proofs for two |
|
38 %algorithms in Isabelle/HOL---one about type-checking in |
|
39 %LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests |
|
40 %in access control~\cite{WuZhangUrban12}. The formalisations |
|
41 %uncovered a gap in the informal correctness proof of the former and |
|
42 %made us realise that important details were left out in the informal |
|
43 %model for the latter. However, in both cases we were unable to |
|
44 %formalise in Isabelle/HOL computability arguments about the |
|
45 %algorithms. |
|
46 |
|
47 |
36 \noindent |
48 \noindent |
37 We formalised in earlier work the correctness proofs for two |
49 Suppose you want to mechanise a proof whether a predicate @{term P}, say, is |
38 algorithms in Isabelle/HOL---one about type-checking in |
50 decidable or not. Decidability of @{text P} usually amounts to showing |
39 LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests |
|
40 in access control~\cite{WuZhangUrban12}. The formalisations |
|
41 uncovered a gap in the informal correctness proof of the former and |
|
42 made us realise that important details were left out in the informal |
|
43 model for the latter. However, in both cases we were unable to |
|
44 formalise in Isabelle/HOL computability arguments about the |
|
45 algorithms. The reason is that both algorithms are formulated in terms |
|
46 of inductive predicates. Suppose @{text "P"} stands for one such |
|
47 predicate. Decidability of @{text P} usually amounts to showing |
|
48 whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work |
51 whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work |
49 in Isabelle/HOL, since it is a theorem prover based on classical logic |
52 in Isabelle/HOL and other HOL theorem provers, since they are based on classical logic |
50 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} |
53 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} |
51 is always provable no matter whether @{text P} is constructed by |
54 is always provable no matter whether @{text P} is constructed by |
52 computable means. The same problem would arise if we had formulated |
55 computable means. |
53 the algorithms as recursive functions, because internally in |
56 |
54 Isabelle/HOL, like in all HOL-based theorem provers, functions are |
57 %The same problem would arise if we had formulated |
55 represented as inductively defined predicates too. |
58 %the algorithms as recursive functions, because internally in |
56 |
59 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
57 The only satisfying way out of this problem in a theorem prover based on classical |
60 %represented as inductively defined predicates too. |
58 logic is to formalise a theory of computability. Norrish provided such |
61 |
59 a formalisation for the HOL4 theorem prover. He choose the |
62 The only satisfying way out of this problem in a theorem prover based |
60 $\lambda$-calculus as the starting point for his formalisation |
63 on classical logic is to formalise a theory of computability. Norrish |
61 of computability theory, |
64 provided such a formalisation for the HOL4 theorem prover. He choose |
62 because of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his |
65 the $\lambda$-calculus as the starting point for his formalisation of |
63 formalisation is a clever infrastructure for reducing |
66 computability theory, because of its ``simplicity'' \cite[Page |
64 $\lambda$-terms. He also established the computational equivalence |
67 297]{Norrish11}. Part of his formalisation is a clever infrastructure |
65 between the $\lambda$-calculus and recursive functions. Nevertheless he |
68 for reducing $\lambda$-terms. He also established the computational |
66 concluded that it would be ``appealing'' to have formalisations for more |
69 equivalence between the $\lambda$-calculus and recursive functions. |
67 operational models of computations, such as Turing machines or register |
70 Nevertheless he concluded that it would be ``appealing'' |
68 machines. One reason is that many proofs in the literature use |
71 to have formalisations for more operational models of |
69 them. He noted however that in the context of theorem provers |
72 computations, such as Turing machines or register machines. One |
70 \cite[Page 310]{Norrish11}: |
73 reason is that many proofs in the literature use them. He noted |
|
74 however that in the context of theorem provers \cite[Page 310]{Norrish11}: |
71 |
75 |
72 \begin{quote} |
76 \begin{quote} |
73 \it``If register machines are unappealing because of their |
77 \it``If register machines are unappealing because of their |
74 general fiddliness, Turing machines are an even more |
78 general fiddliness,\\ Turing machines are an even more |
75 daunting prospect.'' |
79 daunting prospect.'' |
76 \end{quote} |
80 \end{quote} |
77 |
81 |
78 \noindent |
82 \noindent |
79 In this paper we take on this daunting prospect and provide a |
83 In this paper we take on this daunting prospect and provide a |
80 formalisation of Turing machines, as well as abacus machines (a kind |
84 formalisation of Turing machines, as well as abacus machines (a kind |
81 of register machines) and recursive functions. To see the difficulties |
85 of register machines) and recursive functions. To see the difficulties |
82 involved with this work, one has to understand that interactive |
86 involved with this work, one has to understand that Turing machine |
83 theorem provers, like Isabelle/HOL, are at their best when the |
87 programs can be completely \emph{unstructured}, behaving |
84 data-structures at hand are ``structurally'' defined, like lists, |
88 similar to Basic's infamous goto. This precludes in the |
85 natural numbers, regular expressions, etc. Such data-structures come |
89 general case a compositional Hoare-style reasoning about Turing |
86 with convenient reasoning infrastructures (for example induction |
90 programs. We provide such Hoare-rules for when it is possible to |
87 principles, recursion combinators and so on). But this is \emph{not} |
91 reason in a compositional manner (which is fortunately quite often), but also tackle |
88 the case with Turing machines (and also not with register machines): |
92 the more complicated case when we translate abacus programs into |
89 underlying their definitions are sets of states together with |
93 Turing programs. This aspect of reasoning about computability theory |
90 transition functions, all of which are not structurally defined. This |
94 is usually completely left out in the informal literature, e.g.~\cite{Boolos87}. |
91 means we have to implement our own reasoning infrastructure in order |
95 |
92 to prove properties about them. This leads to annoyingly fiddly |
96 %To see the difficulties |
93 formalisations. We noticed first the difference between both, |
97 %involved with this work, one has to understand that interactive |
94 structural and non-structural, ``worlds'' when formalising the |
98 %theorem provers, like Isabelle/HOL, are at their best when the |
95 Myhill-Nerode theorem, where regular expressions fared much better |
99 %data-structures at hand are ``structurally'' defined, like lists, |
96 than automata \cite{WuZhangUrban11}. However, with Turing machines |
100 %natural numbers, regular expressions, etc. Such data-structures come |
97 there seems to be no alternative if one wants to formalise the great |
101 %with convenient reasoning infrastructures (for example induction |
98 many proofs from the literature that use them. We will analyse one |
102 %principles, recursion combinators and so on). But this is \emph{not} |
99 example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The |
103 %the case with Turing machines (and also not with register machines): |
100 standard proof of this property uses the notion of universal |
104 %underlying their definitions are sets of states together with |
101 Turing machines. |
105 %transition functions, all of which are not structurally defined. This |
102 |
106 %means we have to implement our own reasoning infrastructure in order |
103 We are not the first who formalised Turing machines in a theorem |
107 %to prove properties about them. This leads to annoyingly fiddly |
104 prover: we are aware of the preliminary work by Asperti and Ricciotti |
108 %formalisations. We noticed first the difference between both, |
|
109 %structural and non-structural, ``worlds'' when formalising the |
|
110 %Myhill-Nerode theorem, where regular expressions fared much better |
|
111 %than automata \cite{WuZhangUrban11}. However, with Turing machines |
|
112 %there seems to be no alternative if one wants to formalise the great |
|
113 %many proofs from the literature that use them. We will analyse one |
|
114 %example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The |
|
115 %standard proof of this property uses the notion of universal |
|
116 %Turing machines. |
|
117 |
|
118 We are not the first who formalised Turing machines: we are aware |
|
119 of the preliminary work by Asperti and Ricciotti |
105 \cite{AspertiRicciotti12}. They describe a complete formalisation of |
120 \cite{AspertiRicciotti12}. They describe a complete formalisation of |
106 Turing machines in the Matita theorem prover, including a universal |
121 Turing machines in the Matita theorem prover, including a universal |
107 Turing machine. They report that the informal proofs from which they |
122 Turing machine. They report that the informal proofs from which they |
108 started are \emph{not} ``sufficiently accurate to be directly usable as a |
123 started are \emph{not} ``sufficiently accurate to be directly usable as a |
109 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
124 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
114 machines computing unary functions. We had to figure out a way to |
129 machines computing unary functions. We had to figure out a way to |
115 generalise this result to $n$-ary functions. Similarly, when compiling |
130 generalise this result to $n$-ary functions. Similarly, when compiling |
116 recursive functions to abacus machines, the textbook again only shows |
131 recursive functions to abacus machines, the textbook again only shows |
117 how it can be done for 2- and 3-ary functions, but in the |
132 how it can be done for 2- and 3-ary functions, but in the |
118 formalisation we need arbitrary functions. But the general ideas for |
133 formalisation we need arbitrary functions. But the general ideas for |
119 how to do this are clear enough in \cite{Boolos87}. However, one |
134 how to do this are clear enough in \cite{Boolos87}. |
120 aspect that is completely left out from the informal description in |
135 %However, one |
121 \cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing |
136 %aspect that is completely left out from the informal description in |
122 machines are correct. We will introduce Hoare-style proof rules |
137 %\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing |
123 which help us with such correctness arguments of Turing machines. |
138 %machines are correct. We will introduce Hoare-style proof rules |
|
139 %which help us with such correctness arguments of Turing machines. |
124 |
140 |
125 The main difference between our formalisation and the one by Asperti |
141 The main difference between our formalisation and the one by Asperti |
126 and Ricciotti is that their universal Turing machine uses a different |
142 and Ricciotti is that their universal Turing machine uses a different |
127 alphabet than the machines it simulates. They write \cite[Page |
143 alphabet than the machines it simulates. They write \cite[Page |
128 23]{AspertiRicciotti12}: |
144 23]{AspertiRicciotti12}: |
257 blank cell to the right-list; otherwise we have to remove the |
271 blank cell to the right-list; otherwise we have to remove the |
258 head from the left-list and prepend it to the right-list. Similarly |
272 head from the left-list and prepend it to the right-list. Similarly |
259 in the fourth clause for a right move action. The @{term Nop} operation |
273 in the fourth clause for a right move action. The @{term Nop} operation |
260 leaves the the tape unchanged (last clause). |
274 leaves the the tape unchanged (last clause). |
261 |
275 |
262 Note that our treatment of the tape is rather ``unsymmetric''---we |
276 %Note that our treatment of the tape is rather ``unsymmetric''---we |
263 have the convention that the head of the right-list is where the |
277 %have the convention that the head of the right-list is where the |
264 head is currently positioned. Asperti and Ricciotti |
278 %head is currently positioned. Asperti and Ricciotti |
265 \cite{AspertiRicciotti12} also considered such a representation, but |
279 %\cite{AspertiRicciotti12} also considered such a representation, but |
266 dismiss it as it complicates their definition for \emph{tape |
280 %dismiss it as it complicates their definition for \emph{tape |
267 equality}. The reason is that moving the head one step to |
281 %equality}. The reason is that moving the head one step to |
268 the left and then back to the right might change the tape (in case |
282 %the left and then back to the right might change the tape (in case |
269 of going over the ``edge''). Therefore they distinguish four types |
283 %of going over the ``edge''). Therefore they distinguish four types |
270 of tapes: one where the tape is empty; another where the head |
284 %of tapes: one where the tape is empty; another where the head |
271 is on the left edge, respectively right edge, and in the middle |
285 %is on the left edge, respectively right edge, and in the middle |
272 of the tape. The reading, writing and moving of the tape is then |
286 %of the tape. The reading, writing and moving of the tape is then |
273 defined in terms of these four cases. In this way they can keep the |
287 %defined in terms of these four cases. In this way they can keep the |
274 tape in a ``normalised'' form, and thus making a left-move followed |
288 %tape in a ``normalised'' form, and thus making a left-move followed |
275 by a right-move being the identity on tapes. Since we are not using |
289 %by a right-move being the identity on tapes. Since we are not using |
276 the notion of tape equality, we can get away with the unsymmetric |
290 %the notion of tape equality, we can get away with the unsymmetric |
277 definition above, and by using the @{term update} function |
291 %definition above, and by using the @{term update} function |
278 cover uniformly all cases including corner cases. |
292 %cover uniformly all cases including corner cases. |
279 |
293 |
280 Next we need to define the \emph{states} of a Turing machine. Given |
294 Next we need to define the \emph{states} of a Turing machine. Given |
281 how little is usually said about how to represent them in informal |
295 how little is usually said about how to represent them in informal |
282 presentations, it might be surprising that in a theorem prover we |
296 presentations, it might be surprising that in a theorem prover we |
283 have to select carefully a representation. If we use the naive |
297 have to select carefully a representation. If we use the naive |