diff -r 01f688735b9b -r 2cae8a39803e Paper/Paper.thy --- a/Paper/Paper.thy Thu Jan 31 11:35:16 2013 +0000 +++ b/Paper/Paper.thy Fri Feb 01 01:34:37 2013 +0000 @@ -22,16 +22,14 @@ update2 ("update") and tm_wf0 ("wf") and (*is_even ("iseven") and*) - tcopy_begin ("copy\<^bsub>begin\<^esub>") and - tcopy_loop ("copy\<^bsub>loop\<^esub>") and - tcopy_end ("copy\<^bsub>end\<^esub>") and + tcopy_begin ("cbegin") and + tcopy_loop ("cloop") and + tcopy_end ("cend") and step0 ("step") and - uncomputable.tcontra ("C") and + uncomputable.tcontra ("tcontra") and steps0 ("steps") and exponent ("_\<^bsup>_\<^esup>") and -(* abc_lm_v ("lookup") and - abc_lm_s ("set") and*) - haltP ("stdhalt") and + haltP ("halts") and tcopy ("copy") and tape_of ("\_\") and tm_comp ("_ \ _") and @@ -41,7 +39,12 @@ inv_begin2 ("I\<^isub>2") and inv_begin3 ("I\<^isub>3") and inv_begin4 ("I\<^isub>4") and - inv_begin ("I\<^bsub>begin\<^esub>") + inv_begin ("I\<^bsub>cbegin\<^esub>") and + inv_loop1 ("J\<^isub>1") and + inv_loop0 ("J\<^isub>0") and + inv_end1 ("K\<^isub>1") and + inv_end0 ("K\<^isub>0") and + measure_begin_step ("M\<^bsub>cbegin\<^esub>") lemma inv_begin_print: @@ -71,6 +74,13 @@ done +lemma measure_begin_print: + shows "s = 2 \ measure_begin_step (s, l, r) = length r" and + "s = 3 \ measure_begin_step (s, l, r) = (if r = [] \ r = [Bk] then 1 else 0)" and + "s = 4 \ measure_begin_step (s, l, r) = length l" and + "s \ {2,3,4} \ measure_begin_step (s, l, r) = 0" +by (simp_all) + declare [[show_question_marks = false]] (* THEOREMS *) @@ -900,20 +910,28 @@ \begin{figure}[t] \begin{center} - \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}} - @{thm (lhs) inv_begin0.simps} & @{text "\"} & @{thm (rhs) inv_begin01} @{text "\"}& (halting state)\\ - & & @{thm (rhs) inv_begin02} \\ + \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}} + \hline @{thm (lhs) inv_begin1.simps} & @{text "\"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ @{thm (lhs) inv_begin2.simps} & @{text "\"} & @{thm (rhs) inv_begin2.simps}\\ @{thm (lhs) inv_begin3.simps} & @{text "\"} & @{thm (rhs) inv_begin3.simps}\\ @{thm (lhs) inv_begin4.simps} & @{text "\"} & @{thm (rhs) inv_begin4.simps}\\ + @{thm (lhs) inv_begin0.simps} & @{text "\"} & @{thm (rhs) inv_begin01} @{text "\"}& (halting state)\\ + & & @{thm (rhs) inv_begin02}\smallskip \\ + \hline @{thm (lhs) inv_loop1.simps} & @{text "\"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\"}\\ - & & @{thm (rhs) inv_loop1_exit.simps}\\ - @{thm (lhs) inv_loop0.simps} & @{text "\"} & @{thm (rhs) inv_loop0.simps}\\ + & & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\ + @{thm (lhs) inv_loop0.simps} & @{text "\"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\ + \hline + @{thm (lhs) inv_end1.simps} & @{text "\"} & @{thm (rhs) inv_end1.simps} & (starting state)\\ + @{thm (lhs) inv_end0.simps} & @{text "\"} & @{thm (rhs) inv_end0.simps} & (halting state)\smallskip\\ + \hline \end{tabular} \end{center} - \caption{The invariants for each state of @{term tcopy_begin}. They depend on - the number @{term n} of @{term Oc}s with which this Turing machine is started.}\label{invbegin} + \caption{The invariants @{term inv_begin0},\ldots,@{term inv_begin4} for the states of + @{term tcopy_begin}. Below, the invariants for the starting and halting states of + @{term tcopy_loop} and @{term tcopy_end}. In each invariant the parameter @{term n} stands for the number + of @{term Oc}s with which the Turing machine is started.}\label{invbegin} \end{figure} \begin{center} @@ -932,41 +950,90 @@ This invariant depends on @{term n} representing the number of @{term Oc}s (or encoded number) on the tape. It is not hard (26 lines of automated proof script) to show that for @{term "n > - (0::nat)"} this invariant is preserved under computation rules - @{term step} and @{term steps}. + (0::nat)"} this invariant is preserved under the computation rules + @{term step} and @{term steps}. This gives us partial correctness + for @{term "tcopy_begin"}. - measure for the copying TM, which we however omit. + We next need to show that @{term "tcopy_begin"} terminates. For this + we introduce lexicographically ordered pairs @{term "(n, m)"} + derived from configurations @{text "(s, (l, r))"}: @{text n} stands + for the state ordered according to how @{term tcopy_begin} executes + them, that is @{text "1 > 2 > 3 > 4 > 0"}; @{term m} is calculated + according to the measure function: - \begin{center} - @{thm begin_correct}\\ - @{thm loop_correct}\\ - @{thm end_correct} + \begin{tabular}{rcl} + @{term measure_begin_step}@{text "(s, (l, r))"} & @{text "\"} & + @{text "if"} @{thm (prem 1) measure_begin_print(1)} @{text then} @{thm (rhs) measure_begin_print(1)}\\ + & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(2)} @{text then} @{thm (rhs) measure_begin_print(2)} \\ + & & @{text else} @{text "if"} @{thm (prem 1) measure_begin_print(3)} @{text then} @{thm (rhs) measure_begin_print(3)}\\ + & & @{text else} @{thm (rhs) measure_begin_print(4)}\\ + \end{tabular} + \end{center} + + \noindent + With this in place, we can show that for every starting tape of the + form @{term "([], Oc \ n)"} with @{term "n > (0::nat)"}, the Turing + machine @{term "tcopy_begin"} will halt. Taking this and the partial + correctness proof together we obtain for @{term tcopy_begin} (similar + resoning is needed for @{term tcopy_loop} and @{term tcopy_end}): + + + \begin{center} + @{thm (concl) begin_correct}\hspace{6mm} + @{thm (concl) loop_correct}\hspace{6mm} + @{thm (concl) end_correct} \end{center} + \noindent + where we assume @{text "0 < n"}. Since @{term "inv_begin0 n \ inv_loop1 n"} holds + and @{term "inv_loop0 n = inv_end1 n"}, we can derive using our Hoare-rules + the correctness of @{term tcopy} + \begin{center} + @{thm tcopy_correct} + \end{center} + + Finally, we are in the position to prove the undecidability of the halting problem. + A program @{term p} started with a standard tape containing the (encoded) numbers + @{term ns} will \emph{halt} with a standard tape containging a single (encoded) + number is defined as \begin{center} @{thm haltP_def} \end{center} - - Undecidability of the halting problem. - - We assume a coding function from Turing machine programs to natural numbers. - + \noindent + This means we considering only Turing machine programs representing functions that take + some numbers as input and produce a single number as output. There is no Turing + machine that can decide the halting problem (answer @{text 0} for halting and + @{text 1} for looping). Given our correctness proofs for @{term dither} and @{term tcopy} + this non-existence is relatively straightforward to establish. We first assume there is a coding + function, written @{term code}, from Turing machine programs to natural numbers. + Suppose a Turing machine @{term H} exists such that if started with the standard + tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0} or @{text 1} depending + on whether @{text M} halts when started with the input tape containing @{term ""}. + This is formalised as follows + + \begin{center} + \begin{tabular}{r} @{thm (prem 2) uncomputable.h_case} implies - @{thm (concl) uncomputable.h_case} + @{thm (concl) uncomputable.h_case}\\ @{thm (prem 2) uncomputable.nh_case} implies @{thm (concl) uncomputable.nh_case} + \end{tabular} + \end{center} - Then contradiction + \noindent + The contradiction can be derived using the following Turing machine \begin{center} @{term "tcontra"} @{text "\"} @{term "(tcopy |+| H) |+| dither"} \end{center} + \noindent + Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"} Proof \begin{center}