--- a/Paper/Paper.thy Fri Feb 01 14:54:47 2013 +0000
+++ b/Paper/Paper.thy Sun Feb 03 12:24:00 2013 +0000
@@ -7,6 +7,7 @@
hide_const (open) s
*)
+
hide_const (open) Divides.adjust
abbreviation
@@ -14,6 +15,43 @@
consts DUMMY::'a
+
+(* THEOREMS *)
+notation (Rule output)
+ "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+syntax (Rule output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
+ ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (Axiom output)
+ "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
+notation (IfThen output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (IfThenNoBox output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+
+context uncomputable
+begin
+
notation (latex output)
Cons ("_::_" [48,47] 48) and
set ("") and
@@ -26,7 +64,8 @@
tcopy_loop ("cloop") and
tcopy_end ("cend") and
step0 ("step") and
- uncomputable.tcontra ("tcontra") and
+ tcontra ("contra") and
+ code_tcontra ("code contra") and
steps0 ("steps") and
exponent ("_\<^bsup>_\<^esup>") and
haltP ("halts") and
@@ -83,38 +122,6 @@
declare [[show_question_marks = false]]
-(* THEOREMS *)
-notation (Rule output)
- "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
-
-syntax (Rule output)
- "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
-
- "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
- ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
-
- "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
-
-notation (Axiom output)
- "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
-
-notation (IfThen output)
- "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-syntax (IfThen output)
- "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
- "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
- "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
-
-notation (IfThenNoBox output)
- "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
-syntax (IfThenNoBox output)
- "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
- ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
- "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
- "_asm" :: "prop \<Rightarrow> asms" ("_")
-
lemma nats2tape:
shows "<([]::nat list)> = []"
and "<[n]> = <n>"
@@ -143,6 +150,7 @@
shows "inv_begin0 n (l, r) = (n = 1 \<and> (l, r) = ([], [Bk, Oc, Bk, Oc]))"
using assms by auto
+
(*>*)
section {* Introduction *}
@@ -173,7 +181,7 @@
matter whether @{text P} is constructed by computable means. We hit on
this limitation previously when we mechanised the correctness proofs
of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12}, but
-were unable to formalise arguments about decidability.
+were unable to formalise arguments about decidability or undecidability.
%The same problem would arise if we had formulated
%the algorithms as recursive functions, because internally in
@@ -583,7 +591,7 @@
\noindent Recall our definition of @{term fetch} (shown in
\eqref{fetch}) with the default value for the @{text 0}-state. In
case a Turing program takes according to the usual textbook
- definition \cite{Boolos87} less than @{text n} steps before it
+ definition, say \cite{Boolos87}, less than @{text n} steps before it
halts, then in our setting the @{term steps}-evaluation does not
actually halt, but rather transitions to the @{text 0}-state (the
final state) and remains there performing @{text Nop}-actions until
@@ -786,7 +794,7 @@
\noindent
where
@{term "P' \<mapsto> P"} stands for the fact that for all tapes @{term "tp"},
- @{term "P' tp"} implies @{term "P tp"}.
+ @{term "P' tp"} implies @{term "P tp"} (similarly for @{text "Q"} and @{text "Q'"}).
Like Asperti and Ricciotti with their notion of realisability, we
have set up our Hoare-rules so that we can deal explicitly
@@ -994,11 +1002,11 @@
\noindent
where we assume @{text "0 < n"} (similar resoning is needed for
- @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
+ the Hoare-triples for @{term tcopy_loop} and @{term tcopy_end}). Since the invariant of
the halting state of @{term tcopy_begin} implies the invariant of
the starting state of @{term tcopy_loop}, that is @{term "inv_begin0
n \<mapsto> inv_loop1 n"} holds, and also @{term "inv_loop0 n = inv_end1
- n"}, we can derive using our Hoare-rules for the correctness
+ n"}, we can derive the following Hoare-triple for the correctness
of @{term tcopy}:
\begin{center}
@@ -1007,7 +1015,7 @@
\noindent
That means if we start with a tape of the form @{term "([], <n::nat>)"} then
- @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}.
+ @{term tcopy} will halt with the tape \mbox{@{term "([Bk], <(n::nat, n::nat)>)"}}, as desired.
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
@@ -1026,7 +1034,7 @@
general whether a Turing machine program halts (answer either @{text
0} for halting and @{text 1} for looping). Given our correctness
proofs for @{term dither} and @{term tcopy} shown above, this
- non-existence is relatively straightforward to establish. We first
+ non-existence is now relatively straightforward to establish. We first
assume there is a coding function, written @{term "code M"}, which
represents a Turing machine @{term "M"} as a natural number. No
further assumptions are made about this coding function. Suppose a
@@ -1034,8 +1042,8 @@
standard tape @{term "([Bk], <(code M, ns)>)"} returns @{text 0},
respectively @{text 1}, depending on whether @{text M} halts when
started with the input tape containing @{term "<ns>"}. This
- assumption is formalised as follows---for all @{term M} and natural
- numbers @{term ns}:
+ assumption is formalised as follows---for all @{term M} and all lists of
+ natural numbers @{term ns}:
\begin{center}
\begin{tabular}{r}
@@ -1051,34 +1059,69 @@
The contradiction can be derived using the following Turing machine
\begin{center}
- @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
+ @{thm tcontra_def}
+ \end{center}
+
+ \noindent
+ Suppose @{thm (prem 1) "tcontra_halt"}. Given the invariants on the
+ left, we can derive the following Hoare-pair for @{term tcontra} on the right.
+
+ \begin{center}\small
+ \begin{tabular}{@ {}c@ {\hspace{-10mm}}c@ {}}
+ \begin{tabular}[t]{@ {}l@ {}}
+ @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+ @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+ @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
+ \end{tabular}
+ &
+ \begin{tabular}[b]{@ {}l@ {}}
+ \raisebox{-20mm}{$\inferrule*{
+ \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
+ {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
+ \\ @{term "{P\<^isub>3} dither \<up>"}
+ }
+ {@{term "{P\<^isub>1} tcontra \<up>"}}
+ $}
+ \end{tabular}
+ \end{tabular}
\end{center}
\noindent
- Let us assume @{thm (prem 2) "uncomputable.tcontra_halt"}
- Proof
+ This Hoare-pair contradicts our assumption that @{term tcontra} started
+ with @{term "<(code tcontra)>"} halts.
+
+ Suppose @{thm (prem 1) "tcontra_unhalt"}. Again given the invariants on the
+ left, we can derive the Hoare-triple for @{term tcontra} on the right.
- \begin{center}
- $\inferrule*{
- \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
- {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
- \\ @{term "{P\<^isub>3} dither {P\<^isub>3}"}
+ \begin{center}\small
+ \begin{tabular}{@ {}c@ {\hspace{-17mm}}c@ {}}
+ \begin{tabular}[t]{@ {}l@ {}}
+ @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+ @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+ @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
+ \end{tabular}
+ &
+ \begin{tabular}[t]{@ {}l@ {}}
+ \raisebox{-20mm}{$\inferrule*{
+ \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
+ {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
+ \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
}
- {@{term "{P\<^isub>1} tcontra {P\<^isub>3}"}}
- $
+ {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
+ $}
+ \end{tabular}
+ \end{tabular}
\end{center}
- \begin{center}
- $\inferrule*{
- \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {Q\<^isub>3}"}}
- {@{term "{P\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
- \\ @{term "{Q\<^isub>3} dither \<up>"}
- }
- {@{term "{P\<^isub>1} tcontra \<up>"}}
- $
- \end{center}
+ \noindent
+ This time the Hoare-triple states that @{term tcontra} terminates
+ with the ``output'' @{term "<(1::nat)>"}. In both case we come
+ to an contradiction, which means we have to abondon our assumption
+ that there exists a Turing machine @{term H} which can decide
+ whether Turing machines terminate.
+
- Magnus: invariants -- Section 5.4.5 on page 75.
+
*}
@@ -1204,6 +1247,9 @@
a new tape corresponding to the value @{term l} (the number of @{term Oc}s
clustered on the output tape).
+
+
+ Magnus: invariants -- Section 5.4.5 on page 75.
*}
@@ -1220,4 +1266,5 @@
(*<*)
end
+end
(*>*)
\ No newline at end of file