Paper/Paper.thy
changeset 93 f2bda6ba4952
parent 92 b9d0dd18c81e
child 94 aeaf1374dc67
equal deleted inserted replaced
92:b9d0dd18c81e 93:f2bda6ba4952
    24   (*is_even ("iseven") and*)
    24   (*is_even ("iseven") and*)
    25   tcopy_begin ("copy\<^bsub>begin\<^esub>") and
    25   tcopy_begin ("copy\<^bsub>begin\<^esub>") and
    26   tcopy_loop ("copy\<^bsub>loop\<^esub>") and
    26   tcopy_loop ("copy\<^bsub>loop\<^esub>") and
    27   tcopy_end ("copy\<^bsub>end\<^esub>") and
    27   tcopy_end ("copy\<^bsub>end\<^esub>") and
    28   step0 ("step") and
    28   step0 ("step") and
       
    29   uncomputable.tcontra ("C") and
    29   steps0 ("steps") and
    30   steps0 ("steps") and
    30   exponent ("_\<^bsup>_\<^esup>") and
    31   exponent ("_\<^bsup>_\<^esup>") and
    31 (*  abc_lm_v ("lookup") and
    32 (*  abc_lm_v ("lookup") and
    32   abc_lm_s ("set") and*)
    33   abc_lm_s ("set") and*)
    33   haltP ("stdhalt") and 
    34   haltP ("stdhalt") and 
    76   and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
    77   and "ns \<noteq> [] \<Longrightarrow> <n#ns> = Oc \<up> (n + 1) @ [Bk] @ <ns>"
    77 apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
    78 apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps)
    78 apply(case_tac ns)
    79 apply(case_tac ns)
    79 apply(auto)
    80 apply(auto)
    80 done
    81 done
       
    82 
       
    83 lemmas HR1 = 
       
    84   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"]
       
    85 
       
    86 lemmas HR2 =
       
    87   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"]
    81 
    88 
    82 (*>*)
    89 (*>*)
    83 
    90 
    84 section {* Introduction *}
    91 section {* Introduction *}
    85 
    92 
   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
   313   \end{tabular}
   319   \end{tabular}
   314   \end{center}
   320   \end{center}
   315 
   321 
   316   \noindent
   322   \noindent
   317   We slightly deviate
   323   We slightly deviate
   318   from the presentation in \cite{Boolos87} and \cite{AspertiRicciotti12} 
   324   from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12}) 
   319   by using the @{term Nop} operation; however its use
   325   by using the @{term Nop} operation; however its use
   320   will become important when we formalise halting computations and also universal Turing 
   326   will become important when we formalise halting computations and also universal Turing 
   321   machines.  Given a tape and an action, we can define the
   327   machines.  Given a tape and an action, we can define the
   322   following tape updating function:
   328   following tape updating function:
   323 
   329 
   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