5 |
5 |
6 (* |
6 (* |
7 hide_const (open) s |
7 hide_const (open) s |
8 *) |
8 *) |
9 |
9 |
|
10 |
10 hide_const (open) Divides.adjust |
11 hide_const (open) Divides.adjust |
11 |
12 |
12 abbreviation |
13 abbreviation |
13 "update2 p a \<equiv> update a p" |
14 "update2 p a \<equiv> update a p" |
14 |
15 |
15 consts DUMMY::'a |
16 consts DUMMY::'a |
|
17 |
|
18 |
|
19 (* THEOREMS *) |
|
20 notation (Rule output) |
|
21 "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
22 |
|
23 syntax (Rule output) |
|
24 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
25 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
26 |
|
27 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" |
|
28 ("\<^raw:\mbox{>_\<^raw:}\\>/ _") |
|
29 |
|
30 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
31 |
|
32 notation (Axiom output) |
|
33 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") |
|
34 |
|
35 notation (IfThen output) |
|
36 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
37 syntax (IfThen output) |
|
38 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
39 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
40 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
41 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
42 |
|
43 notation (IfThenNoBox output) |
|
44 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
45 syntax (IfThenNoBox output) |
|
46 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
47 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
48 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
49 "_asm" :: "prop \<Rightarrow> asms" ("_") |
|
50 |
|
51 |
|
52 context uncomputable |
|
53 begin |
16 |
54 |
17 notation (latex output) |
55 notation (latex output) |
18 Cons ("_::_" [48,47] 48) and |
56 Cons ("_::_" [48,47] 48) and |
19 set ("") and |
57 set ("") and |
20 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
58 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
24 (*is_even ("iseven") and*) |
62 (*is_even ("iseven") and*) |
25 tcopy_begin ("cbegin") and |
63 tcopy_begin ("cbegin") and |
26 tcopy_loop ("cloop") and |
64 tcopy_loop ("cloop") and |
27 tcopy_end ("cend") and |
65 tcopy_end ("cend") and |
28 step0 ("step") and |
66 step0 ("step") and |
29 uncomputable.tcontra ("tcontra") and |
67 tcontra ("contra") and |
|
68 code_tcontra ("code contra") and |
30 steps0 ("steps") and |
69 steps0 ("steps") and |
31 exponent ("_\<^bsup>_\<^esup>") and |
70 exponent ("_\<^bsup>_\<^esup>") and |
32 haltP ("halts") and |
71 haltP ("halts") and |
33 tcopy ("copy") and |
72 tcopy ("copy") and |
34 tape_of ("\<langle>_\<rangle>") and |
73 tape_of ("\<langle>_\<rangle>") and |
81 "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0" |
120 "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0" |
82 by (simp_all) |
121 by (simp_all) |
83 |
122 |
84 declare [[show_question_marks = false]] |
123 declare [[show_question_marks = false]] |
85 |
124 |
86 (* THEOREMS *) |
|
87 notation (Rule output) |
|
88 "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
89 |
|
90 syntax (Rule output) |
|
91 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
92 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") |
|
93 |
|
94 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" |
|
95 ("\<^raw:\mbox{>_\<^raw:}\\>/ _") |
|
96 |
|
97 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
98 |
|
99 notation (Axiom output) |
|
100 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") |
|
101 |
|
102 notation (IfThen output) |
|
103 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
104 syntax (IfThen output) |
|
105 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
106 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
107 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
108 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
|
109 |
|
110 notation (IfThenNoBox output) |
|
111 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
112 syntax (IfThenNoBox output) |
|
113 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
114 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
|
115 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
|
116 "_asm" :: "prop \<Rightarrow> asms" ("_") |
|
117 |
|
118 lemma nats2tape: |
125 lemma nats2tape: |
119 shows "<([]::nat list)> = []" |
126 shows "<([]::nat list)> = []" |
120 and "<[n]> = <n>" |
127 and "<[n]> = <n>" |
121 and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>" |
128 and "ns \<noteq> [] \<Longrightarrow> <n#ns> = <(n::nat, ns)>" |
122 and "<(n, m)> = <n> @ [Bk] @ <m>" |
129 and "<(n, m)> = <n> @ [Bk] @ <m>" |
171 since they are based on classical logic where the law of excluded |
179 since they are based on classical logic where the law of excluded |
172 middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no |
180 middle ensures that \mbox{@{term "P \<or> \<not>P"}} is always provable no |
173 matter whether @{text P} is constructed by computable means. We hit on |
181 matter whether @{text P} is constructed by computable means. We hit on |
174 this limitation previously when we mechanised the correctness proofs |
182 this limitation previously when we mechanised the correctness proofs |
175 of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but |
183 of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but |
176 were unable to formalise arguments about decidability. |
184 were unable to formalise arguments about decidability or undecidability. |
177 |
185 |
178 %The same problem would arise if we had formulated |
186 %The same problem would arise if we had formulated |
179 %the algorithms as recursive functions, because internally in |
187 %the algorithms as recursive functions, because internally in |
180 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
188 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
181 %represented as inductively defined predicates too. |
189 %represented as inductively defined predicates too. |
581 \end{center} |
589 \end{center} |
582 |
590 |
583 \noindent Recall our definition of @{term fetch} (shown in |
591 \noindent Recall our definition of @{term fetch} (shown in |
584 \eqref{fetch}) with the default value for the @{text 0}-state. In |
592 \eqref{fetch}) with the default value for the @{text 0}-state. In |
585 case a Turing program takes according to the usual textbook |
593 case a Turing program takes according to the usual textbook |
586 definition \cite{Boolos87} less than @{text n} steps before it |
594 definition, say \cite{Boolos87}, less than @{text n} steps before it |
587 halts, then in our setting the @{term steps}-evaluation does not |
595 halts, then in our setting the @{term steps}-evaluation does not |
588 actually halt, but rather transitions to the @{text 0}-state (the |
596 actually halt, but rather transitions to the @{text 0}-state (the |
589 final state) and remains there performing @{text Nop}-actions until |
597 final state) and remains there performing @{text Nop}-actions until |
590 @{text n} is reached. |
598 @{text n} is reached. |
591 |
599 |
784 \end{equation} |
792 \end{equation} |
785 |
793 |
786 \noindent |
794 \noindent |
787 where |
795 where |
788 @{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"}, |
796 @{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"}, |
789 @{term "P' tp"} implies @{term "P tp"}. |
797 @{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}). |
790 |
798 |
791 Like Asperti and Ricciotti with their notion of realisability, we |
799 Like Asperti and Ricciotti with their notion of realisability, we |
792 have set up our Hoare-rules so that we can deal explicitly |
800 have set up our Hoare-rules so that we can deal explicitly |
793 with total correctness and non-terminantion, rather than have |
801 with total correctness and non-terminantion, rather than have |
794 notions for partial correctness and termination. Although the latter |
802 notions for partial correctness and termination. Although the latter |
992 @{thm (concl) end_correct} |
1000 @{thm (concl) end_correct} |
993 \end{center} |
1001 \end{center} |
994 |
1002 |
995 \noindent |
1003 \noindent |
996 where we assume @{text "0 < n"} (similar resoning is needed for |
1004 where we assume @{text "0 < n"} (similar resoning is needed for |
997 @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of |
1005 the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of |
998 the halting state of @{term tcopy_begin} implies the invariant of |
1006 the halting state of @{term tcopy_begin} implies the invariant of |
999 the starting state of @{term tcopy_loop}, that is @{term "inv_begin0 |
1007 the starting state of @{term tcopy_loop}, that is @{term "inv_begin0 |
1000 n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1 |
1008 n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1 |
1001 n"}, we can derive using our Hoare-rules for the correctness |
1009 n"}, we can derive the following Hoare-triple for the correctness |
1002 of @{term tcopy}: |
1010 of @{term tcopy}: |
1003 |
1011 |
1004 \begin{center} |
1012 \begin{center} |
1005 @{thm tcopy_correct} |
1013 @{thm tcopy_correct} |
1006 \end{center} |
1014 \end{center} |
1007 |
1015 |
1008 \noindent |
1016 \noindent |
1009 That means if we start with a tape of the form @{term "([], <n::nat>)"} then |
1017 That means if we start with a tape of the form @{term "([], <n::nat>)"} then |
1010 @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}. |
1018 @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}, as desired. |
1011 |
1019 |
1012 Finally, we are in the position to prove the undecidability of the halting problem. |
1020 Finally, we are in the position to prove the undecidability of the halting problem. |
1013 A program @{term p} started with a standard tape containing the (encoded) numbers |
1021 A program @{term p} started with a standard tape containing the (encoded) numbers |
1014 @{term ns} will \emph{halt} with a standard tape containging a single (encoded) |
1022 @{term ns} will \emph{halt} with a standard tape containging a single (encoded) |
1015 number is defined as |
1023 number is defined as |
1024 single number as output. For undecidability, the property we are |
1032 single number as output. For undecidability, the property we are |
1025 proving is that there is no Turing machine that can decide in |
1033 proving is that there is no Turing machine that can decide in |
1026 general whether a Turing machine program halts (answer either @{text |
1034 general whether a Turing machine program halts (answer either @{text |
1027 0} for halting and @{text 1} for looping). Given our correctness |
1035 0} for halting and @{text 1} for looping). Given our correctness |
1028 proofs for @{term dither} and @{term tcopy} shown above, this |
1036 proofs for @{term dither} and @{term tcopy} shown above, this |
1029 non-existence is relatively straightforward to establish. We first |
1037 non-existence is now relatively straightforward to establish. We first |
1030 assume there is a coding function, written @{term "code M"}, which |
1038 assume there is a coding function, written @{term "code M"}, which |
1031 represents a Turing machine @{term "M"} as a natural number. No |
1039 represents a Turing machine @{term "M"} as a natural number. No |
1032 further assumptions are made about this coding function. Suppose a |
1040 further assumptions are made about this coding function. Suppose a |
1033 Turing machine @{term H} exists such that if started with the |
1041 Turing machine @{term H} exists such that if started with the |
1034 standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0}, |
1042 standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0}, |
1035 respectively @{text 1}, depending on whether @{text M} halts when |
1043 respectively @{text 1}, depending on whether @{text M} halts when |
1036 started with the input tape containing @{term "<ns>"}. This |
1044 started with the input tape containing @{term "<ns>"}. This |
1037 assumption is formalised as follows---for all @{term M} and natural |
1045 assumption is formalised as follows---for all @{term M} and all lists of |
1038 numbers @{term ns}: |
1046 natural numbers @{term ns}: |
1039 |
1047 |
1040 \begin{center} |
1048 \begin{center} |
1041 \begin{tabular}{r} |
1049 \begin{tabular}{r} |
1042 @{thm (prem 2) uncomputable.h_case} implies |
1050 @{thm (prem 2) uncomputable.h_case} implies |
1043 @{thm (concl) uncomputable.h_case}\\ |
1051 @{thm (concl) uncomputable.h_case}\\ |
1049 |
1057 |
1050 \noindent |
1058 \noindent |
1051 The contradiction can be derived using the following Turing machine |
1059 The contradiction can be derived using the following Turing machine |
1052 |
1060 |
1053 \begin{center} |
1061 \begin{center} |
1054 @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"} |
1062 @{thm tcontra_def} |
1055 \end{center} |
1063 \end{center} |
1056 |
1064 |
1057 \noindent |
1065 \noindent |
1058 Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"} |
1066 Suppose @{thm (prem 1) "tcontra_halt"}. Given the invariants on the |
1059 Proof |
1067 left, we can derive the following Hoare-pair for @{term tcontra} on the right. |
1060 |
1068 |
1061 \begin{center} |
1069 \begin{center}\small |
1062 $\inferrule*{ |
1070 \begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}} |
|
1071 \begin{tabular}[t]{@ {}l@ {}} |
|
1072 @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
|
1073 @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
|
1074 @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"} |
|
1075 \end{tabular} |
|
1076 & |
|
1077 \begin{tabular}[b]{@ {}l@ {}} |
|
1078 \raisebox{-20mm}{$\inferrule*{ |
1063 \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}} |
1079 \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}} |
1064 {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}} |
1080 {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}} |
1065 \\ @{term "{P\<^isub>3} dither {P\<^isub>3}"} |
1081 \\ @{term "{P\<^isub>3} dither \<up>"} |
1066 } |
|
1067 {@{term "{P\<^isub>1} tcontra {P\<^isub>3}"}} |
|
1068 $ |
|
1069 \end{center} |
|
1070 |
|
1071 \begin{center} |
|
1072 $\inferrule*{ |
|
1073 \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {Q\<^isub>3}"}} |
|
1074 {@{term "{P\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}} |
|
1075 \\ @{term "{Q\<^isub>3} dither \<up>"} |
|
1076 } |
1082 } |
1077 {@{term "{P\<^isub>1} tcontra \<up>"}} |
1083 {@{term "{P\<^isub>1} tcontra \<up>"}} |
1078 $ |
1084 $} |
1079 \end{center} |
1085 \end{tabular} |
1080 |
1086 \end{tabular} |
1081 Magnus: invariants -- Section 5.4.5 on page 75. |
1087 \end{center} |
|
1088 |
|
1089 \noindent |
|
1090 This Hoare-pair contradicts our assumption that @{term tcontra} started |
|
1091 with @{term "<(code tcontra)>"} halts. |
|
1092 |
|
1093 Suppose @{thm (prem 1) "tcontra_unhalt"}. Again given the invariants on the |
|
1094 left, we can derive the Hoare-triple for @{term tcontra} on the right. |
|
1095 |
|
1096 \begin{center}\small |
|
1097 \begin{tabular}{@ {}c@ {\hspace{-17mm}}c@ {}} |
|
1098 \begin{tabular}[t]{@ {}l@ {}} |
|
1099 @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\ |
|
1100 @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\ |
|
1101 @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"} |
|
1102 \end{tabular} |
|
1103 & |
|
1104 \begin{tabular}[t]{@ {}l@ {}} |
|
1105 \raisebox{-20mm}{$\inferrule*{ |
|
1106 \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}} |
|
1107 {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}} |
|
1108 \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"} |
|
1109 } |
|
1110 {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}} |
|
1111 $} |
|
1112 \end{tabular} |
|
1113 \end{tabular} |
|
1114 \end{center} |
|
1115 |
|
1116 \noindent |
|
1117 This time the Hoare-triple states that @{term tcontra} terminates |
|
1118 with the ``output'' @{term "<(1::nat)>"}. In both case we come |
|
1119 to an contradiction, which means we have to abondon our assumption |
|
1120 that there exists a Turing machine @{term H} which can decide |
|
1121 whether Turing machines terminate. |
|
1122 |
|
1123 |
|
1124 |
1082 *} |
1125 *} |
1083 |
1126 |
1084 |
1127 |
1085 section {* Abacus Machines *} |
1128 section {* Abacus Machines *} |
1086 |
1129 |