# HG changeset patch # User Christian Urban # Date 1359724375 0 # Node ID c2a7a99bf554d88a7a08bd8814160a346fd48299 # Parent c3155e9e4f638e790c0df47683195475105af1e2 updated paper diff -r c3155e9e4f63 -r c2a7a99bf554 Paper/Paper.thy --- 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 \ 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 \ - 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 \ 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 "([], )"} 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 ""}. 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 ""}. This + assumption is formalised as follows---for all @{term M} and natural + numbers @{term ns}: \begin{center} \begin{tabular}{r} diff -r c3155e9e4f63 -r c2a7a99bf554 paper.pdf Binary file paper.pdf has changed