--- a/Paper/Paper.thy Fri Feb 01 10:14:09 2013 +0000
+++ b/Paper/Paper.thy Fri Feb 01 13:12:55 2013 +0000
@@ -897,15 +897,19 @@
the first program terminates generating a tape for which the second
program loops. The side-conditions about @{thm (prem 3) HR2} are
needed 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.
+ initial state in @{term "p\<^isub>1"} and @{term "p\<^isub>2"}, respectively, match
+ up correctly. These Hoare-rules allow us to prove the correctness
+ of @{term tcopy} by considering the correctness of the components
+ @{term "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"}
+ in isolation. This simplifies the reasoning considerably, for
+ example when designing decreasing measures for proving the termination
+ of the programs. We will show the details for the program @{term
+ "tcopy_begin"}. For the two other programs we refer the reader to
+ our formalisation.
- The Hoare-rules allow us to prove the correctness of @{term
- tcopy} by considering the correctness of the components @{term
- "tcopy_begin"}, @{term "tcopy_loop"} and @{term "tcopy_end"} in
- isolation. We will show the details for the program @{term
- "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots,
- @{term "inv_begin4"} shown in Figure~\ref{invbegin}, which correspond to
- each state of @{term tcopy_begin}, we define the
+ Given the invariants @{term "inv_begin0"},\ldots,
+ @{term "inv_begin4"} shown in Figure~\ref{invbegin}, which
+ correspond to each state of @{term tcopy_begin}, we define the
following invariant for the whole @{term tcopy_begin} program:
\begin{figure}[t]
@@ -961,7 +965,7 @@
the state @{text s}, but ordered according to how @{term tcopy_begin} executes
them, that is @{text "1 > 2 > 3 > 4 > 0"}; in order to have
a strictly decreasing meansure, @{term m} takes the data on the tape into
- account and is calculated according to the measure function:
+ account and is calculated according to the following measure function:
\begin{center}
\begin{tabular}{rcl}
@@ -977,9 +981,9 @@
\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 eventually halt. Taking this and the partial
- correctness proof together, we obtain for @{term tcopy_begin} the Hoare-triple
- (similar resoning is needed for @{term tcopy_loop} and @{term tcopy_end}):
+ machine @{term "tcopy_begin"} will eventually halt (the measure
+ decreases in each step). Taking this and the partial correctness
+ proof together, we obtain the left-most Hoare-triple for @{term tcopy_begin}:
\begin{center}
@@ -989,17 +993,22 @@
\end{center}
\noindent
- where we assume @{text "0 < n"}. 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 sequentially composed Turing programs
- the correctness of @{term tcopy}:
+ where we assume @{text "0 < n"} (similar resoning is needed 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
+ of @{term tcopy}:
\begin{center}
@{thm tcopy_correct}
\end{center}
+ \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)>)"}}.
+
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)
@@ -1010,21 +1019,23 @@
\end{center}
\noindent
- This means we considering only Turing machine programs representing
- functions that take some numbers as input and produce a single
- number as output. The undecidability problem states that there is no
- Turing machine that can decide the halting problem (answer eith
- @{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 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 Turing
- machine @{term H} exists such that if started with the 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}:
+ This roughly means we considering only Turing machine programs
+ representing functions that take some numbers as input and produce a
+ single number as output. For undecidability, the property we are
+ proving is that there is no Turing machine that can decide in
+ 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
+ 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
+ Turing machine @{term H} exists such that if started with the
+ 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}:
\begin{center}
\begin{tabular}{r}