# HG changeset patch # User Christian Urban # Date 1360206111 0 # Node ID 38d8e0e37b7d5729222473a38e367bda4237c754 # Parent 07730607b0ca9cc48551029fe9515873fb0cebaf updated paper diff -r 07730607b0ca -r 38d8e0e37b7d Paper/Paper.thy --- a/Paper/Paper.thy Thu Feb 07 01:00:55 2013 +0000 +++ b/Paper/Paper.thy Thu Feb 07 03:01:51 2013 +0000 @@ -1,6 +1,6 @@ (*<*) theory Paper -imports "../thys/recursive" +imports "../thys/UTM" begin @@ -1329,6 +1329,33 @@ with the standard tape @{term "([Bk, Bk], )"} will terminate with the standard tape @{term "(Bk \ k, @ Bk \ l)"} for some @{text k} and @{text l}. + Having + + we can prove that if + + \begin{center} + @{thm (prem 3) UTM_halt_lemma2} + \end{center} + then + + \begin{center} + @{thm (concl) UTM_halt_lemma2} + \end{center} + + under the assumption that @{text p} + is well-formed and the arguments are not empty. + + + \begin{center} + @{thm (prem 2) UTM_unhalt_lemma2} + \end{center} + then + + \begin{center} + @{thm (concl) UTM_unhalt_lemma2} + \end{center} + + and the also the definition of the universal function (we refer the reader to our formalisation). @@ -1358,6 +1385,7 @@ but with @{term "([], [Oc])"} according to def Chap 8 *} +(* section {* XYZ *} text {* @@ -1406,6 +1434,7 @@ \] In summary, according to Chapter 3, the Turing machine in \eqref{contrived_tm} computes non-result and according to Chapter 8, it computes an identify function. *} +*) (* section {* Wang Tiles\label{Wang} *} @@ -1432,39 +1461,39 @@ We therefore have formalised Turing machines and the main computability results from Chapters 3 to 8 in the textbook by Boolos et al \cite{Boolos87}. For this we did not need to implement - anything on the ML-level of Isabelle/HOL. While formalising + anything on the ML-level of Isabelle/HOL. While formalising the six chapters \cite{Boolos87} we have found an inconsistency in Bolos et al's definitions of what function a Turing machine calculates. In Chapter 3 they use a definition that states a function is undefined if the Turing machine loops \emph{or} halts with a non-standard tape. Whereas in Chapter 8 about the universal Turing machine, the Turing machines will \emph{not} halt unless the tape is in standard - form. Following in the footsteps of another paper \cite{Nipkow98} - formalising the results from a semantics textbook, we could - therefore have titled our paper ``Boolos et al are (almost) + form. If the title had not already been taken \cite{Nipkow98}, we could + have titled our paper ``Boolos et al are (almost) Right''. We have not attempted to formalise everything precisely as Boolos et al present it, but use definitions that make our mechanised proofs manageable. For example our definition of the halting state performing @{term Nop}-operations seems to be non-standard, but very much suited to a formalisation in a theorem - prover where the @{term steps}-function need to be total. + prover where the @{term steps}-function needs to be total. - The most closely related work is by Norrish \cite{Norrish11}, and by - Asperti and Ricciotti \cite{AspertiRicciotti12}. Norrish mentions - that formalising Turing machines would be a ``daunting prospect'' + %The most closely related work is by Norrish \cite{Norrish11}, and by + %Asperti and Ricciotti \cite{AspertiRicciotti12}. + Norrish mentions + that formalising Turing machines would be a ``\emph{daunting prospect}'' \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to some slick mechanised proofs, our experience is that Turing machines are not too daunting if one is only concerned with formalising the undecidability of the halting problem for Turing machines. This took us around 1500 loc of Isar-proofs, which is just one-and-a-half times of a mechanised proof pearl about the Myhill-Nerode - theorem. So our conclusion is it not as daunting as we estimated - when reading the paper by Norrish \cite{Norrish11}. The work + theorem. So our conclusion is that it not as daunting for this part of the + work as we estimated when reading the paper by Norrish \cite{Norrish11}. The work involved with constructing a universal Turing machine via recursive - functions and abacus machines, on the other hand, is not a project + functions and abacus machines, we agree, is not a project one wants to undertake too many times (our formalisation of abacus machines and their correct translation is approximately 4300 loc; - recursive functions XX loc and the universal Turing machine XX loc). + recursive functions 5000 loc and the universal Turing machine 10000 loc). Our work was also very much inspired by the formalisation of Turing machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the @@ -1481,38 +1510,38 @@ For us the most interesting aspect of our work are the correctness proofs for Turing machines. Informal presentations of computability theory often leave the constructions of particular Turing machines - as exercise to the reader, as for example \cite{Boolos87}, deeming + as exercise to the reader, for example \cite{Boolos87}, deeming it to be just a chore. However, as far as we are aware all informal presentations leave out any arguments why these Turing machines - should be correct. This means the reader or formalsiser is left + should be correct. This means the reader is left with the task of finding appropriate invariants and measures for showing correctness and termination of these Turing machines. Whenever we can use Hoare-style reasoning, the invariants are relatively straightforward and much smaller than for example the invariants used by Myreen in a correctness proof of a garbage collector - written in machine code \cite[Page 76]{Myreen09}. Howvere, the invariant + written in machine code \cite[Page 76]{Myreen09}. However, the invariant needed for the abacus proof, where Hoare-style reasoning does not work, is similar in size as the one by Myreen and finding a sufficiently strong one took us, like Myreen for his, something on the magnitude of weeks. Our reasoning about the invariants is not much supported by the - automation in Isabelle. There is however a tantalising connection + automation beyond the standard automation tools available in Isabelle/HOL. + There is however a tantalising connection between our work and very recent work \cite{Jensen13} on verifying - X86 assembly code. They observed a similar phenomenon with assembly + X86 assembly code that might change that. They observed a similar phenomenon with assembly programs that Hoare-style reasoning is sometimes possible, but - sometimes it is not. In order to ease their reasoning they + sometimes it is not. In order to ease their reasoning, they introduced a more primitive specification logic, on which Hoare-rules can be provided for special cases. It remains to be seen whether their specification logic for assembly code can make it easier to reason about our Turing programs. That would be an attractive result, because Turing machine programs are very much - like assmbly programs and it would connect some very classic work on - Turing machines with very cutting-edge work on machine code + like assembly programs and it would connect some very classic work on + Turing machines to very cutting-edge work on machine code verification. In order to try out such ideas, our formalisation provides the ``playground''. The code of our formalisation is available from the - Mercurial repository at\\ - \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}. + Mercurial repository at \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/tm/}. *} diff -r 07730607b0ca -r 38d8e0e37b7d ROOT.ML --- a/ROOT.ML Thu Feb 07 01:00:55 2013 +0000 +++ b/ROOT.ML Thu Feb 07 03:01:51 2013 +0000 @@ -18,4 +18,5 @@ "thys/abacus", "thys/rec_def", "thys/recursive", - "thys/UF"] + "thys/UF", + "thys/UTM"] diff -r 07730607b0ca -r 38d8e0e37b7d paper.pdf Binary file paper.pdf has changed diff -r 07730607b0ca -r 38d8e0e37b7d thys/UTM.thy --- a/thys/UTM.thy Thu Feb 07 01:00:55 2013 +0000 +++ b/thys/UTM.thy Thu Feb 07 03:01:51 2013 +0000 @@ -3648,11 +3648,11 @@ apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps) done -lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc (Suc 0)))) Bk = (L, 8)" +lemma [simp]: "fetch t_wcode_adjust 4 Bk = (L, 8)" apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4) done -lemma [simp]: "fetch t_wcode_adjust (Suc (Suc (Suc (Suc 0)))) Oc = (L, 5)" +lemma [simp]: "fetch t_wcode_adjust 4 Oc = (L, 5)" apply(simp add: fetch.simps t_wcode_adjust_def nth_of.simps numeral_4_eq_4) done @@ -4471,6 +4471,30 @@ declare numeral_2_eq_2[simp del] +lemma [simp]: "wadjust_start m rs (c, Bk # list) + \ wadjust_start m rs (c, Oc # list)" +apply(auto simp: wadjust_start.simps) +done + +lemma [simp]: "wadjust_backto_standard_pos m rs (c, Bk # list) + \ wadjust_stop m rs (Bk # c, list)" +apply(auto simp: wadjust_backto_standard_pos.simps +wadjust_stop.simps wadjust_backto_standard_pos_B.simps) +done + +lemma [simp]: "wadjust_start m rs (c, Oc # list) + \ wadjust_loop_start m rs (Oc # c, list)" +apply(auto simp: wadjust_start.simps wadjust_loop_start.simps) +apply(rule_tac x = ln in exI, simp) +apply(rule_tac x = "rn" in exI, simp) +apply(rule_tac x = 1 in exI, simp) +done + +lemma [simp]:" wadjust_erase2 m rs (c, Oc # list) + \ wadjust_erase2 m rs (c, Bk # list)" +apply(auto simp: wadjust_erase2.simps) +done + lemma wadjust_correctness: shows "let P = (\ (len, st, l, r). st = 0) in let Q = (\ (len, st, l, r). wadjust_inv st m rs (l, r)) in @@ -4491,9 +4515,10 @@ apply(rule_tac allI, rule_tac impI, case_tac "?f n", simp) apply(simp add: step.simps) apply(case_tac d, case_tac [2] aa, simp_all) + apply(simp_all only: wadjust_inv.simps split: if_splits) + apply(simp_all) apply(simp_all add: wadjust_inv.simps wadjust_le_def - abacus.lex_triple_def abacus.lex_pair_def lex_square_def numeral_4_eq_4 - split: if_splits) + abacus.lex_triple_def abacus.lex_pair_def lex_square_def split: if_splits) done next show "?Q (?f 0)" @@ -4928,7 +4953,7 @@ text {* The correctness of @{text "UTM"}, the halt case. *} -lemma UTM_halt_lemma: +lemma UTM_halt_lemma': assumes tm_wf: "tm_wf (tp, 0)" and result: "0 < rs" and args: "args \ []" @@ -5291,7 +5316,7 @@ The correctness of @{text "UTM"}, the unhalt case. *} -lemma UTM_uhalt_lemma: +lemma UTM_uhalt_lemma': assumes tm_wf: "tm_wf (tp, 0)" and unhalt: "\ stp. (\ TSTD (steps0 (Suc 0, Bk\(l), ) tp stp))" and args: "args \ []" @@ -5301,4 +5326,101 @@ apply(case_tac "rec_ci rec_F", simp) done +lemma UTM_halt_lemma: + assumes tm_wf: "tm_wf (p, 0)" + and resut: "rs > 0" + and args: "(args::nat list) \ []" + and exec: "{(\tp. tp = (Bk\i, ))} p {(\tp. tp = (Bk\m, Oc\rs @ Bk\k))}" + shows "{(\tp. tp = ([], ))} UTM {(\tp. (\ m n. tp = (Bk\m, Oc\rs @ Bk\n)))}" +proof - + have "{(\ (l, r). l = [] \ r = )} (t_wcode |+| t_utm) + {(\ (l, r). (\ m. l = Bk\m) \ (\ n. r = Oc\rs @ Bk\n))}" + proof(rule_tac Hoare_plus_halt) + show "{\(l, r). l = [] \ r = } t_wcode {\ (l, r). (l = [Bk] \ + (\ rn. r = Oc\(Suc (code p)) @ Bk # Oc\(Suc (bl_bin ())) @ Bk\(rn)))}" + apply(rule_tac Hoare_haltI, auto) + using wcode_lemma_1[of args "code p"] args + apply(auto) + apply(rule_tac x = stp in exI, simp) + done + next + have "\ stp. steps0 (Suc 0, Bk\i, ) p stp = (0, Bk\m, Oc\rs @ Bk\k)" + using exec + apply(simp add: Hoare_halt_def, auto) + apply(case_tac "steps0 (Suc 0, Bk \ i, ) p n", simp) + apply(rule_tac x = n in exI, simp) + done + then obtain stp where k: "steps0 (Suc 0, Bk\i, ) p stp = (0, Bk\m, Oc\rs @ Bk\k)" + .. + thus "{\(l, r). l = [Bk] \ (\rn. r = Oc \ Suc (code p) @ Bk # Oc \ Suc (bl_bin ()) @ Bk \ rn)} + t_utm {\(l, r). (\m. l = Bk \ m) \ (\n. r = Oc \ rs @ Bk \ n)}" + proof(rule_tac Hoare_haltI, auto) + fix rn + show "\n. is_final (steps0 (Suc 0, [Bk], Oc \ Suc (code p) @ Bk # Oc \ Suc (bl_bin ()) @ Bk \ rn) t_utm n) \ + (\(l, r). (\m. l = Bk \ m) \ (\n. r = Oc \ rs @ Bk \ n)) holds_for steps0 + (Suc 0, [Bk], Oc \ Suc (code p) @ Bk # Oc \ Suc (bl_bin ()) @ Bk \ rn) t_utm n" + using t_utm_halt_eq[of p i "args" stp m rs k rn] assms k + apply(auto simp: bin_wc_eq, auto) + apply(rule_tac x = stpa in exI, simp add: tape_of_nl_abv tape_of_nat_abv) + done + qed + next + show "tm_wf0 t_wcode" by auto + qed + thus "?thesis" + apply(case_tac "rec_ci rec_F") + apply(simp add: UTM_def t_utm_def F_aprog_def F_tprog_def) + apply(auto simp add: Hoare_halt_def) + apply(rule_tac x="n" in exI) + apply(auto) + apply(case_tac "(steps0 (Suc 0, [], ) + (t_wcode |+| ((tm_of (a [+] dummy_abc (Suc (Suc 0)))) @ + shift (mopup (Suc (Suc 0))) + (length (tm_of (a [+] dummy_abc (Suc (Suc 0)))) div + 2))) n)") + apply(simp) + done +qed + +lemma UTM_halt_lemma2: + assumes tm_wf: "tm_wf (p, 0)" + and args: "(args::nat list) \ []" + and exec: "{(\tp. tp = ([], ))} p {(\tp. tp = (Bk\m, <(n::nat)> @ Bk\k))}" + shows "{(\tp. tp = ([], ))} UTM {(\tp. (\ m k. tp = (Bk\m, @ Bk\k)))}" +using UTM_halt_lemma[OF assms(1) _ assms(2), where i="0"] +using assms(3) +apply(simp add: tape_of_nat_abv) +done + + +lemma UTM_unhalt_lemma: + assumes tm_wf: "tm_wf (p, 0)" + and unhalt: "{(\tp. tp = (Bk\i, ))} p \" + and args: "args \ []" + shows "{(\tp. tp = ([], ))} UTM \" +proof - + have "\ stp. (\ TSTD (steps0 (Suc 0, Bk\(i), ) p stp))" + using unhalt + apply(auto simp: Hoare_unhalt_def) + apply(case_tac "steps0 (Suc 0, Bk \ i, ) p stp", simp) + apply(erule_tac x = stp in allE, simp add: TSTD_def) + done + then have "\ stp. \ is_final (steps0 (Suc 0, [], ) UTM stp)" + using assms + apply(rule_tac UTM_uhalt_lemma', simp_all) + done + thus "?thesis" + apply(simp add: Hoare_unhalt_def) + done +qed + +lemma UTM_unhalt_lemma2: + assumes tm_wf: "tm_wf (p, 0)" + and unhalt: "{(\tp. tp = ([], ))} p \" + and args: "args \ []" + shows "{(\tp. tp = ([], ))} UTM \" +using UTM_unhalt_lemma[OF assms(1), where i="0"] +using assms(2-3) +apply(simp add: tape_of_nat_abv) +done end \ No newline at end of file