20 set ("") and |
20 set ("") and |
21 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
21 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
22 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
22 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
23 update2 ("update") and |
23 update2 ("update") and |
24 tm_wf0 ("wf") and |
24 tm_wf0 ("wf") and |
|
25 is_even ("iseven") and |
25 (* abc_lm_v ("lookup") and |
26 (* abc_lm_v ("lookup") and |
26 abc_lm_s ("set") and*) |
27 abc_lm_s ("set") and*) |
27 haltP ("stdhalt") and |
28 haltP ("stdhalt") and |
28 tcopy ("copy") and |
29 tcopy ("copy") and |
29 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
30 tape_of_nat_list ("\<ulcorner>_\<urcorner>") and |
30 tm_comp ("_ \<oplus> _") and |
31 tm_comp ("_ \<oplus> _") and |
31 DUMMY ("\<^raw:\mbox{$\_$}>") |
32 DUMMY ("\<^raw:\mbox{$\_$}>") |
32 |
33 |
33 declare [[show_question_marks = false]] |
34 declare [[show_question_marks = false]] |
|
35 |
|
36 (* THEOREMS *) |
|
37 notation (Rule output) |
|
38 "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
39 |
|
40 syntax (Rule output) |
|
41 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
42 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
43 |
|
44 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" |
|
45 ("\<^raw:\mbox{>_\<^raw:}\\>/ _") |
|
46 |
|
47 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
48 |
|
49 notation (Axiom output) |
|
50 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") |
|
51 |
|
52 notation (IfThen output) |
|
53 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
54 syntax (IfThen output) |
|
55 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
56 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
57 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
58 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
59 |
|
60 notation (IfThenNoBox output) |
|
61 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
62 syntax (IfThenNoBox output) |
|
63 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
64 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
65 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
66 "_asm" :: "prop \<Rightarrow> asms" ("_") |
|
67 |
|
68 |
|
69 |
34 (*>*) |
70 (*>*) |
35 |
71 |
36 section {* Introduction *} |
72 section {* Introduction *} |
37 |
73 |
38 |
74 |
50 %formalise in Isabelle/HOL computability arguments about the |
86 %formalise in Isabelle/HOL computability arguments about the |
51 %algorithms. |
87 %algorithms. |
52 |
88 |
53 |
89 |
54 \noindent |
90 \noindent |
55 Suppose you want to mechanise a proof about whether a predicate @{term P}, say, is |
91 Suppose you want to mechanise a proof for whether a predicate @{term P}, say, is |
56 decidable or not. Decidability of @{text P} usually amounts to showing |
92 decidable or not. Decidability of @{text P} usually amounts to showing |
57 whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work |
93 whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work |
58 in Isabelle/HOL and other HOL theorem provers, since they are based on classical logic |
94 in Isabelle/HOL and other HOL theorem provers, since they are based on classical logic |
59 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} |
95 where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}} |
60 is always provable no matter whether @{text P} is constructed by |
96 is always provable no matter whether @{text P} is constructed by |
61 computable means. |
97 computable means. We hit this limitation previously when we mechanised the correctness |
|
98 proofs of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, |
|
99 but were unable to formalise arguments about computability. |
62 |
100 |
63 %The same problem would arise if we had formulated |
101 %The same problem would arise if we had formulated |
64 %the algorithms as recursive functions, because internally in |
102 %the algorithms as recursive functions, because internally in |
65 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
103 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
66 %represented as inductively defined predicates too. |
104 %represented as inductively defined predicates too. |
181 prove the correctness of concrete Turing machines that are needed |
219 prove the correctness of concrete Turing machines that are needed |
182 in this proof; such correctness proofs are left out in the informal literature. |
220 in this proof; such correctness proofs are left out in the informal literature. |
183 We construct the universal Turing machine from \cite{Boolos87} by |
221 We construct the universal Turing machine from \cite{Boolos87} by |
184 relating recursive functions to abacus machines and abacus machines to |
222 relating recursive functions to abacus machines and abacus machines to |
185 Turing machines. Since we have set up in Isabelle/HOL a very general computability |
223 Turing machines. Since we have set up in Isabelle/HOL a very general computability |
186 model and undecidability result, we are able to formalise the |
224 model and undecidability result, we are able to formalise other |
187 undecidability of Wang's tiling problem. We are not aware of any other |
225 results: we describe a proof of the computational equivalence |
188 formalisation of a substantial undecidability problem. |
226 of single-sided Turing machines, which is not given in \cite{Boolos87}, |
|
227 but needed for formalising the undecidability proof of Wang's tiling problem. {\it citation} |
|
228 %We are not aware of any other |
|
229 %formalisation of a substantial undecidability problem. |
189 *} |
230 *} |
190 |
231 |
191 section {* Turing Machines *} |
232 section {* Turing Machines *} |
192 |
233 |
193 text {* \noindent |
234 text {* \noindent |
309 %possibly renaming states apart whenever both machines share |
350 %possibly renaming states apart whenever both machines share |
310 %states.\footnote{The usual disjoint union operation in Isabelle/HOL |
351 %states.\footnote{The usual disjoint union operation in Isabelle/HOL |
311 %cannot be used as it does not preserve types.} This renaming can be |
352 %cannot be used as it does not preserve types.} This renaming can be |
312 %quite cumbersome to reason about. |
353 %quite cumbersome to reason about. |
313 We followed the choice made in \cite{AspertiRicciotti12} |
354 We followed the choice made in \cite{AspertiRicciotti12} |
314 representing a state by a natural number and the states of a Turing |
355 representing a state by a natural number and the states in a Turing |
315 machine by the initial segment of natural numbers starting from @{text 0}. |
356 machine programme by the initial segment of natural numbers starting from @{text 0}. |
316 In doing so we can compose two Turing machine by |
357 In doing so we can compose two Turing machine programs by |
317 shifting the states of one by an appropriate amount to a higher |
358 shifting the states of one by an appropriate amount to a higher |
318 segment and adjusting some ``next states'' in the other. {\it composition here?} |
359 segment and adjusting some ``next states'' in the other. |
319 |
360 |
320 An \emph{instruction} of a Turing machine is a pair consisting of |
361 An \emph{instruction} of a Turing machine is a pair consisting of |
321 an action and a natural number (the next state). A \emph{program} @{term p} of a Turing |
362 an action and a natural number (the next state). A \emph{program} @{term p} of a Turing |
322 machine is then a list of such pairs. Using as an example the following Turing machine |
363 machine is then a list of such pairs. Using as an example the following Turing machine |
323 program, which consists of four instructions |
364 program, which consists of four instructions |
354 Given a program @{term p}, a state |
395 Given a program @{term p}, a state |
355 and the cell being read by the head, we need to fetch |
396 and the cell being read by the head, we need to fetch |
356 the corresponding instruction from the program. For this we define |
397 the corresponding instruction from the program. For this we define |
357 the function @{term fetch} |
398 the function @{term fetch} |
358 |
399 |
359 \begin{center} |
400 \begin{equation}\label{fetch} |
360 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
401 \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
361 \multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\ |
402 \multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\ |
362 @{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\ |
403 @{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\ |
363 \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\ |
404 \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\ |
364 @{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\ |
405 @{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\ |
365 \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}} |
406 \multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}} |
366 \end{tabular} |
407 \end{tabular}} |
367 \end{center} |
408 \end{equation} |
368 |
409 |
369 \noindent |
410 \noindent |
370 In this definition the function @{term nth_of} returns the @{text n}th element |
411 In this definition the function @{term nth_of} returns the @{text n}th element |
371 from a list, provided it exists (@{term Some}-case), or if it does not, it |
412 from a list, provided it exists (@{term Some}-case), or if it does not, it |
372 returns the default action @{term Nop} and the default state @{text 0} |
413 returns the default action @{term Nop} and the default state @{text 0} |
373 (@{term None}-case). In doing so we slightly deviate from the description |
414 (@{term None}-case). We often need to restrict Turing machine programs |
374 in \cite{Boolos87}: if their Turing machines transition to a non-existing |
415 to be well-formed: a program @{term p} is \emph{well-formed} if it |
375 state, then the computation is halted. We will transition in such cases |
416 satisfies the following three properties: |
376 to the @{text 0}-state.\footnote{\it However, with introducing the |
417 |
377 notion of \emph{well-formed} Turing machine programs we will later exclude such |
418 \begin{center} |
378 cases and make the @{text 0}-state the only ``halting state''. A program |
419 @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]} |
379 @{term p} is said to be well-formed if it satisfies |
|
380 the following three properties: |
|
381 |
|
382 \begin{center} |
|
383 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
384 @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\ |
|
385 & @{text "\<and>"} & @{term "iseven (length p)"}\\ |
|
386 & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"} |
|
387 \end{tabular} |
|
388 \end{center} |
420 \end{center} |
389 |
421 |
390 \noindent |
422 \noindent |
391 The first says that @{text p} must have at least an instruction for the starting |
423 The first says that @{text p} must have at least an instruction for the starting |
392 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every |
424 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every |
393 state, and the third that every next-state is one of the states mentioned in |
425 state, and the third that every next-state is one of the states mentioned in |
394 the program or being the @{text 0}-state. |
426 the program or being the @{text 0}-state. |
395 } |
|
396 |
427 |
397 A \emph{configuration} @{term c} of a Turing machine is a state together with |
428 A \emph{configuration} @{term c} of a Turing machine is a state together with |
398 a tape. This is written as @{text "(s, (l, r))"}. If we have a |
429 a tape. This is written as @{text "(s, (l, r))"}. If we have a |
399 configuration and a program, we can calculate |
430 configuration and a program, we can calculate |
400 what the next configuration is by fetching the appropriate action and next state |
431 what the next configuration is by fetching the appropriate action and next state |
423 @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\ |
454 @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\ |
424 \end{tabular} |
455 \end{tabular} |
425 \end{center} |
456 \end{center} |
426 |
457 |
427 \noindent |
458 \noindent |
428 Recall our definition of @{term fetch} with the default value for |
459 Recall our definition of @{term fetch} (shown in \ref{fetch}) with the default value for |
429 the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less |
460 the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less |
430 then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation |
461 then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation |
431 does not actually halt, but rather transitions to the @{text 0}-state and |
462 does not actually halt, but rather transitions to the @{text 0}-state and |
432 remains there performing @{text Nop}-actions until @{text n} is reached. |
463 remains there performing @{text Nop}-actions until @{text n} is reached. |
433 |
464 |
434 Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program |
|
435 @{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"} |
|
436 |
|
437 \begin{center} |
|
438 \begin{tabular}{l} |
|
439 @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\ |
|
440 \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"} |
|
441 \end{tabular} |
|
442 \end{center} |
|
443 |
|
444 \noindent |
|
445 where @{text 1} stands for the starting state and @{text 0} for our final state. |
|
446 A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff |
|
447 |
|
448 \begin{center} |
|
449 @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv> |
|
450 \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} |
|
451 \end{center} |
|
452 |
|
453 \noindent |
|
454 Later on we need to consider specific Turing machines that |
|
455 start with a tape in standard form and halt the computation |
|
456 in standard form. To define a tape in standard form, it is |
|
457 useful to have an operation %@{ term "tape_of_nat_list DUMMY"} |
|
458 that translates lists of natural numbers into tapes. |
|
459 |
|
460 |
|
461 \begin{center} |
|
462 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
463 %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\ |
|
464 %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\ |
|
465 %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\ |
|
466 \end{tabular} |
|
467 \end{center} |
|
468 |
|
469 |
|
470 |
|
471 |
|
472 By this we mean |
|
473 |
|
474 \begin{center} |
|
475 %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]} |
|
476 \end{center} |
|
477 |
|
478 \noindent |
|
479 This means the Turing machine starts with a tape containg @{text n} @{term Oc}s |
|
480 and the head pointing to the first one; the Turing machine |
|
481 halts with a tape consisting of some @{term Bk}s, followed by a |
|
482 ``cluster'' of @{term Oc}s and after that by some @{term Bk}s. |
|
483 The head in the output is pointing again at the first @{term Oc}. |
|
484 The intuitive meaning of this definition is to start the Turing machine with a |
|
485 tape corresponding to a value @{term n} and producing |
|
486 a new tape corresponding to the value @{term l} (the number of @{term Oc}s |
|
487 clustered on the output tape). |
|
488 |
|
489 Before we can prove the undecidability of the halting problem for Turing machines, |
465 Before we can prove the undecidability of the halting problem for Turing machines, |
490 we have to define how to compose two Turing machines. Given our setup, this is |
466 we have to define how to compose two Turing machine programs. Given our setup, this is |
491 relatively straightforward, if slightly fiddly. We use the following two |
467 relatively straightforward, if slightly fiddly. We use the following two |
492 auxiliary functions: |
468 auxiliary functions: |
493 |
469 |
494 \begin{center} |
470 \begin{center} |
495 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
471 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
499 \end{center} |
475 \end{center} |
500 |
476 |
501 \noindent |
477 \noindent |
502 The first adds @{text n} to all states, exept the @{text 0}-state, |
478 The first adds @{text n} to all states, exept the @{text 0}-state, |
503 thus moving all ``regular'' states to the segment starting at @{text |
479 thus moving all ``regular'' states to the segment starting at @{text |
504 n}; the second adds @{term "length p div 2 + 1"} to the @{text |
480 n}; the second adds @{term "Suc(length p div 2)"} to the @{text |
505 0}-state, thus ridirecting all references to the ``halting state'' |
481 0}-state, thus redirecting all references to the ``halting state'' |
506 to the first state after the program @{text p}. With these two |
482 to the first state after the program @{text p}. With these two |
507 functions in place, we can define the \emph{sequential composition} |
483 functions in place, we can define the \emph{sequential composition} |
508 of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} |
484 of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"} |
509 |
485 |
510 \begin{center} |
486 \begin{center} |
511 @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]} |
487 @{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]} |
512 \end{center} |
488 \end{center} |
513 |
489 |
514 \noindent |
490 \noindent |
515 This means @{text "p\<^isub>1"} is executed first. Whenever it originally |
491 %This means @{text "p\<^isub>1"} is executed first. Whenever it originally |
516 transitioned to the @{text 0}-state, it will in the composed program transition to the starting |
492 %transitioned to the @{text 0}-state, it will in the composed program transition to the starting |
517 state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"} |
493 %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"} |
518 have been shifted in order to make sure that the states of the composed |
494 %have been shifted in order to make sure that the states of the composed |
519 program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' |
495 %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy'' |
520 an initial segment of the natural numbers. |
496 %an initial segment of the natural numbers. |
|
497 |
|
498 In the following we will consider the following Turing machine program |
|
499 that makes a copies a value on the tape. |
|
500 |
|
501 \begin{figure} |
|
502 \begin{center} |
|
503 \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}} |
|
504 @{thm tcopy_init_def} & |
|
505 @{thm tcopy_loop_def} & |
|
506 @{thm tcopy_end_def} |
|
507 \end{tabular} |
|
508 \end{center} |
|
509 \end{figure} |
|
510 |
521 |
511 |
522 \begin{center} |
512 \begin{center} |
523 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}} |
513 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}} |
524 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
514 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
525 \end{tabular} |
515 \end{tabular} |
618 The most closely related work is by Norrish \cite{Norrish11}, and Asperti and |
608 The most closely related work is by Norrish \cite{Norrish11}, and Asperti and |
619 Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on |
609 Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on |
620 lambda-terms. For this he introduced a clever rewriting technology |
610 lambda-terms. For this he introduced a clever rewriting technology |
621 based on combinators and de-Bruijn indices for |
611 based on combinators and de-Bruijn indices for |
622 rewriting modulo $\beta$-equivalence (to keep it manageable) |
612 rewriting modulo $\beta$-equivalence (to keep it manageable) |
|
613 |
|
614 |
|
615 |
|
616 Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program |
|
617 @{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"} |
|
618 |
|
619 \begin{center} |
|
620 \begin{tabular}{l} |
|
621 @{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\ |
|
622 \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"} |
|
623 \end{tabular} |
|
624 \end{center} |
|
625 |
|
626 \noindent |
|
627 where @{text 1} stands for the starting state and @{text 0} for our final state. |
|
628 A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff |
|
629 |
|
630 \begin{center} |
|
631 @{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv> |
|
632 \<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} |
|
633 \end{center} |
|
634 |
|
635 \noindent |
|
636 Later on we need to consider specific Turing machines that |
|
637 start with a tape in standard form and halt the computation |
|
638 in standard form. To define a tape in standard form, it is |
|
639 useful to have an operation %@{ term "tape_of_nat_list DUMMY"} |
|
640 that translates lists of natural numbers into tapes. |
|
641 |
|
642 |
|
643 \begin{center} |
|
644 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
645 %@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\ |
|
646 %@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\ |
|
647 %@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\ |
|
648 \end{tabular} |
|
649 \end{center} |
|
650 |
|
651 |
|
652 By this we mean |
|
653 |
|
654 \begin{center} |
|
655 %@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]} |
|
656 \end{center} |
|
657 |
|
658 \noindent |
|
659 This means the Turing machine starts with a tape containg @{text n} @{term Oc}s |
|
660 and the head pointing to the first one; the Turing machine |
|
661 halts with a tape consisting of some @{term Bk}s, followed by a |
|
662 ``cluster'' of @{term Oc}s and after that by some @{term Bk}s. |
|
663 The head in the output is pointing again at the first @{term Oc}. |
|
664 The intuitive meaning of this definition is to start the Turing machine with a |
|
665 tape corresponding to a value @{term n} and producing |
|
666 a new tape corresponding to the value @{term l} (the number of @{term Oc}s |
|
667 clustered on the output tape). |
|
668 |
623 *} |
669 *} |
624 |
670 |
625 |
671 |
626 (* |
672 (* |
627 Questions: |
673 Questions: |