--- a/Paper/Paper.thy Sun Jan 27 20:01:13 2013 +0000
+++ b/Paper/Paper.thy Mon Jan 28 02:38:57 2013 +0000
@@ -26,6 +26,7 @@
tcopy_loop ("copy\<^bsub>loop\<^esub>") and
tcopy_end ("copy\<^bsub>end\<^esub>") and
step0 ("step") and
+ uncomputable.tcontra ("C") and
steps0 ("steps") and
exponent ("_\<^bsup>_\<^esup>") and
(* abc_lm_v ("lookup") and
@@ -79,6 +80,12 @@
apply(auto)
done
+lemmas HR1 =
+ 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"]
+
+lemmas HR2 =
+ 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"]
+
(*>*)
section {* Introduction *}
@@ -118,17 +125,16 @@
The only satisfying way out of this problem in a theorem prover based
on classical logic is to formalise a theory of computability. Norrish
-provided such a formalisation for the HOL. He choose
-the $\lambda$-calculus as the starting point for his formalisation of
-computability theory, because of its ``simplicity'' \cite[Page
-297]{Norrish11}. Part of his formalisation is a clever infrastructure
-for reducing $\lambda$-terms. He also established the computational
-equivalence between the $\lambda$-calculus and recursive functions.
-Nevertheless he concluded that it would be appealing
- to have formalisations for more operational models of
-computations, such as Turing machines or register machines. One
-reason is that many proofs in the literature use them. He noted
-however that \cite[Page 310]{Norrish11}:
+provided such a formalisation for HOL4. He choose the
+$\lambda$-calculus as the starting point for his formalisation because
+of its ``simplicity'' \cite[Page 297]{Norrish11}. Part of his
+formalisation is a clever infrastructure for reducing
+$\lambda$-terms. He also established the computational equivalence
+between the $\lambda$-calculus and recursive functions. Nevertheless
+he concluded that it would be appealing to have formalisations for
+more operational models of computations, such as Turing machines or
+register machines. One reason is that many proofs in the literature
+use them. He noted however that \cite[Page 310]{Norrish11}:
\begin{quote}
\it``If register machines are unappealing because of their
@@ -185,7 +191,7 @@
our formalisation we follow mainly the proofs from the textbook
\cite{Boolos87} and found that the description there is quite
detailed. Some details are left out however: for example, constructing
-the \emph{copy Turing program} is left as an excerise to the reader; also
+the \emph{copy Turing machine} is left as an excerise to the reader; also
\cite{Boolos87} only shows how the universal Turing machine is constructed for Turing
machines computing unary functions. We had to figure out a way to
generalise this result to $n$-ary functions. Similarly, when compiling
@@ -315,7 +321,7 @@
\noindent
We slightly deviate
- from the presentation in \cite{Boolos87} and \cite{AspertiRicciotti12}
+ from the presentation in \cite{Boolos87} (and also \cite{AspertiRicciotti12})
by using the @{term Nop} operation; however its use
will become important when we formalise halting computations and also universal Turing
machines. Given a tape and an action, we can define the
@@ -675,7 +681,7 @@
\noindent
whose three components are given in Figure~\ref{copy}. To the prove
- correctness of these Turing machine programs, we introduce the
+ the correctness of Turing machine programs, we introduce the
notion of total correctness defined in terms of
\emph{Hoare-triples}, written @{term "{P} p {Q}"}. They are very similar
to the notion of \emph{realisability} in \cite{AspertiRicciotti12}.
@@ -684,7 +690,7 @@
a tape satisfying @{term P} will after some @{text n} steps halt (have
transitioned into the halting state) with a tape satisfying @{term
Q}. We also have \emph{Hoare-pairs} of the form @{term "{P} p \<up>"}
- realising the case that a program @{term p} started with a tape
+ implementing the case that a program @{term p} started with a tape
satisfying @{term P} will loop (never transition into the halting
state). Both notion are formally defined as
@@ -709,13 +715,13 @@
\noindent
Like Asperti and Ricciotti with their notion of realisability, we
- have set up our Hoare-style reasoning so that we can deal explicitly
+ have set up our Hoare-rules so that we can deal explicitly
with total correctness and non-terminantion, rather than have
notions for partial correctness and termination. Although the latter
would allow us to reason more uniformly (only using Hoare-triples),
- we prefer our definitions because we can derive (below) simple
+ we prefer our definitions because we can derive simple
Hoare-rules for sequentially composed Turing programs. In this way
- we can reason about the correctness of @{term "tcopy_init"}, for
+ we can reason about the correctness of @{term "tcopy_begin"}, for
example, completely separately from @{term "tcopy_loop"} and @{term
"tcopy_end"}.
@@ -792,44 +798,84 @@
to produce the standard tape @{term "(DUMMY, <[n, n::nat]>)"} when
started with @{term "(DUMMY, <[n::nat]>)"}, that is making a copy of
a value on the tape. Reasoning about this program is substantially
- harder than about @{term dither}. To ease the burden, we can prove
- the following Hoare-rules for sequentially composed programs.
+ harder than about @{term dither}. To ease the burden, we prove
+ the following two Hoare-rules for sequentially composed programs.
\begin{center}
- \begin{tabular}{@ {}p{3cm}@ {\hspace{9mm}}p{3cm}@ {}}
- @{thm[mode=Rule]
- 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"]}
- &
- @{thm[mode=Rule]
- 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"]}
+ \begin{tabular}{@ {\hspace{-10mm}}c@ {\hspace{9mm}}c@ {}}
+ $\inferrule*[Right=@{thm (prem 4) HR1}]
+ {@{thm (prem 1) HR1} \\ @{thm (prem 3) HR1} \\ @{thm (prem 2) HR1}}
+ {@{thm (concl) HR1}}
+ $ &
+ $
+ \inferrule*[Right=@{thm (prem 4) HR2}]
+ {@{thm (prem 1) HR2} \\ @{thm (prem 3) HR2} \\ @{thm (prem 2) HR2}}
+ {@{thm (concl) HR2}}
+ $
\end{tabular}
\end{center}
-
+
\noindent
- The first corresponds to the usual Hoare-rule for composition of imperative
- programs, where @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for
- all tapes @{term "(l, r)"}. The second rule covers the case where rughly the
- first program terminates generating a tape for which the second program
- loops. These are two cases we need in our proof for undecidability.
-
+ The first corresponds to the usual Hoare-rule for composition of two
+ terminating programs. The premise @{term "Q\<^isub>1 \<mapsto> P\<^isub>2"} means that
+ @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for all tapes @{term "(l,
+ r)"}. The second rule covers the case where the first program
+ terminates generating a tape for which the second program loops.
+ The side-condition about @{thm (prem 4) HR2} is needed in both rules
+ in order to ensure that the redirection of the halting and initial
+ state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"} match up correctly.
+
+
The Hoare-rules above allow us to prove the correctness of @{term tcopy}
by considering the correctness of @{term "tcopy_begin"}, @{term "tcopy_loop"}
and @{term "tcopy_end"} in isolation. We will show some details for the
the program @{term "tcopy_begin"}.
- assertion holds for all tapes
-
- Hoare rule for composition
-
- For showing the undecidability of the halting problem, we need to consider
- two specific Turing machines. copying TM and dithering TM
-
- correctness of the copying TM
-
measure for the copying TM, which we however omit.
- halting problem
+ \begin{center}
+ @{thm haltP_def[where lm="ns"]}
+ \end{center}
+
+
+ Undecidability of the halting problem.
+
+ We assume a coding function from Turing machine programs to natural numbers.
+
+ @{thm (prem 2) uncomputable.h_case} implies
+ @{thm (concl) uncomputable.h_case}
+
+ @{thm (prem 2) uncomputable.nh_case} implies
+ @{thm (concl) uncomputable.nh_case}
+
+ Then contradiction
+
+ \begin{center}
+ @{term "tcontra"} @{text "\<equiv>"} @{term "(tcopy |+| H) |+| dither"}
+ \end{center}
+
+ Proof
+
+ \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}"}
+ }
+ {@{term "{P\<^isub>1} tcontra {P\<^isub>3}"}}
+ $
+ \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}
Magnus: invariants -- Section 5.4.5 on page 75.
*}