diff -r bd320b5365e2 -r d6f04e3e9894 Paper/Paper.thy --- a/Paper/Paper.thy Tue Jan 29 16:37:38 2013 +0000 +++ b/Paper/Paper.thy Wed Jan 30 02:26:56 2013 +0000 @@ -35,7 +35,41 @@ tcopy ("copy") and tape_of ("\_\") and tm_comp ("_ \ _") and - DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") + DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") and + inv_begin0 ("I\<^isub>0") and + inv_begin1 ("I\<^isub>1") and + inv_begin2 ("I\<^isub>2") and + inv_begin3 ("I\<^isub>3") and + inv_begin4 ("I\<^isub>4") and + inv_begin ("I\<^bsub>begin\<^esub>") + + +lemma inv_begin_print: + shows "s = 0 \ inv_begin n (s, tp) = inv_begin0 n tp" and + "s = 1 \ inv_begin n (s, tp) = inv_begin1 n tp" and + "s = 2 \ inv_begin n (s, tp) = inv_begin2 n tp" and + "s = 3 \ inv_begin n (s, tp) = inv_begin3 n tp" and + "s = 4 \ inv_begin n (s, tp) = inv_begin4 n tp" and + "s \ {0,1,2,3,4} \ inv_begin n (s, l, r) = False" +apply(case_tac [!] tp) +by (auto) + +lemma inv1: + shows "0 < n \ inv_begin0 n \ inv_loop1 n" +unfolding assert_imp_def +unfolding inv_loop1.simps inv_begin0.simps +apply(auto) +apply(rule_tac x="1" in exI) +apply(auto simp add: replicate.simps) +done + +lemma inv2: + shows "0 < n \ inv_loop0 n = inv_end1 n" +apply(rule ext) +apply(case_tac x) +apply(simp add: inv_end1.simps) +done + declare [[show_question_marks = false]] @@ -73,12 +107,15 @@ lemma nats2tape: shows "<([]::nat list)> = []" - and "<[n]> = Oc \ (n + 1)" - and "ns \ [] \ = Oc \ (n + 1) @ [Bk] @ " -apply(auto simp add: tape_of_nl_abv tape_of_nat_list.simps) + and "<[n]> = " + and "ns \ [] \ = <(n::nat, ns)>" + and "<(n, m)> = @ [Bk] @ " + and "<[n, m]> = <(n, m)>" + and " = Oc \ (n + 1)" +apply(auto simp add: tape_of_nat_pair tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps) apply(case_tac ns) -apply(auto) -done +apply(auto simp add: tape_of_nat_pair tape_of_nat_abv) +done lemmas HR1 = Hoare_plus_halt_simple[where ?P1.0="P" and ?P2.0="Q" and ?P3.0="R\" and ?A="p\<^isub>1" and B="p\<^isub>2"] @@ -86,6 +123,16 @@ lemmas HR2 = Hoare_plus_unhalt_simple[where ?P1.0="P" and ?P2.0="Q" and ?A="p\<^isub>1" and B="p\<^isub>2"] +lemma inv_begin01: + assumes "n > 1" + shows "inv_begin0 n (l, r) = (n > 1 \ (l, r) = (Oc \ (n - 2), [Oc, Oc, Bk, Oc]))" +using assms by auto + +lemma inv_begin02: + assumes "n = 1" + shows "inv_begin0 n (l, r) = (n = 1 \ (l, r) = ([], [Bk, Oc, Bk, Oc]))" +using assms by auto + (*>*) section {* Introduction *} @@ -179,26 +226,27 @@ %standard proof of this property uses the notion of universal %Turing machines. -We are not the first who formalised Turing machines: we are aware -of the work by Asperti and Ricciotti -\cite{AspertiRicciotti12}. They describe a complete formalisation of -Turing machines in the Matita theorem prover, including a universal -Turing machine. However, they do \emph{not} formalise the undecidability of the -halting problem since their main focus is complexity, rather than -computability theory. They also report that the informal proofs from which they -started are not ``sufficiently accurate to be directly usable as a -guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For -our formalisation we follow mainly the proofs from the textbook +We are not the first who formalised Turing machines: we are aware of +the work by Asperti and Ricciotti \cite{AspertiRicciotti12}. They +describe a complete formalisation of Turing machines in the Matita +theorem prover, including a universal Turing machine. However, they do +\emph{not} formalise the undecidability of the halting problem since +their main focus is complexity, rather than computability theory. They +also report that the informal proofs from which they started are not +``sufficiently accurate to be directly usable as a guideline for +formalization'' \cite[Page 2]{AspertiRicciotti12}. For 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 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 -recursive functions to abacus machines, the textbook again only shows -how it can be done for 2- and 3-ary functions, but in the -formalisation we need arbitrary functions. But the general ideas for -how to do this are clear enough in \cite{Boolos87}. +the \emph{copy Turing machine} and its correctness proof are 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 recursive functions to +abacus machines, the textbook again only shows how it can be done for +2- and 3-ary functions, but in the formalisation we need arbitrary +functions. But the general ideas for how to do this are clear enough +in \cite{Boolos87}. %However, one %aspect that is completely left out from the informal description in %\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing @@ -443,7 +491,7 @@ In this definition the function @{term nth_of} returns the @{text n}th element from a list, provided it exists (@{term Some}-case), or if it does not, it returns the default action @{term Nop} and the default state @{text 0} - (@{term None}-case). We often need to restrict Turing machine programs + (@{term None}-case). We often have to restrict Turing machine programs to be well-formed: a program @{term p} is \emph{well-formed} if it satisfies the following three properties: @@ -638,10 +686,10 @@ \end{tikzpicture}\\[-8mm]\mbox{} \end{center} \caption{The three components of the \emph{copy Turing machine} (above). If started - (below) with the tape @{term "([], <[2::nat]>)"} the first machine appends @{term "[Bk, Oc]"} at + (below) with the tape @{term "([], <(2::nat)>)"} the first machine appends @{term "[Bk, Oc]"} at the end of the right tape; the second then ``moves'' all @{term Oc}s except the first from the beginning of the tape to the end; the third ``refills'' the original - block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <[2::nat, 2::nat]>)"}.} + block of @{term "Oc"}s. The resulting tape is @{term "([Bk], <(2::nat, 2::nat)>)"}.} \label{copy} \end{figure} @@ -649,10 +697,14 @@ We often need to restrict tapes to be in \emph{standard form}, which means the left list of the tape is either empty or only contains @{text "Bk"}s, and the right list contains some ``clusters'' of @{text "Oc"}s separted by single - blanks. To make this formal we define the following function + blanks. To make this formal we define the following overloaded function \begin{center} - \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} + \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} + @{thm (lhs) nats2tape(6)} & @{text "\"} & @{thm (rhs) nats2tape(6)}\\ + @{thm (lhs) nats2tape(4)} & @{text "\"} & @{thm (rhs) nats2tape(4)}\\ + \end{tabular}\hspace{6mm} + \begin{tabular}[t]{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{thm (lhs) nats2tape(1)} & @{text "\"} & @{thm (rhs) nats2tape(1)}\\ @{thm (lhs) nats2tape(2)} & @{text "\"} & @{thm (rhs) nats2tape(2)}\\ @{thm (lhs) nats2tape(3)} & @{text "\"} & @{thm (rhs) nats2tape(3)} @@ -666,10 +718,10 @@ is represented by a single filled cell on a standard tape, @{text 1} by two filled cells and so on. Before we can prove the undecidability of the halting problem for our - Turing machines, we need to analyse two concrete Turing machine + Turing machines, we have to analyse two concrete Turing machine programs and establish that they are correct---that means they are ``doing what they are supposed to be doing''. Such correctness proofs are usually left - out in the informal literature, for example \cite{Boolos87}. One program + out in the informal literature, for example \cite{Boolos87}. The first program we need to prove correct is the @{term dither} program shown in \eqref{dither} and the other program is @{term "tcopy"} defined as @@ -680,19 +732,18 @@ \end{equation} \noindent - whose three components are given in Figure~\ref{copy}. To the prove - 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}. - They implement the - idea that a program @{term p} started in state @{term "1::nat"} with - 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 \"} - 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 + whose three components are given in Figure~\ref{copy}. We introduce + the notion of total correctness defined in terms of + \emph{Hoare-triples}, written @{term "{P} p {Q}"} (this notion is + very similar to \emph{realisability} in \cite{AspertiRicciotti12}). + The Hoare-triples implement the idea that a program @{term p} + started in state @{term "1::nat"} with 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 \"} 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 \begin{center} \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} @@ -796,11 +847,11 @@ number of steps we can perform starting from the input tape. The program @{term tcopy} defined in \eqref{tcopy} has 15 states; - its purpose is to produce the standard tape @{term "(DUMMY, <[n, - n::nat]>)"} when started with @{term "(DUMMY, <[n::nat]>)"}, that is + its purpose is 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 prove the following two Hoare-rules for sequentially + burden, we derive the following two Hoare-rules for sequentially composed programs. \begin{center} @@ -825,23 +876,56 @@ 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 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}, + we define the following invariant for @{term "tcopy_begin"}. - 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 the details for - the program @{term "tcopy_begin"}. We found the following invariants for each - state: + \begin{figure} + \begin{center} + \begin{tabular}{@ {}lcl@ {\hspace{-2cm}}l@ {}} + @{thm (lhs) inv_begin0.simps} & @{text "\"} & @{thm (rhs) inv_begin01} @{text "\"}& (halting state)\\ + & & @{thm (rhs) inv_begin02} \\ + @{thm (lhs) inv_begin1.simps} & @{text "\"} & @{thm (rhs) inv_begin1.simps} & (starting state)\\ + @{thm (lhs) inv_begin2.simps} & @{text "\"} & @{thm (rhs) inv_begin2.simps}\\ + @{thm (lhs) inv_begin3.simps} & @{text "\"} & @{thm (rhs) inv_begin3.simps}\\ + @{thm (lhs) inv_begin4.simps} & @{text "\"} & @{thm (rhs) inv_begin4.simps} + \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} + \end{figure} \begin{center} - @{thm inv_begin0.simps}\\ - @{thm inv_begin1.simps}\\ - @{thm inv_begin2.simps}\\ - @{thm inv_begin3.simps}\\ - @{thm inv_begin4.simps} + \begin{tabular}{rcl} + @{thm (lhs) inv_begin.simps} & @{text "\"} & + @{text "if"} @{thm (prem 1) inv_begin_print(1)} @{text then} @{thm (rhs) inv_begin_print(1)}\\ + & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(2)} @{text then} @{thm (rhs) inv_begin_print(2)} \\ + & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(3)} @{text then} @{thm (rhs) inv_begin_print(3)}\\ + & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(4)} @{text then} @{thm (rhs) inv_begin_print(4)}\\ + & & @{text else} @{text "if"} @{thm (prem 1) inv_begin_print(5)} @{text then} @{thm (rhs) inv_begin_print(5)}\\ + & & @{text else} @{thm (rhs) inv_begin_print(6)} + \end{tabular} + \end{center} + + \noindent + This definition depends on @{term n}, which represents the number + of @{term Oc}s 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 @{term step} and @{term steps}. + + + measure for the copying TM, which we however omit. + + + \begin{center} + @{thm begin_correct}\\ + @{thm loop_correct}\\ + @{thm end_correct} \end{center} - measure for the copying TM, which we however omit. \begin{center} @{thm haltP_def[where lm="ns"]}