Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Paper/Paper.thy
changeset 105 2cae8a39803e
parent 104 01f688735b9b
child 106 c3155e9e4f63
equal deleted inserted replaced
104:01f688735b9b 105:2cae8a39803e 
    20   W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
 
    20   W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
 
    21   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
 
    21   W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
 
    22   update2 ("update") and
 
    22   update2 ("update") and
 
    23   tm_wf0 ("wf") and
 
    23   tm_wf0 ("wf") and
 
    24   (*is_even ("iseven") and*)
 
    24   (*is_even ("iseven") and*)
 
    25   tcopy_begin ("copy\<^bsub>begin\<^esub>") and
 
    25   tcopy_begin ("cbegin") and
 
    26   tcopy_loop ("copy\<^bsub>loop\<^esub>") and
 
    26   tcopy_loop ("cloop") and
 
    27   tcopy_end ("copy\<^bsub>end\<^esub>") and
 
    27   tcopy_end ("cend") and
 
    28   step0 ("step") and
 
    28   step0 ("step") and
 
    29   uncomputable.tcontra ("C") and
 
    29   uncomputable.tcontra ("tcontra") and
 
    30   steps0 ("steps") and
 
    30   steps0 ("steps") and
 
    31   exponent ("_\<^bsup>_\<^esup>") and
 
    31   exponent ("_\<^bsup>_\<^esup>") and
 
    32 (*  abc_lm_v ("lookup") and
 
    32   haltP ("halts") and 
    33   abc_lm_s ("set") and*)
 
       
    34   haltP ("stdhalt") and 
       
    35   tcopy ("copy") and 
    33   tcopy ("copy") and 
    36   tape_of ("\<langle>_\<rangle>") and 
    34   tape_of ("\<langle>_\<rangle>") and 
    37   tm_comp ("_ \<oplus> _") and 
    35   tm_comp ("_ \<oplus> _") and 
    38   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and
 
    36   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and
 
    39   inv_begin0 ("I\<^isub>0") and
 
    37   inv_begin0 ("I\<^isub>0") and
 
    40   inv_begin1 ("I\<^isub>1") and
 
    38   inv_begin1 ("I\<^isub>1") and
 
    41   inv_begin2 ("I\<^isub>2") and
 
    39   inv_begin2 ("I\<^isub>2") and
 
    42   inv_begin3 ("I\<^isub>3") and
 
    40   inv_begin3 ("I\<^isub>3") and
 
    43   inv_begin4 ("I\<^isub>4") and 
    41   inv_begin4 ("I\<^isub>4") and 
    44   inv_begin ("I\<^bsub>begin\<^esub>")
 
    42   inv_begin ("I\<^bsub>cbegin\<^esub>") and
 
       
    43   inv_loop1 ("J\<^isub>1") and
 
       
    44   inv_loop0 ("J\<^isub>0") and
 
       
    45   inv_end1 ("K\<^isub>1") and
 
       
    46   inv_end0 ("K\<^isub>0") and
 
       
    47   measure_begin_step ("M\<^bsub>cbegin\<^esub>")
 
    45 
    48 
    46  
    49  
    47 lemma inv_begin_print:
 
    50 lemma inv_begin_print:
 
    48   shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
 
    51   shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and
 
    49         "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 
    52         "s = 1 \<Longrightarrow> inv_begin n (s, tp) = inv_begin1 n tp" and 
    68 apply(rule ext)
 
    71 apply(rule ext)
 
    69 apply(case_tac x)
 
    72 apply(case_tac x)
 
    70 apply(simp add: inv_end1.simps)
 
    73 apply(simp add: inv_end1.simps)
 
    71 done
 
    74 done
 
    72 
    75 
       
    76 
       
    77 lemma measure_begin_print:
 
       
    78   shows "s = 2 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
 
       
    79         "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
 
       
    80         "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and 
       
    81         "s \<notin> {2,3,4} \<Longrightarrow> measure_begin_step (s, l, r) = 0"
 
       
    82 by (simp_all)
 
    73 
    83 
    74 declare [[show_question_marks = false]]
 
    84 declare [[show_question_marks = false]]
 
    75 
    85 
    76 (* THEOREMS *)
 
    86 (* THEOREMS *)
 
    77 notation (Rule output)
 
    87 notation (Rule output)
 
   898   each state of @{term tcopy_begin}, we define the
 
   908   each state of @{term tcopy_begin}, we define the
 
   899   following invariant for the whole @{term tcopy_begin} program:
 
   909   following invariant for the whole @{term tcopy_begin} program:
 
   900 
   910 
   901   \begin{figure}[t]
 
   911   \begin{figure}[t]
 
   902   \begin{center}
 
   912   \begin{center}
 
   903   \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}}
 
   913   \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}}
 
   904   @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
 
   914   \hline
 
   905                                 &             & @{thm (rhs) inv_begin02} \\
 
       
   906   @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
 
   915   @{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
 
   907   @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
 
   916   @{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
 
   908   @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
 
   917   @{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
 
   909   @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
 
   918   @{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
 
       
   919   @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
 
       
   920                                 &             & @{thm (rhs) inv_begin02}\smallskip \\
 
       
   921    \hline
 
   910   @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
 
   922   @{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
 
   911                                &             & @{thm (rhs) inv_loop1_exit.simps}\\
 
   923                                &             & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
 
   912   @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}\\
 
   924   @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
 
   913   \end{tabular}
 
   925    \hline
 
   914   \end{center}
 
   926   @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
 
   915   \caption{The invariants for each state of @{term tcopy_begin}. They depend on
 
   927   @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\
 
   916   the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin}
 
   928   \hline
 
       
   929   \end{tabular}
 
       
   930   \end{center}
 
       
   931   \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} for the states of 
       
   932   @{term tcopy_begin}. Below, the invariants 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
 
       
   934   of @{term Oc}s with which the Turing machine is started.}\label{invbegin}
 
   917   \end{figure}
 
   935   \end{figure}
 
   918 
   936 
   919   \begin{center}
 
   937   \begin{center}
 
   920   \begin{tabular}{rcl}
 
   938   \begin{tabular}{rcl}
 
   921   @{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} & 
   939   @{thm (lhs) inv_begin.simps} & @{text "\<equiv>"} & 
   930 
   948 
   931   \noindent
 
   949   \noindent
 
   932   This invariant depends on @{term n} representing the number of
 
   950   This invariant depends on @{term n} representing the number of
 
   933   @{term Oc}s (or encoded number) on the tape. It is not hard (26
 
   951   @{term Oc}s (or encoded number) on the tape. It is not hard (26
 
   934   lines of automated proof script) to show that for @{term "n >
 
   952   lines of automated proof script) to show that for @{term "n >
 
   935   (0::nat)"} this invariant is preserved under computation rules
 
   953   (0::nat)"} this invariant is preserved under the computation rules
 
   936   @{term step} and @{term steps}.
 
   954   @{term step} and @{term steps}. This gives us partial correctness
 
   937 
   955   for @{term "tcopy_begin"}. 
   938   measure for the copying TM, which we however omit.
 
   956 
   939 
   957   We next need to show that @{term "tcopy_begin"} terminates. For this
 
       
   958   we introduce lexicographically ordered pairs @{term "(n, m)"}
 
       
   959   derived from configurations @{text "(s, (l, r))"}: @{text n} stands
 
       
   960   for the state ordered according to how @{term tcopy_begin} executes
 
       
   961   them, that is @{text "1 > 2 > 3 > 4 > 0"}; @{term m} is calculated
 
       
   962   according to the measure function:
 
       
   963 
       
   964   \begin{center}
 
       
   965   \begin{tabular}{rcl}
 
       
   966   @{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)}\\
 
       
   968   & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} @{thm (rhs) measure_begin_print(2)} \\
 
       
   969  & & @{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)}\\
 
       
   971   \end{tabular}
 
       
   972   \end{center}
 
   940   
   973   
   941   \begin{center}
 
   974   \noindent
 
   942   @{thm begin_correct}\\
 
   975   With this in place, we can show that for every starting tape of the
 
   943   @{thm loop_correct}\\
 
   976   form @{term "([], Oc \<up> n)"} with @{term "n > (0::nat)"}, the Turing
 
   944   @{thm end_correct}
 
   977   machine @{term "tcopy_begin"} will halt. Taking this and the partial
 
   945   \end{center}
 
   978   correctness proof together we obtain for @{term tcopy_begin} (similar 
   946 
   979   resoning is needed for @{term tcopy_loop} and @{term tcopy_end}):
 
   947 
   980    
       
   981 
       
   982   \begin{center}
 
       
   983   @{thm (concl) begin_correct}\hspace{6mm}
 
       
   984   @{thm (concl) loop_correct}\hspace{6mm}
 
       
   985   @{thm (concl) end_correct}
 
       
   986   \end{center}
 
       
   987 
       
   988   \noindent 
       
   989   where we assume @{text "0 < n"}. Since @{term "inv_begin0 n \<mapsto> inv_loop1 n"} holds
 
       
   990   and @{term "inv_loop0 n = inv_end1 n"}, we can derive using our Hoare-rules
 
       
   991   the correctness of @{term tcopy}
 
       
   992 
       
   993   \begin{center}
 
       
   994   @{thm tcopy_correct}
 
       
   995   \end{center}
 
       
   996 
       
   997   Finally, we are in the position to prove the undecidability of the halting problem.
 
       
   998   A program @{term p} started with a standard tape containing the (encoded) numbers
 
       
   999   @{term ns} will \emph{halt} with a standard tape containging a single (encoded) 
       
  1000   number is defined as
 
   948 
  1001 
   949   \begin{center}
 
  1002   \begin{center}
 
   950   @{thm haltP_def}
 
  1003   @{thm haltP_def}
 
   951   \end{center}
 
  1004   \end{center}
 
   952 
  1005 
   953 
  1006   \noindent
 
   954   Undecidability of the halting problem.
 
  1007   This means we considering only Turing machine programs representing functions that take 
   955 
  1008   some numbers as input and produce a single number as output. There is no Turing
 
   956   We assume a coding function from Turing machine programs to natural numbers.
 
  1009   machine that can decide the halting problem (answer @{text 0} for halting and 
   957   
  1010   @{text 1} for looping). Given our correctness proofs for @{term dither} and @{term tcopy} 
       
  1011   this non-existence is relatively straightforward to establish. We first assume there is a coding 
       
  1012   function, written @{term code}, from Turing machine programs to natural numbers.
 
       
  1013   Suppose a Turing machine @{term H} exists such that if started with the standard 
       
  1014   tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0} or @{text 1} depending
 
       
  1015   on whether @{text M} halts when started with the input tape containing @{term "<ns>"}.
 
       
  1016   This is formalised as follows
 
       
  1017  
       
  1018   \begin{center}
 
       
  1019   \begin{tabular}{r}
 
   958   @{thm (prem 2) uncomputable.h_case} implies
 
  1020   @{thm (prem 2) uncomputable.h_case} implies
 
   959   @{thm (concl) uncomputable.h_case}
 
  1021   @{thm (concl) uncomputable.h_case}\\
 
   960   
  1022   
   961   @{thm (prem 2) uncomputable.nh_case} implies
 
  1023   @{thm (prem 2) uncomputable.nh_case} implies
 
   962   @{thm (concl) uncomputable.nh_case}
 
  1024   @{thm (concl) uncomputable.nh_case}
 
   963 
  1025   \end{tabular}
 
   964   Then contradiction
 
  1026   \end{center}
 
       
  1027 
       
  1028   \noindent
 
       
  1029   The contradiction can be derived using the following Turing machine
 
   965 
  1030 
   966   \begin{center}
 
  1031   \begin{center}
 
   967   @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
 
  1032   @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
 
   968   \end{center}
 
  1033   \end{center}
 
   969 
  1034 
       
  1035   \noindent
 
       
  1036   Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"}
 
   970   Proof
 
  1037   Proof
 
   971 
  1038 
   972   \begin{center}
 
  1039   \begin{center}
 
   973   $\inferrule*{
 
  1040   $\inferrule*{
 
   974     \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
 
  1041     \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
tm