926 @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\ |
926 @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\ |
927 @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ |
927 @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ |
928 \hline |
928 \hline |
929 \end{tabular} |
929 \end{tabular} |
930 \end{center} |
930 \end{center} |
931 \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} for the states of |
931 \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} are for the states of |
932 @{term tcopy_begin}. Below, the invariants for the starting and halting states of |
932 @{term tcopy_begin}. Below, the invariants only for the starting and halting states of |
933 @{term tcopy_loop} and @{term tcopy_end}. In each invariant the parameter @{term n} stands for the number |
933 @{term tcopy_loop} and @{term tcopy_end} are shown. In each invariant the parameter |
|
934 @{term n} stands for the number |
934 of @{term Oc}s with which the Turing machine is started.}\label{invbegin} |
935 of @{term Oc}s with which the Turing machine is started.}\label{invbegin} |
935 \end{figure} |
936 \end{figure} |
936 |
937 |
937 \begin{center} |
938 \begin{center} |
938 \begin{tabular}{rcl} |
939 \begin{tabular}{rcl} |
954 @{term step} and @{term steps}. This gives us partial correctness |
955 @{term step} and @{term steps}. This gives us partial correctness |
955 for @{term "tcopy_begin"}. |
956 for @{term "tcopy_begin"}. |
956 |
957 |
957 We next need to show that @{term "tcopy_begin"} terminates. For this |
958 We next need to show that @{term "tcopy_begin"} terminates. For this |
958 we introduce lexicographically ordered pairs @{term "(n, m)"} |
959 we introduce lexicographically ordered pairs @{term "(n, m)"} |
959 derived from configurations @{text "(s, (l, r))"}: @{text n} stands |
960 derived from configurations @{text "(s, (l, r))"}: @{text n} is |
960 for the state ordered according to how @{term tcopy_begin} executes |
961 the state @{text s}, but ordered according to how @{term tcopy_begin} executes |
961 them, that is @{text "1 > 2 > 3 > 4 > 0"}; @{term m} is calculated |
962 them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have |
962 according to the measure function: |
963 a strictly decreasing meansure, @{term m} takes the data on the tape into |
|
964 account and is calculated according to the measure function: |
963 |
965 |
964 \begin{center} |
966 \begin{center} |
965 \begin{tabular}{rcl} |
967 \begin{tabular}{rcl} |
966 @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & |
968 @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & |
967 @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\ |
969 @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\ |
968 & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} @{thm (rhs) measure_begin_print(2)} \\ |
970 & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} |
|
971 @{text "("}@{thm (rhs) measure_begin_print(2)}@{text ")"} \\ |
969 & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\ |
972 & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\ |
970 & & @{text else} @{thm (rhs) measure_begin_print(4)}\\ |
973 & & @{text else} @{thm (rhs) measure_begin_print(4)}\\ |
971 \end{tabular} |
974 \end{tabular} |
972 \end{center} |
975 \end{center} |
973 |
976 |
974 \noindent |
977 \noindent |
975 With this in place, we can show that for every starting tape of the |
978 With this in place, we can show that for every starting tape of the |
976 form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing |
979 form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing |
977 machine @{term "tcopy_begin"} will halt. Taking this and the partial |
980 machine @{term "tcopy_begin"} will eventually halt. Taking this and the partial |
978 correctness proof together we obtain for @{term tcopy_begin} (similar |
981 correctness proof together, we obtain for @{term tcopy_begin} the Hoare-triple |
979 resoning is needed for @{term tcopy_loop} and @{term tcopy_end}): |
982 (similar resoning is needed for @{term tcopy_loop} and @{term tcopy_end}): |
980 |
983 |
981 |
984 |
982 \begin{center} |
985 \begin{center} |
983 @{thm (concl) begin_correct}\hspace{6mm} |
986 @{thm (concl) begin_correct}\hspace{6mm} |
984 @{thm (concl) loop_correct}\hspace{6mm} |
987 @{thm (concl) loop_correct}\hspace{6mm} |
985 @{thm (concl) end_correct} |
988 @{thm (concl) end_correct} |
986 \end{center} |
989 \end{center} |
987 |
990 |
988 \noindent |
991 \noindent |
989 where we assume @{text "0 < n"}. Since @{term "inv_begin0 n \<mapsto> inv_loop1 n"} holds |
992 where we assume @{text "0 < n"}. Since the invariant of the halting |
990 and @{term "inv_loop0 n = inv_end1 n"}, we can derive using our Hoare-rules |
993 state of @{term tcopy_begin} implies the invariant of the starting |
991 the correctness of @{term tcopy} |
994 state of @{term tcopy_loop}, that is @{term "inv_begin0 n \<mapsto> |
|
995 inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1 n"}, we |
|
996 can derive using our Hoare-rules for sequentially composed Turing programs |
|
997 the correctness of @{term tcopy}: |
992 |
998 |
993 \begin{center} |
999 \begin{center} |
994 @{thm tcopy_correct} |
1000 @{thm tcopy_correct} |
995 \end{center} |
1001 \end{center} |
996 |
1002 |
1002 \begin{center} |
1008 \begin{center} |
1003 @{thm haltP_def} |
1009 @{thm haltP_def} |
1004 \end{center} |
1010 \end{center} |
1005 |
1011 |
1006 \noindent |
1012 \noindent |
1007 This means we considering only Turing machine programs representing functions that take |
1013 This means we considering only Turing machine programs representing |
1008 some numbers as input and produce a single number as output. There is no Turing |
1014 functions that take some numbers as input and produce a single |
1009 machine that can decide the halting problem (answer @{text 0} for halting and |
1015 number as output. The undecidability problem states that there is no |
1010 @{text 1} for looping). Given our correctness proofs for @{term dither} and @{term tcopy} |
1016 Turing machine that can decide the halting problem (answer eith |
1011 this non-existence is relatively straightforward to establish. We first assume there is a coding |
1017 @{text 0} for halting and @{text 1} for looping). Given our |
1012 function, written @{term code}, from Turing machine programs to natural numbers. |
1018 correctness proofs for @{term dither} and @{term tcopy} shown above, |
1013 Suppose a Turing machine @{term H} exists such that if started with the standard |
1019 this non-existence is relatively straightforward to establish. We |
1014 tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0} or @{text 1} depending |
1020 first assume there is a coding function, written @{term "code M"}, which |
1015 on whether @{text M} halts when started with the input tape containing @{term "<ns>"}. |
1021 represents a Turing machine @{term "M"} as a natural number. No further |
1016 This is formalised as follows |
1022 assumptions are made about this coding function. Suppose a Turing |
1017 |
1023 machine @{term H} exists such that if started with the standard tape |
|
1024 @{term "([Bk], <(code M, ns)>)"} returns @{text 0}, respectively @{text 1}, |
|
1025 depending on whether @{text M} halts when started with the input |
|
1026 tape containing @{term "<ns>"}. This assumption is formalised as |
|
1027 follows---for all @{term M} and natural numbers @{term ns}: |
|
1028 |
1018 \begin{center} |
1029 \begin{center} |
1019 \begin{tabular}{r} |
1030 \begin{tabular}{r} |
1020 @{thm (prem 2) uncomputable.h_case} implies |
1031 @{thm (prem 2) uncomputable.h_case} implies |
1021 @{thm (concl) uncomputable.h_case}\\ |
1032 @{thm (concl) uncomputable.h_case}\\ |
1022 |
1033 |