--- 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 ("\<langle>_\<rangle>") and
tm_comp ("_ \<oplus> _") 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 \<Longrightarrow> measure_begin_step (s, l, r) = length r" and
+ "s = 3 \<Longrightarrow> measure_begin_step (s, l, r) = (if r = [] \<or> r = [Bk] then 1 else 0)" and
+ "s = 4 \<Longrightarrow> measure_begin_step (s, l, r) = length l" and
+ "s \<notin> {2,3,4} \<Longrightarrow> 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 "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
- & & @{thm (rhs) inv_begin02} \\
+ \begin{tabular}{@ {}lcl@ {\hspace{-0.5cm}}l@ {}}
+ \hline
@{thm (lhs) inv_begin1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\
@{thm (lhs) inv_begin2.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin2.simps}\\
@{thm (lhs) inv_begin3.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin3.simps}\\
@{thm (lhs) inv_begin4.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin4.simps}\\
+ @{thm (lhs) inv_begin0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_begin01} @{text "\<or>"}& (halting state)\\
+ & & @{thm (rhs) inv_begin02}\smallskip \\
+ \hline
@{thm (lhs) inv_loop1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop1_loop.simps} @{text "\<or>"}\\
- & & @{thm (rhs) inv_loop1_exit.simps}\\
- @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}\\
+ & & @{thm (rhs) inv_loop1_exit.simps} & (starting state)\\
+ @{thm (lhs) inv_loop0.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_loop0.simps}& (halting state)\smallskip\\
+ \hline
+ @{thm (lhs) inv_end1.simps} & @{text "\<equiv>"} & @{thm (rhs) inv_end1.simps} & (starting state)\\
+ @{thm (lhs) inv_end0.simps} & @{text "\<equiv>"} & @{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 "\<equiv>"} &
+ @{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 \<up> 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 \<mapsto> 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 "<ns>"}.
+ 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 "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
\end{center}
+ \noindent
+ Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"}
Proof
\begin{center}