189 and "14 = Suc 13" |
189 and "14 = Suc 13" |
190 and "15 = Suc 14" |
190 and "15 = Suc 14" |
191 apply(arith)+ |
191 apply(arith)+ |
192 done |
192 done |
193 |
193 |
194 (* |
194 lemma tm_wf_simps: |
195 lemma "run tcopy (1, [], <0::nat>) = (0, [Bk], [Oc, Bk, Oc])" |
195 "tm_wf0 p = (2 <=length p \<and> is_even(length p) \<and> (\<forall>(a,s) \<in> set p. s <= (length p) div 2))" |
196 apply(subst run.simps) |
196 apply(simp add: tm_wf.simps) |
197 apply(simp) |
|
198 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) |
|
199 apply(subst run.simps) |
|
200 apply(simp) |
|
201 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) |
|
202 apply(subst run.simps) |
|
203 apply(simp) |
|
204 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) |
|
205 apply(subst run.simps) |
|
206 apply(simp) |
|
207 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) |
|
208 apply(subst run.simps) |
|
209 apply(simp) |
|
210 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) |
|
211 apply(subst run.simps) |
|
212 apply(simp) |
|
213 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) |
|
214 apply(subst run.simps) |
|
215 apply(simp) |
|
216 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral nth_of.simps del: run.simps) |
|
217 apply(simp only: numeral[symmetric]) |
|
218 apply(simp) |
|
219 apply(subst run.simps) |
|
220 apply(simp) |
|
221 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) |
|
222 apply(simp only: numeral[symmetric]) |
|
223 apply(simp) |
|
224 apply(subst run.simps) |
|
225 apply(simp) |
|
226 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) |
|
227 apply(simp only: numeral[symmetric]) |
|
228 apply(simp) |
|
229 apply(subst run.simps) |
|
230 apply(simp) |
|
231 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) |
|
232 apply(simp only: numeral[symmetric]) |
|
233 apply(simp) |
|
234 apply(subst run.simps) |
|
235 apply(simp) |
|
236 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) |
|
237 apply(simp only: numeral[symmetric]) |
|
238 apply(simp) |
|
239 apply(subst run.simps) |
|
240 apply(simp) |
|
241 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) |
|
242 apply(simp only: numeral[symmetric]) |
|
243 apply(simp) |
|
244 apply(subst run.simps) |
|
245 apply(simp) |
|
246 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) |
|
247 apply(simp only: numeral[symmetric]) |
|
248 apply(simp) |
|
249 apply(subst run.simps) |
|
250 apply(simp) |
|
251 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) |
|
252 apply(simp only: numeral[symmetric]) |
|
253 apply(simp) |
|
254 apply(subst run.simps) |
|
255 apply(simp) |
|
256 apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) |
|
257 apply(simp only: numeral[symmetric]) |
|
258 apply(simp) |
|
259 apply(subst run.simps) |
|
260 apply(simp) |
|
261 done |
197 done |
262 *) |
|
263 |
198 |
264 (*>*) |
199 (*>*) |
265 |
200 |
266 section {* Introduction *} |
201 section {* Introduction *} |
267 |
202 |
418 \cite{AspertiRicciotti12}, instead follow the proof in |
353 \cite{AspertiRicciotti12}, instead follow the proof in |
419 \cite{Boolos87} by translating abacus machines to Turing machines and in |
354 \cite{Boolos87} by translating abacus machines to Turing machines and in |
420 turn recursive functions to abacus machines. The universal Turing |
355 turn recursive functions to abacus machines. The universal Turing |
421 machine can then be constructed by translating from a (universal) recursive function. |
356 machine can then be constructed by translating from a (universal) recursive function. |
422 The part of mechanising the translation of recursive function to register |
357 The part of mechanising the translation of recursive function to register |
423 machines has already been done by Zammit in HOL \cite{Zammit99}, |
358 machines has already been done by Zammit in HOL4 \cite{Zammit99}, |
424 although his register machines use a slightly different instruction |
359 although his register machines use a slightly different instruction |
425 set than the one described in \cite{Boolos87}. |
360 set than the one described in \cite{Boolos87}. |
426 |
361 |
427 \smallskip |
362 \smallskip |
428 \noindent |
363 \noindent |
504 |
439 |
505 \begin{center} |
440 \begin{center} |
506 \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l} |
441 \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l} |
507 @{text "a"} & $::=$ & @{term "W0"} & (write blank, @{term Bk})\\ |
442 @{text "a"} & $::=$ & @{term "W0"} & (write blank, @{term Bk})\\ |
508 & $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\ |
443 & $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\ |
509 \end{tabular} |
|
510 \begin{tabular}[t]{rcl@ {\hspace{2mm}}l} |
|
511 & $\mid$ & @{term L} & (move left)\\ |
444 & $\mid$ & @{term L} & (move left)\\ |
512 & $\mid$ & @{term R} & (move right)\\ |
445 & $\mid$ & @{term R} & (move right)\\ |
513 \end{tabular} |
|
514 \begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}} |
|
515 & $\mid$ & @{term Nop} & (do-nothing operation)\\ |
446 & $\mid$ & @{term Nop} & (do-nothing operation)\\ |
516 \end{tabular} |
447 \end{tabular} |
517 \end{center} |
448 \end{center} |
518 |
449 |
519 \noindent |
450 \noindent |
643 (@{term None}-case). We often have to restrict Turing machine programs |
574 (@{term None}-case). We often have to restrict Turing machine programs |
644 to be well-formed: a program @{term p} is \emph{well-formed} if it |
575 to be well-formed: a program @{term p} is \emph{well-formed} if it |
645 satisfies the following three properties: |
576 satisfies the following three properties: |
646 |
577 |
647 \begin{center} |
578 \begin{center} |
648 @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]} |
579 @{thm tm_wf_simps[where p="p", THEN eq_reflection]} |
649 \end{center} |
580 \end{center} |
650 |
581 |
651 \noindent |
582 \noindent |
652 The first states that @{text p} must have at least an instruction for the starting |
583 The first states that @{text p} must have at least an instruction for the starting |
653 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every |
584 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every |
901 |
832 |
902 \begin{center} |
833 \begin{center} |
903 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
834 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
904 \begin{tabular}[t]{@ {}l@ {}} |
835 \begin{tabular}[t]{@ {}l@ {}} |
905 \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm] |
836 \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\<equiv>"}\\[1mm] |
906 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
837 \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ |
907 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
838 \hspace{7mm}if @{term "P tp"} holds then\\ |
908 \hspace{7mm}@{text "\<exists>"} @{term n}. such that\\ |
839 \hspace{7mm}@{text "\<exists>"}@{term n}. such that\\ |
909 \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
840 \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\ |
910 \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} |
841 \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"} |
911 \end{tabular} & |
842 \end{tabular} & |
912 \begin{tabular}[t]{@ {}l@ {}} |
843 \begin{tabular}[t]{@ {}l@ {}} |
913 \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm] |
844 \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm] |
914 \hspace{5mm}@{text "\<forall>"} @{term "(l, r)"}.\\ |
845 \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ |
915 \hspace{7mm}if @{term "P (l, r)"} holds then\\ |
846 \hspace{7mm}if @{term "P tp"} holds then\\ |
916 \hspace{7mm}@{text "\<forall>"} @{term n}. @{text "\<not> is_final (steps (1, (l, r)) p n)"} |
847 \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"} |
917 \end{tabular} |
848 \end{tabular} |
918 \end{tabular} |
849 \end{tabular} |
919 \end{center} |
850 \end{center} |
920 |
851 |
921 \noindent |
852 \noindent |
1306 |
1237 |
1307 The main point of abacus programs is to be able to translate them to |
1238 The main point of abacus programs is to be able to translate them to |
1308 Turing machine programs. Registers and their content are represented by |
1239 Turing machine programs. Registers and their content are represented by |
1309 standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it |
1240 standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it |
1310 is impossible to build Turing machine programs out of components |
1241 is impossible to build Turing machine programs out of components |
1311 using our @{text "\<oplus>"}-operation shown in the previous section. |
1242 using our @{text ";"}-operation shown in the previous section. |
1312 To overcome this difficulty, we calculate a \emph{layout} of an |
1243 To overcome this difficulty, we calculate a \emph{layout} of an |
1313 abacus program as follows |
1244 abacus program as follows |
1314 |
1245 |
1315 \begin{center} |
1246 \begin{center} |
1316 \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
1247 \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
1463 function, written @{text UF}. This universal function acts like an interpreter for Turing machines. |
1394 function, written @{text UF}. This universal function acts like an interpreter for Turing machines. |
1464 It takes two arguments: one is the code of the Turing machine to be interpreted and the |
1395 It takes two arguments: one is the code of the Turing machine to be interpreted and the |
1465 other is the ``packed version'' of the arguments of the Turing machine. |
1396 other is the ``packed version'' of the arguments of the Turing machine. |
1466 We can then consider how this universal function is translated to a |
1397 We can then consider how this universal function is translated to a |
1467 Turing machine and from this construct the universal Turing machine, |
1398 Turing machine and from this construct the universal Turing machine, |
1468 written @{term UTM}. @{text UTM} is defined as |
1399 written @{term UTM}. It is defined as |
1469 the composition of the Turing machine that packages the arguments and |
1400 the composition of the Turing machine that packages the arguments and |
1470 the translated recursive |
1401 the translated recursive |
1471 function @{text UF}: |
1402 function @{text UF}: |
1472 |
1403 |
1473 \begin{center} |
1404 \begin{center} |
1474 @{text "UTM \<equiv> arg_coding \<oplus> (translate UF)"} |
1405 @{text "UTM \<equiv> arg_coding ; (translate UF)"} |
1475 \end{center} |
1406 \end{center} |
1476 |
1407 |
1477 \noindent |
1408 \noindent |
1478 Suppose |
1409 Suppose |
1479 a Turing program @{term p} is well-formed and when started with the standard |
1410 a Turing program @{term p} is well-formed and when started with the standard |
1654 computability because in Isabelle/HOL we cannot, for example, |
1585 computability because in Isabelle/HOL we cannot, for example, |
1655 represent the decidability of a predicate @{text P}, say, as the |
1586 represent the decidability of a predicate @{text P}, say, as the |
1656 formula @{term "P \<or> \<not>P"}. For reasoning about computability we need |
1587 formula @{term "P \<or> \<not>P"}. For reasoning about computability we need |
1657 to formalise a concrete model of computations. We could have |
1588 to formalise a concrete model of computations. We could have |
1658 followed Norrish \cite{Norrish11} using the $\lambda$-calculus as |
1589 followed Norrish \cite{Norrish11} using the $\lambda$-calculus as |
1659 the starting point for computability theory, but then we would have |
1590 the starting point for formalising computability theory, but then we would have |
1660 to reimplement on the ML-level his infrastructure for rewriting |
1591 to reimplement on the ML-level his infrastructure for rewriting |
1661 $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that |
1592 $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that |
1662 can rewrite terms modulo an arbitrary equivalence relation, which |
1593 can rewrite terms modulo an arbitrary equivalence relation, which |
1663 Isabelle unfortunately does not yet have. Even though we would |
1594 Isabelle unfortunately does not yet have. Even though, we would |
1664 still need to connect $\lambda$-terms somehow to Turing machines for |
1595 still need to connect $\lambda$-terms somehow to Turing machines for |
1665 proofs that make essential use of them (for example the |
1596 proofs that make essential use of them (for example the |
1666 undecidability proof for Wang's tiling problem \cite{Robinson71}). |
1597 undecidability proof for Wang's tiling problem \cite{Robinson71}). |
1667 |
1598 |
1668 We therefore have formalised Turing machines in the first place and the main |
1599 We therefore have formalised Turing machines in the first place and the main |