92 steps ("nsteps") and |
92 steps ("nsteps") and |
93 abc_lm_v ("lookup") and |
93 abc_lm_v ("lookup") and |
94 abc_lm_s ("set") and |
94 abc_lm_s ("set") and |
95 haltP ("stdhalt") and |
95 haltP ("stdhalt") and |
96 tshift ("shift") and |
96 tshift ("shift") and |
|
97 tcopy ("copy") and |
97 change_termi_state ("adjust") and |
98 change_termi_state ("adjust") and |
98 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
99 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
99 t_add ("_ \<oplus> _") and |
100 t_add ("_ \<oplus> _") and |
100 DUMMY ("\<^raw:\mbox{$\_$}>") |
101 DUMMY ("\<^raw:\mbox{$\_$}>") |
101 |
102 |
176 We are not the first who formalised Turing machines in a theorem |
177 We are not the first who formalised Turing machines in a theorem |
177 prover: we are aware of the preliminary work by Asperti and Ricciotti |
178 prover: we are aware of the preliminary work by Asperti and Ricciotti |
178 \cite{AspertiRicciotti12}. They describe a complete formalisation of |
179 \cite{AspertiRicciotti12}. They describe a complete formalisation of |
179 Turing machines in the Matita theorem prover, including a universal |
180 Turing machines in the Matita theorem prover, including a universal |
180 Turing machine. They report that the informal proofs from which they |
181 Turing machine. They report that the informal proofs from which they |
181 started are \emph{not} ``sufficiently accurate to be directly useable as a |
182 started are \emph{not} ``sufficiently accurate to be directly usable as a |
182 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
183 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
183 our formalisation we followed mainly the proofs from the textbook |
184 our formalisation we followed mainly the proofs from the textbook |
184 \cite{Boolos87} and found that the description there is quite |
185 \cite{Boolos87} and found that the description there is quite |
185 detailed. Some details are left out however: for example, it is only |
186 detailed. Some details are left out however: for example, it is only |
186 shown how the universal Turing machine is constructed for Turing |
187 shown how the universal Turing machine is constructed for Turing |
187 machines computing unary functions. We had to figure out a way to |
188 machines computing unary functions. We had to figure out a way to |
188 generalize this result to $n$-ary functions. Similarly, when compiling |
189 generalise this result to $n$-ary functions. Similarly, when compiling |
189 recursive functions to abacus machines, the textbook again only shows |
190 recursive functions to abacus machines, the textbook again only shows |
190 how it can be done for 2- and 3-ary functions, but in the |
191 how it can be done for 2- and 3-ary functions, but in the |
191 formalisation we need arbitrary functions. But the general ideas for |
192 formalisation we need arbitrary functions. But the general ideas for |
192 how to do this are clear enough in \cite{Boolos87}. However, one |
193 how to do this are clear enough in \cite{Boolos87}. However, one |
193 aspect that is completely left out from the informal description in |
194 aspect that is completely left out from the informal description in |
309 \end{tabular} |
310 \end{tabular} |
310 \end{center} |
311 \end{center} |
311 |
312 |
312 \noindent |
313 \noindent |
313 The first two clauses replace the head of the right-list |
314 The first two clauses replace the head of the right-list |
314 with a new @{term Bk} or @{term Oc}, repsectively. To see that |
315 with a new @{term Bk} or @{term Oc}, respectively. To see that |
315 these two clauses make sense in case where @{text r} is the empty |
316 these two clauses make sense in case where @{text r} is the empty |
316 list, one has to know that the tail function, @{term tl}, is defined in |
317 list, one has to know that the tail function, @{term tl}, is defined in |
317 Isabelle/HOL |
318 Isabelle/HOL |
318 such that @{term "tl [] == []"} holds. The third clause |
319 such that @{term "tl [] == []"} holds. The third clause |
319 implements the move of the head one step to the left: we need |
320 implements the move of the head one step to the left: we need |
337 defined in terms of these four cases. In this way they can keep the |
338 defined in terms of these four cases. In this way they can keep the |
338 tape in a ``normalised'' form, and thus making a left-move followed |
339 tape in a ``normalised'' form, and thus making a left-move followed |
339 by a right-move being the identity on tapes. Since we are not using |
340 by a right-move being the identity on tapes. Since we are not using |
340 the notion of tape equality, we can get away with the unsymmetric |
341 the notion of tape equality, we can get away with the unsymmetric |
341 definition above, and by using the @{term update} function |
342 definition above, and by using the @{term update} function |
342 cover uniformely all cases including corner cases. |
343 cover uniformly all cases including corner cases. |
343 |
344 |
344 Next we need to define the \emph{states} of a Turing machine. Given |
345 Next we need to define the \emph{states} of a Turing machine. Given |
345 how little is usually said about how to represent them in informal |
346 how little is usually said about how to represent them in informal |
346 presentations, it might be surprising that in a theorem prover we |
347 presentations, it might be surprising that in a theorem prover we |
347 have to select carfully a representation. If we use the naive |
348 have to select carefully a representation. If we use the naive |
348 representation where a Turing machine consists of a finite set of |
349 representation where a Turing machine consists of a finite set of |
349 states, then we will have difficulties composing two Turing |
350 states, then we will have difficulties composing two Turing |
350 machines: we would need to combine two finite sets of states, |
351 machines: we would need to combine two finite sets of states, |
351 possibly renaming states apart whenever both machines share |
352 possibly renaming states apart whenever both machines share |
352 states.\footnote{The usual disjoint union operation in Isabelle/HOL |
353 states.\footnote{The usual disjoint union operation in Isabelle/HOL |
532 a new tape corresponding to the value @{term l} (the number of @{term Oc}s |
533 a new tape corresponding to the value @{term l} (the number of @{term Oc}s |
533 clustered on the output tape). |
534 clustered on the output tape). |
534 |
535 |
535 Before we can prove the undecidability of the halting problem for Turing machines, |
536 Before we can prove the undecidability of the halting problem for Turing machines, |
536 we have to define how to compose two Turing machines. Given our setup, this is |
537 we have to define how to compose two Turing machines. Given our setup, this is |
537 relatively straightforward, if slightly fiddly. We have the following two |
538 relatively straightforward, if slightly fiddly. We use the following two |
538 auxiliary functions: |
539 auxiliary functions: |
539 |
540 |
540 \begin{center} |
541 \begin{center} |
541 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
542 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
542 @{thm (lhs) tshift_def2} @{text "\<equiv>"}\\ |
543 @{thm (lhs) tshift_def2} @{text "\<equiv>"}\\ |
546 \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\ |
547 \hspace{14mm}@{text "(a, if s = 0 then length p div 2 + 1 else s)) p"}\\ |
547 \end{tabular} |
548 \end{tabular} |
548 \end{center} |
549 \end{center} |
549 |
550 |
550 \noindent |
551 \noindent |
551 With this we can define the \emph{sequential composition} of two |
552 The first adds @{text n} to all states, exept the @{text 0}-state, |
552 Turing machines @{text "M\<^isub>1"} and @{text "M\<^isub>2"} |
553 thus moving all ``regular'' states to the segment starting at @{text |
553 |
554 n}; the second adds @{term "length p div 2 + 1"} to the @{text |
554 \begin{center} |
555 0}-state, thus ridirecting all references to the ``halting state'' |
555 @{thm t_add.simps[where ?t1.0="M\<^isub>1" and ?t2.0="M\<^isub>2", THEN eq_reflection]} |
556 to the first state after the program @{text p}. With these two |
556 \end{center} |
557 functions in place, we can define the \emph{sequential composition} |
557 |
558 of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} |
|
559 |
|
560 \begin{center} |
|
561 @{thm t_add.simps[where ?t1.0="p\<^isub>1" and ?t2.0="p\<^isub>2", THEN eq_reflection]} |
|
562 \end{center} |
|
563 |
|
564 \noindent |
|
565 This means @{text "p\<^isub>1"} is executed first. Whenever it originally |
|
566 transitioned to the @{text 0}-state, it will in the composed program transition to the starting |
|
567 state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"} |
|
568 have been shifted in order to make sure that the states of the composed |
|
569 program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' |
|
570 an initial segment of the natural numbers. |
|
571 |
|
572 \begin{center} |
|
573 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}} |
|
574 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
|
575 \end{tabular} |
|
576 \end{center} |
558 |
577 |
559 |
578 |
560 assertion holds for all tapes |
579 assertion holds for all tapes |
561 |
580 |
562 Hoare rule for composition |
581 Hoare rule for composition |