116 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
123 %Isabelle/HOL, like in all HOL-based theorem provers, functions are |
117 %represented as inductively defined predicates too. |
124 %represented as inductively defined predicates too. |
118 |
125 |
119 The only satisfying way out of this problem in a theorem prover based |
126 The only satisfying way out of this problem in a theorem prover based |
120 on classical logic is to formalise a theory of computability. Norrish |
127 on classical logic is to formalise a theory of computability. Norrish |
121 provided such a formalisation for the HOL. He choose |
128 provided such a formalisation for HOL4. He choose the |
122 the $\lambda$-calculus as the starting point for his formalisation of |
129 $\lambda$-calculus as the starting point for his formalisation because |
123 computability theory, because of its ``simplicity'' \cite[Page |
130 of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his |
124 297]{Norrish11}. Part of his formalisation is a clever infrastructure |
131 formalisation is a clever infrastructure for reducing |
125 for reducing $\lambda$-terms. He also established the computational |
132 $\lambda$-terms. He also established the computational equivalence |
126 equivalence between the $\lambda$-calculus and recursive functions. |
133 between the $\lambda$-calculus and recursive functions. Nevertheless |
127 Nevertheless he concluded that it would be appealing |
134 he concluded that it would be appealing to have formalisations for |
128 to have formalisations for more operational models of |
135 more operational models of computations, such as Turing machines or |
129 computations, such as Turing machines or register machines. One |
136 register machines. One reason is that many proofs in the literature |
130 reason is that many proofs in the literature use them. He noted |
137 use them. He noted however that \cite[Page 310]{Norrish11}: |
131 however that \cite[Page 310]{Norrish11}: |
|
132 |
138 |
133 \begin{quote} |
139 \begin{quote} |
134 \it``If register machines are unappealing because of their |
140 \it``If register machines are unappealing because of their |
135 general fiddliness,\\ Turing machines are an even more |
141 general fiddliness,\\ Turing machines are an even more |
136 daunting prospect.'' |
142 daunting prospect.'' |
183 started are not ``sufficiently accurate to be directly usable as a |
189 started are not ``sufficiently accurate to be directly usable as a |
184 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
190 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For |
185 our formalisation we follow mainly the proofs from the textbook |
191 our formalisation we follow mainly the proofs from the textbook |
186 \cite{Boolos87} and found that the description there is quite |
192 \cite{Boolos87} and found that the description there is quite |
187 detailed. Some details are left out however: for example, constructing |
193 detailed. Some details are left out however: for example, constructing |
188 the \emph{copy Turing program} is left as an excerise to the reader; also |
194 the \emph{copy Turing machine} is left as an excerise to the reader; also |
189 \cite{Boolos87} only shows how the universal Turing machine is constructed for Turing |
195 \cite{Boolos87} only shows how the universal Turing machine is constructed for Turing |
190 machines computing unary functions. We had to figure out a way to |
196 machines computing unary functions. We had to figure out a way to |
191 generalise this result to $n$-ary functions. Similarly, when compiling |
197 generalise this result to $n$-ary functions. Similarly, when compiling |
192 recursive functions to abacus machines, the textbook again only shows |
198 recursive functions to abacus machines, the textbook again only shows |
193 how it can be done for 2- and 3-ary functions, but in the |
199 how it can be done for 2- and 3-ary functions, but in the |
673 \end{tabular}}\label{tcopy} |
679 \end{tabular}}\label{tcopy} |
674 \end{equation} |
680 \end{equation} |
675 |
681 |
676 \noindent |
682 \noindent |
677 whose three components are given in Figure~\ref{copy}. To the prove |
683 whose three components are given in Figure~\ref{copy}. To the prove |
678 correctness of these Turing machine programs, we introduce the |
684 the correctness of Turing machine programs, we introduce the |
679 notion of total correctness defined in terms of |
685 notion of total correctness defined in terms of |
680 \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar |
686 \emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar |
681 to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. |
687 to the notion of \emph{realisability} in \cite{AspertiRicciotti12}. |
682 They implement the |
688 They implement the |
683 idea that a program @{term p} started in state @{term "1::nat"} with |
689 idea that a program @{term p} started in state @{term "1::nat"} with |
684 a tape satisfying @{term P} will after some @{text n} steps halt (have |
690 a tape satisfying @{term P} will after some @{text n} steps halt (have |
685 transitioned into the halting state) with a tape satisfying @{term |
691 transitioned into the halting state) with a tape satisfying @{term |
686 Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"} |
692 Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"} |
687 realising the case that a program @{term p} started with a tape |
693 implementing the case that a program @{term p} started with a tape |
688 satisfying @{term P} will loop (never transition into the halting |
694 satisfying @{term P} will loop (never transition into the halting |
689 state). Both notion are formally defined as |
695 state). Both notion are formally defined as |
690 |
696 |
691 \begin{center} |
697 \begin{center} |
692 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
698 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
707 \end{tabular} |
713 \end{tabular} |
708 \end{center} |
714 \end{center} |
709 |
715 |
710 \noindent |
716 \noindent |
711 Like Asperti and Ricciotti with their notion of realisability, we |
717 Like Asperti and Ricciotti with their notion of realisability, we |
712 have set up our Hoare-style reasoning so that we can deal explicitly |
718 have set up our Hoare-rules so that we can deal explicitly |
713 with total correctness and non-terminantion, rather than have |
719 with total correctness and non-terminantion, rather than have |
714 notions for partial correctness and termination. Although the latter |
720 notions for partial correctness and termination. Although the latter |
715 would allow us to reason more uniformly (only using Hoare-triples), |
721 would allow us to reason more uniformly (only using Hoare-triples), |
716 we prefer our definitions because we can derive (below) simple |
722 we prefer our definitions because we can derive simple |
717 Hoare-rules for sequentially composed Turing programs. In this way |
723 Hoare-rules for sequentially composed Turing programs. In this way |
718 we can reason about the correctness of @{term "tcopy_init"}, for |
724 we can reason about the correctness of @{term "tcopy_begin"}, for |
719 example, completely separately from @{term "tcopy_loop"} and @{term |
725 example, completely separately from @{term "tcopy_loop"} and @{term |
720 "tcopy_end"}. |
726 "tcopy_end"}. |
721 |
727 |
722 It is realatively straightforward to prove that the Turing program |
728 It is realatively straightforward to prove that the Turing program |
723 @{term "dither"} shown in \eqref{dither} is correct. This program |
729 @{term "dither"} shown in \eqref{dither} is correct. This program |
790 |
796 |
791 The purpose of the @{term tcopy} program defined in \eqref{tcopy} is |
797 The purpose of the @{term tcopy} program defined in \eqref{tcopy} is |
792 to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when |
798 to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when |
793 started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of |
799 started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of |
794 a value on the tape. Reasoning about this program is substantially |
800 a value on the tape. Reasoning about this program is substantially |
795 harder than about @{term dither}. To ease the burden, we can prove |
801 harder than about @{term dither}. To ease the burden, we prove |
796 the following Hoare-rules for sequentially composed programs. |
802 the following two Hoare-rules for sequentially composed programs. |
797 |
803 |
798 \begin{center} |
804 \begin{center} |
799 \begin{tabular}{@ {}p{3cm}@ {\hspace{9mm}}p{3cm}@ {}} |
805 \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{9mm}}c@ {}} |
800 @{thm[mode=Rule] |
806 $\inferrule*[Right=@{thm (prem 4) HR1}] |
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"]} |
807 {@{thm (prem 1) HR1} \\ @{thm (prem 3) HR1} \\ @{thm (prem 2) HR1}} |
802 & |
808 {@{thm (concl) HR1}} |
803 @{thm[mode=Rule] |
809 $ & |
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"]} |
810 $ |
805 \end{tabular} |
811 \inferrule*[Right=@{thm (prem 4) HR2}] |
806 \end{center} |
812 {@{thm (prem 1) HR2} \\ @{thm (prem 3) HR2} \\ @{thm (prem 2) HR2}} |
807 |
813 {@{thm (concl) HR2}} |
808 \noindent |
814 $ |
809 The first corresponds to the usual Hoare-rule for composition of imperative |
815 \end{tabular} |
810 programs, where @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for |
816 \end{center} |
811 all tapes @{term "(l, r)"}. The second rule covers the case where rughly the |
817 |
812 first program terminates generating a tape for which the second program |
818 \noindent |
813 loops. These are two cases we need in our proof for undecidability. |
819 The first corresponds to the usual Hoare-rule for composition of two |
814 |
820 terminating programs. The premise @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means that |
|
821 @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for all tapes @{term "(l, |
|
822 r)"}. The second rule covers the case where the first program |
|
823 terminates generating a tape for which the second program loops. |
|
824 The side-condition about @{thm (prem 4) HR2} is needed in both rules |
|
825 in order to ensure that the redirection of the halting and initial |
|
826 state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly. |
|
827 |
|
828 |
815 The Hoare-rules above allow us to prove the correctness of @{term tcopy} |
829 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"} |
830 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 |
831 and @{term "tcopy_end"} in isolation. We will show some details for the |
818 the program @{term "tcopy_begin"}. |
832 the program @{term "tcopy_begin"}. |
819 |
833 |
820 |
834 |
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. |
835 measure for the copying TM, which we however omit. |
831 |
836 |
832 halting problem |
837 \begin{center} |
|
838 @{thm haltP_def[where lm="ns"]} |
|
839 \end{center} |
|
840 |
|
841 |
|
842 Undecidability of the halting problem. |
|
843 |
|
844 We assume a coding function from Turing machine programs to natural numbers. |
|
845 |
|
846 @{thm (prem 2) uncomputable.h_case} implies |
|
847 @{thm (concl) uncomputable.h_case} |
|
848 |
|
849 @{thm (prem 2) uncomputable.nh_case} implies |
|
850 @{thm (concl) uncomputable.nh_case} |
|
851 |
|
852 Then contradiction |
|
853 |
|
854 \begin{center} |
|
855 @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"} |
|
856 \end{center} |
|
857 |
|
858 Proof |
|
859 |
|
860 \begin{center} |
|
861 $\inferrule*{ |
|
862 \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}} |
|
863 {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}} |
|
864 \\ @{term "{P\<^isub>3} dither {P\<^isub>3}"} |
|
865 } |
|
866 {@{term "{P\<^isub>1} tcontra {P\<^isub>3}"}} |
|
867 $ |
|
868 \end{center} |
|
869 |
|
870 \begin{center} |
|
871 $\inferrule*{ |
|
872 \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {Q\<^isub>3}"}} |
|
873 {@{term "{P\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}} |
|
874 \\ @{term "{Q\<^isub>3} dither \<up>"} |
|
875 } |
|
876 {@{term "{P\<^isub>1} tcontra \<up>"}} |
|
877 $ |
|
878 \end{center} |
833 |
879 |
834 Magnus: invariants -- Section 5.4.5 on page 75. |
880 Magnus: invariants -- Section 5.4.5 on page 75. |
835 *} |
881 *} |
836 |
882 |
837 |
883 |