895 The first corresponds to the usual Hoare-rule for composition of two |
895 The first corresponds to the usual Hoare-rule for composition of two |
896 terminating programs. The second rule gives the conditions for when |
896 terminating programs. The second rule gives the conditions for when |
897 the first program terminates generating a tape for which the second |
897 the first program terminates generating a tape for which the second |
898 program loops. The side-conditions about @{thm (prem 3) HR2} are |
898 program loops. The side-conditions about @{thm (prem 3) HR2} are |
899 needed in order to ensure that the redirection of the halting and |
899 needed in order to ensure that the redirection of the halting and |
900 initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly. |
900 initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"}, respectively, match |
901 |
901 up correctly. These Hoare-rules allow us to prove the correctness |
902 The Hoare-rules allow us to prove the correctness of @{term |
902 of @{term tcopy} by considering the correctness of the components |
903 tcopy} by considering the correctness of the components @{term |
903 @{term "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} |
904 "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in |
904 in isolation. This simplifies the reasoning considerably, for |
905 isolation. We will show the details for the program @{term |
905 example when designing decreasing measures for proving the termination |
906 "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots, |
906 of the programs. We will show the details for the program @{term |
907 @{term "inv_begin4"} shown in Figure~\ref{invbegin}, which correspond to |
907 "tcopy_begin"}. For the two other programs we refer the reader to |
908 each state of @{term tcopy_begin}, we define the |
908 our formalisation. |
|
909 |
|
910 Given the invariants @{term "inv_begin0"},\ldots, |
|
911 @{term "inv_begin4"} shown in Figure~\ref{invbegin}, which |
|
912 correspond to each state of @{term tcopy_begin}, we define the |
909 following invariant for the whole @{term tcopy_begin} program: |
913 following invariant for the whole @{term tcopy_begin} program: |
910 |
914 |
911 \begin{figure}[t] |
915 \begin{figure}[t] |
912 \begin{center} |
916 \begin{center} |
913 \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}} |
917 \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}} |
959 we introduce lexicographically ordered pairs @{term "(n, m)"} |
963 we introduce lexicographically ordered pairs @{term "(n, m)"} |
960 derived from configurations @{text "(s, (l, r))"}: @{text n} is |
964 derived from configurations @{text "(s, (l, r))"}: @{text n} is |
961 the state @{text s}, but ordered according to how @{term tcopy_begin} executes |
965 the state @{text s}, but ordered according to how @{term tcopy_begin} executes |
962 them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have |
966 them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have |
963 a strictly decreasing meansure, @{term m} takes the data on the tape into |
967 a strictly decreasing meansure, @{term m} takes the data on the tape into |
964 account and is calculated according to the measure function: |
968 account and is calculated according to the following measure function: |
965 |
969 |
966 \begin{center} |
970 \begin{center} |
967 \begin{tabular}{rcl} |
971 \begin{tabular}{rcl} |
968 @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & |
972 @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\<equiv>"} & |
969 @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\ |
973 @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\ |
975 \end{center} |
979 \end{center} |
976 |
980 |
977 \noindent |
981 \noindent |
978 With this in place, we can show that for every starting tape of the |
982 With this in place, we can show that for every starting tape of the |
979 form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing |
983 form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing |
980 machine @{term "tcopy_begin"} will eventually halt. Taking this and the partial |
984 machine @{term "tcopy_begin"} will eventually halt (the measure |
981 correctness proof together, we obtain for @{term tcopy_begin} the Hoare-triple |
985 decreases in each step). Taking this and the partial correctness |
982 (similar resoning is needed for @{term tcopy_loop} and @{term tcopy_end}): |
986 proof together, we obtain the left-most Hoare-triple for @{term tcopy_begin}: |
983 |
987 |
984 |
988 |
985 \begin{center} |
989 \begin{center} |
986 @{thm (concl) begin_correct}\hspace{6mm} |
990 @{thm (concl) begin_correct}\hspace{6mm} |
987 @{thm (concl) loop_correct}\hspace{6mm} |
991 @{thm (concl) loop_correct}\hspace{6mm} |
988 @{thm (concl) end_correct} |
992 @{thm (concl) end_correct} |
989 \end{center} |
993 \end{center} |
990 |
994 |
991 \noindent |
995 \noindent |
992 where we assume @{text "0 < n"}. Since the invariant of the halting |
996 where we assume @{text "0 < n"} (similar resoning is needed for |
993 state of @{term tcopy_begin} implies the invariant of the starting |
997 @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of |
994 state of @{term tcopy_loop}, that is @{term "inv_begin0 n \<mapsto> |
998 the halting state of @{term tcopy_begin} implies the invariant of |
995 inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1 n"}, we |
999 the starting state of @{term tcopy_loop}, that is @{term "inv_begin0 |
996 can derive using our Hoare-rules for sequentially composed Turing programs |
1000 n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1 |
997 the correctness of @{term tcopy}: |
1001 n"}, we can derive using our Hoare-rules for the correctness |
|
1002 of @{term tcopy}: |
998 |
1003 |
999 \begin{center} |
1004 \begin{center} |
1000 @{thm tcopy_correct} |
1005 @{thm tcopy_correct} |
1001 \end{center} |
1006 \end{center} |
|
1007 |
|
1008 \noindent |
|
1009 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)>)"}}. |
1002 |
1011 |
1003 Finally, we are in the position to prove the undecidability of the halting problem. |
1012 Finally, we are in the position to prove the undecidability of the halting problem. |
1004 A program @{term p} started with a standard tape containing the (encoded) numbers |
1013 A program @{term p} started with a standard tape containing the (encoded) numbers |
1005 @{term ns} will \emph{halt} with a standard tape containging a single (encoded) |
1014 @{term ns} will \emph{halt} with a standard tape containging a single (encoded) |
1006 number is defined as |
1015 number is defined as |
1008 \begin{center} |
1017 \begin{center} |
1009 @{thm haltP_def} |
1018 @{thm haltP_def} |
1010 \end{center} |
1019 \end{center} |
1011 |
1020 |
1012 \noindent |
1021 \noindent |
1013 This means we considering only Turing machine programs representing |
1022 This roughly means we considering only Turing machine programs |
1014 functions that take some numbers as input and produce a single |
1023 representing functions that take some numbers as input and produce a |
1015 number as output. The undecidability problem states that there is no |
1024 single number as output. For undecidability, the property we are |
1016 Turing machine that can decide the halting problem (answer eith |
1025 proving is that there is no Turing machine that can decide in |
1017 @{text 0} for halting and @{text 1} for looping). Given our |
1026 general whether a Turing machine program halts (answer either @{text |
1018 correctness proofs for @{term dither} and @{term tcopy} shown above, |
1027 0} for halting and @{text 1} for looping). Given our correctness |
1019 this non-existence is relatively straightforward to establish. We |
1028 proofs for @{term dither} and @{term tcopy} shown above, this |
1020 first assume there is a coding function, written @{term "code M"}, which |
1029 non-existence is relatively straightforward to establish. We first |
1021 represents a Turing machine @{term "M"} as a natural number. No further |
1030 assume there is a coding function, written @{term "code M"}, which |
1022 assumptions are made about this coding function. Suppose a Turing |
1031 represents a Turing machine @{term "M"} as a natural number. No |
1023 machine @{term H} exists such that if started with the standard tape |
1032 further assumptions are made about this coding function. Suppose a |
1024 @{term "([Bk], <(code M, ns)>)"} returns @{text 0}, respectively @{text 1}, |
1033 Turing machine @{term H} exists such that if started with the |
1025 depending on whether @{text M} halts when started with the input |
1034 standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0}, |
1026 tape containing @{term "<ns>"}. This assumption is formalised as |
1035 respectively @{text 1}, depending on whether @{text M} halts when |
1027 follows---for all @{term M} and natural numbers @{term ns}: |
1036 started with the input tape containing @{term "<ns>"}. This |
|
1037 assumption is formalised as follows---for all @{term M} and natural |
|
1038 numbers @{term ns}: |
1028 |
1039 |
1029 \begin{center} |
1040 \begin{center} |
1030 \begin{tabular}{r} |
1041 \begin{tabular}{r} |
1031 @{thm (prem 2) uncomputable.h_case} implies |
1042 @{thm (prem 2) uncomputable.h_case} implies |
1032 @{thm (concl) uncomputable.h_case}\\ |
1043 @{thm (concl) uncomputable.h_case}\\ |