32 abc_lm_s ("set") and*) |
32 abc_lm_s ("set") and*) |
33 haltP ("stdhalt") and |
33 haltP ("stdhalt") and |
34 tcopy ("copy") and |
34 tcopy ("copy") and |
35 tape_of ("\<langle>_\<rangle>") and |
35 tape_of ("\<langle>_\<rangle>") and |
36 tm_comp ("_ \<oplus> _") and |
36 tm_comp ("_ \<oplus> _") and |
37 DUMMY ("\<^raw:\mbox{$\_$}>") |
37 DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") |
38 |
38 |
39 declare [[show_question_marks = false]] |
39 declare [[show_question_marks = false]] |
40 |
40 |
41 (* THEOREMS *) |
41 (* THEOREMS *) |
42 notation (Rule output) |
42 notation (Rule output) |
520 case a Turing program takes according to the usual textbook |
521 case a Turing program takes according to the usual textbook |
521 definition \cite{Boolos87} less than @{text n} steps before it |
522 definition \cite{Boolos87} less than @{text n} steps before it |
522 halts, then in our setting the @{term steps}-evaluation does not |
523 halts, then in our setting the @{term steps}-evaluation does not |
523 actually halt, but rather transitions to the @{text 0}-state (the |
524 actually halt, but rather transitions to the @{text 0}-state (the |
524 final state) and remains there performing @{text Nop}-actions until |
525 final state) and remains there performing @{text Nop}-actions until |
525 @{text n} is reached. This is different from the setup in |
526 @{text n} is reached. |
526 \cite{AspertiRicciotti12} where an option is returned once a final |
|
527 state is reached. |
|
528 |
527 |
529 \begin{figure}[t] |
528 \begin{figure}[t] |
530 \begin{center} |
529 \begin{center} |
531 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
530 \begin{tabular}{@ {}c@ {\hspace{3mm}}c@ {\hspace{3mm}}c} |
532 \begin{tabular}[t]{@ {}l@ {}} |
531 \begin{tabular}[t]{@ {}l@ {}} |
666 ``doing what they are supposed to be doing''. Such correctness proofs are usually left |
665 ``doing what they are supposed to be doing''. Such correctness proofs are usually left |
667 out in the informal literature, for example \cite{Boolos87}. One program |
666 out in the informal literature, for example \cite{Boolos87}. One program |
668 we need to prove correct is the @{term dither} program shown in \eqref{dither} |
667 we need to prove correct is the @{term dither} program shown in \eqref{dither} |
669 and the other program is @{term "tcopy"} defined as |
668 and the other program is @{term "tcopy"} defined as |
670 |
669 |
671 \begin{center} |
670 \begin{equation} |
672 \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
671 \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} |
673 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
672 @{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def} |
674 \end{tabular} |
673 \end{tabular}}\label{tcopy} |
675 \end{center} |
674 \end{equation} |
676 |
675 |
677 \noindent |
676 \noindent |
678 whose three components are given in Figure~\ref{copy}. To the prove |
677 whose three components are given in Figure~\ref{copy}. To the prove |
679 correctness of these Turing machine programs, we introduce the |
678 correctness of these Turing machine programs, we introduce the |
680 notion of total correctness defined in terms of |
679 notion of total correctness defined in terms of |
774 \raisebox{2mm}{loops} |
773 \raisebox{2mm}{loops} |
775 \end{tabular} |
774 \end{tabular} |
776 \end{center} |
775 \end{center} |
777 |
776 |
778 \noindent |
777 \noindent |
779 We can prove the following formal statements |
778 We can prove the following Hoare-statements: |
780 |
779 |
781 \begin{center} |
780 \begin{center} |
782 \begin{tabular}{l} |
781 \begin{tabular}{l} |
783 @{thm dither_halts}\\ |
782 @{thm dither_halts}\\ |
784 @{thm dither_loops} |
783 @{thm dither_loops} |
785 \end{tabular} |
784 \end{tabular} |
786 \end{center} |
785 \end{center} |
787 |
786 |
788 \noindent |
787 \noindent |
789 {\it unfold} The first states that on a tape @{term "(Bk \<up> n, [Oc, Oc])"} |
788 The first is by a simple calculation. The second is by induction on the |
790 halts in tree steps leaving the tape unchanged. In the other states |
789 number of steps we can perform starting from the input tape. |
791 that @{term dither} started with tape @{term "(Bk \<up> n, [Oc])"} loops. |
790 |
792 |
791 The purpose of the @{term tcopy} program defined in \eqref{tcopy} is |
793 |
792 to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when |
794 |
793 started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of |
795 In the following we will consider the following Turing machine program |
794 a value on the tape. Reasoning about this program is substantially |
796 that makes a copies a value on the tape. |
795 harder than about @{term dither}. To ease the burden, we can prove |
797 |
796 the following Hoare-rules for sequentially composed programs. |
798 |
797 |
799 |
798 \begin{center} |
800 |
799 \begin{tabular}{@ {}p{3cm}@ {\hspace{9mm}}p{3cm}@ {}} |
801 |
|
802 |
|
803 |
|
804 assertion holds for all tapes |
|
805 |
|
806 Hoare rule for composition |
|
807 |
|
808 For showing the undecidability of the halting problem, we need to consider |
|
809 two specific Turing machines. copying TM and dithering TM |
|
810 |
|
811 correctness of the copying TM |
|
812 |
|
813 measure for the copying TM, which we however omit. |
|
814 |
|
815 halting problem |
|
816 *} |
|
817 |
|
818 text {* |
|
819 \begin{center} |
|
820 \begin{tabular}{@ {}p{3cm}p{3cm}@ {}} |
|
821 @{thm[mode=Rule] |
800 @{thm[mode=Rule] |
822 Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]} |
801 Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]} |
823 & |
802 & |
824 @{thm[mode=Rule] |
803 @{thm[mode=Rule] |
825 Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]} |
804 Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]} |
826 \end{tabular} |
805 \end{tabular} |
827 \end{center} |
806 \end{center} |
828 |
807 |
829 |
808 \noindent |
|
809 The first corresponds to the usual Hoare-rule for composition of imperative |
|
810 programs, where @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for |
|
811 all tapes @{term "(l, r)"}. The second rule covers the case where rughly the |
|
812 first program terminates generating a tape for which the second program |
|
813 loops. These are two cases we need in our proof for undecidability. |
|
814 |
|
815 The Hoare-rules above allow us to prove the correctness of @{term tcopy} |
|
816 by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"} |
|
817 and @{term "tcopy_end"} in isolation. We will show some details for the |
|
818 the program @{term "tcopy_begin"}. |
|
819 |
|
820 |
|
821 assertion holds for all tapes |
|
822 |
|
823 Hoare rule for composition |
|
824 |
|
825 For showing the undecidability of the halting problem, we need to consider |
|
826 two specific Turing machines. copying TM and dithering TM |
|
827 |
|
828 correctness of the copying TM |
|
829 |
|
830 measure for the copying TM, which we however omit. |
|
831 |
|
832 halting problem |
|
833 |
|
834 Magnus: invariants -- Section 5.4.5 on page 75. |
830 *} |
835 *} |
|
836 |
831 |
837 |
832 section {* Abacus Machines *} |
838 section {* Abacus Machines *} |
833 |
839 |
834 text {* |
840 text {* |
835 \noindent |
841 \noindent |