--- 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], <ns::nat list>)"} will terminate
with the standard tape @{term "(Bk \<up> k, <n::nat> @ Bk \<up> 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/}.
*}
--- 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"]
Binary file paper.pdf has changed
--- 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)
+ \<Longrightarrow> 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)
+ \<Longrightarrow> 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)
+ \<Longrightarrow> 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)
+ \<Longrightarrow> wadjust_erase2 m rs (c, Bk # list)"
+apply(auto simp: wadjust_erase2.simps)
+done
+
lemma wadjust_correctness:
shows "let P = (\<lambda> (len, st, l, r). st = 0) in
let Q = (\<lambda> (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 \<noteq> []"
@@ -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: "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(l), <args>) tp stp))"
and args: "args \<noteq> []"
@@ -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) \<noteq> []"
+ and exec: "{(\<lambda>tp. tp = (Bk\<up>i, <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, Oc\<up>rs @ Bk\<up>k))}"
+ shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m n. tp = (Bk\<up>m, Oc\<up>rs @ Bk\<up>n)))}"
+proof -
+ have "{(\<lambda> (l, r). l = [] \<and> r = <code p # args>)} (t_wcode |+| t_utm)
+ {(\<lambda> (l, r). (\<exists> m. l = Bk\<up>m) \<and> (\<exists> n. r = Oc\<up>rs @ Bk\<up>n))}"
+ proof(rule_tac Hoare_plus_halt)
+ show "{\<lambda>(l, r). l = [] \<and> r = <code p # args>} t_wcode {\<lambda> (l, r). (l = [Bk] \<and>
+ (\<exists> rn. r = Oc\<up>(Suc (code p)) @ Bk # Oc\<up>(Suc (bl_bin (<args>))) @ Bk\<up>(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 "\<exists> stp. steps0 (Suc 0, Bk\<up>i, <args>) p stp = (0, Bk\<up>m, Oc\<up>rs @ Bk\<up>k)"
+ using exec
+ apply(simp add: Hoare_halt_def, auto)
+ apply(case_tac "steps0 (Suc 0, Bk \<up> i, <args>) p n", simp)
+ apply(rule_tac x = n in exI, simp)
+ done
+ then obtain stp where k: "steps0 (Suc 0, Bk\<up>i, <args>) p stp = (0, Bk\<up>m, Oc\<up>rs @ Bk\<up>k)"
+ ..
+ thus "{\<lambda>(l, r). l = [Bk] \<and> (\<exists>rn. r = Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn)}
+ t_utm {\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)}"
+ proof(rule_tac Hoare_haltI, auto)
+ fix rn
+ show "\<exists>n. is_final (steps0 (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> rn) t_utm n) \<and>
+ (\<lambda>(l, r). (\<exists>m. l = Bk \<up> m) \<and> (\<exists>n. r = Oc \<up> rs @ Bk \<up> n)) holds_for steps0
+ (Suc 0, [Bk], Oc \<up> Suc (code p) @ Bk # Oc \<up> Suc (bl_bin (<args>)) @ Bk \<up> 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, [], <code p # args>)
+ (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) \<noteq> []"
+ and exec: "{(\<lambda>tp. tp = ([], <args>))} p {(\<lambda>tp. tp = (Bk\<up>m, <(n::nat)> @ Bk\<up>k))}"
+ shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM {(\<lambda>tp. (\<exists> m k. tp = (Bk\<up>m, <n> @ Bk\<up>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: "{(\<lambda>tp. tp = (Bk\<up>i, <args>))} p \<up>"
+ and args: "args \<noteq> []"
+ shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
+proof -
+ have "\<forall> stp. (\<not> TSTD (steps0 (Suc 0, Bk\<up>(i), <args>) p stp))"
+ using unhalt
+ apply(auto simp: Hoare_unhalt_def)
+ apply(case_tac "steps0 (Suc 0, Bk \<up> i, <args>) p stp", simp)
+ apply(erule_tac x = stp in allE, simp add: TSTD_def)
+ done
+ then have "\<forall> stp. \<not> is_final (steps0 (Suc 0, [], <code p # args>) 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: "{(\<lambda>tp. tp = ([], <args>))} p \<up>"
+ and args: "args \<noteq> []"
+ shows "{(\<lambda>tp. tp = ([], <code p # args>))} UTM \<up>"
+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