# HG changeset patch # User Christian Urban # Date 1359306938 0 # Node ID 2068654bdf54ae2da3992265c915257218464aeb # Parent d2f4b775cd150ced3b539446c932c34d76657c35 updated paper diff -r d2f4b775cd15 -r 2068654bdf54 Paper/Paper.thy --- a/Paper/Paper.thy Sun Jan 27 15:46:32 2013 +0000 +++ b/Paper/Paper.thy Sun Jan 27 17:15:38 2013 +0000 @@ -34,7 +34,7 @@ tcopy ("copy") and tape_of ("\_\") and tm_comp ("_ \ _") and - DUMMY ("\<^raw:\mbox{$\_$}>") + DUMMY ("\<^raw:\mbox{$\_\!\_\,$}>") declare [[show_question_marks = false]] @@ -315,7 +315,8 @@ \noindent We slightly deviate - from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use + from the presentation in \cite{Boolos87} and \cite{AspertiRicciotti12} + by using the @{term Nop} operation; however its use will become important when we formalise halting computations and also universal Turing machines. Given a tape and an action, we can define the following tape updating function: @@ -522,9 +523,7 @@ halts, then in our setting the @{term steps}-evaluation does not actually halt, but rather transitions to the @{text 0}-state (the final state) and remains there performing @{text Nop}-actions until - @{text n} is reached. This is different from the setup in - \cite{AspertiRicciotti12} where an option is returned once a final - state is reached. + @{text n} is reached. \begin{figure}[t] \begin{center} @@ -668,11 +667,11 @@ we need to prove correct is the @{term dither} program shown in \eqref{dither} and the other program is @{term "tcopy"} defined as - \begin{center} - \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} + \begin{equation} + \mbox{\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}} @{thm (lhs) tcopy_def} & @{text "\"} & @{thm (rhs) tcopy_def} - \end{tabular} - \end{center} + \end{tabular}}\label{tcopy} + \end{equation} \noindent whose three components are given in Figure~\ref{copy}. To the prove @@ -776,7 +775,7 @@ \end{center} \noindent - We can prove the following formal statements + We can prove the following Hoare-statements: \begin{center} \begin{tabular}{l} @@ -786,19 +785,37 @@ \end{center} \noindent - {\it unfold} The first states that on a tape @{term "(Bk \ n, [Oc, Oc])"} - halts in tree steps leaving the tape unchanged. In the other states - that @{term dither} started with tape @{term "(Bk \ n, [Oc])"} loops. - + The first is by a simple calculation. The second is by induction on the + number of steps we can perform starting from the input tape. + The purpose of the @{term tcopy} program defined in \eqref{tcopy} 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 can prove + the following Hoare-rules for sequentially composed programs. - In the following we will consider the following Turing machine program - that makes a copies a value on the tape. - + \begin{center} + \begin{tabular}{@ {}p{3cm}@ {\hspace{9mm}}p{3cm}@ {}} + @{thm[mode=Rule] + Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]} + & + @{thm[mode=Rule] + Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]} + \end{tabular} + \end{center} - + \noindent + The first corresponds to the usual Hoare-rule for composition of imperative + programs, where @{term "Q\<^isub>1 \ P\<^isub>2"} means @{term "Q\<^isub>1"} implies @{term "P\<^isub>2"} for + all tapes @{term "(l, r)"}. The second rule covers the case where rughly the + first program terminates generating a tape for which the second program + loops. These are two cases we need in our proof for undecidability. - + 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 some details for the + the program @{term "tcopy_begin"}. assertion holds for all tapes @@ -813,21 +830,10 @@ measure for the copying TM, which we however omit. halting problem + + Magnus: invariants -- Section 5.4.5 on page 75. *} -text {* - \begin{center} - \begin{tabular}{@ {}p{3cm}p{3cm}@ {}} - @{thm[mode=Rule] - Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]} - & - @{thm[mode=Rule] - Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]} - \end{tabular} - \end{center} - - -*} section {* Abacus Machines *} diff -r d2f4b775cd15 -r 2068654bdf54 paper.pdf Binary file paper.pdf has changed diff -r d2f4b775cd15 -r 2068654bdf54 thys/uncomputable.thy --- a/thys/uncomputable.thy Sun Jan 27 15:46:32 2013 +0000 +++ b/thys/uncomputable.thy Sun Jan 27 17:15:38 2013 +0000 @@ -49,7 +49,7 @@ (R, 2), (R, 2), (L, 5), (W0, 4), (R, 0), (L, 5)]" -definition +idefinition tcopy :: "instr list" where "tcopy \ (tcopy_begin |+| tcopy_loop) |+| tcopy_end" @@ -81,16 +81,13 @@ if s = 4 then inv_begin4 n (l, r) else False)" - - lemma [elim]: "\0 < i; 0 < j\ \ \ia>0. ia + j - Suc 0 = i + j \ Oc # Oc \ i = Oc \ ia" apply(rule_tac x = "Suc i" in exI, simp) done lemma inv_begin_step: - "\inv_begin x cf; x > 0\ - \ inv_begin x (step cf (tcopy_begin, 0))" + "\inv_begin x cf; x > 0\ \ inv_begin x (step cf (tcopy_begin, 0))" unfolding tcopy_begin_def apply(case_tac cf) apply(auto simp: inv_begin.simps step.simps tcopy_begin_def numeral split: if_splits) @@ -139,7 +136,7 @@ by(auto intro:wf_inv_image simp:init_LE_def lex_pair_def) lemma init_halt: - "x > 0 \ \ stp. is_final (steps (Suc 0, [], Oc\x) (tcopy_begin, 0) stp)" + "x > 0 \ \ stp. is_final (steps0 (Suc 0, [], Oc\x) tcopy_begin stp)" proof(rule_tac LE = init_LE in halt_lemma) show "wf init_LE" by(simp add: wf_begin_le) next @@ -173,13 +170,12 @@ qed lemma init_correct: - "x > 0 \ {inv_begin1 x} tcopy_begin {inv_begin0 x}" + "0 < x \ {inv_begin1 x} tcopy_begin {inv_begin0 x}" proof(rule_tac Hoare_haltI) fix l r - assume h: "0 < x" - "inv_begin1 x (l, r)" - hence "\ stp. is_final (steps (Suc 0, [], Oc\x) (tcopy_begin, 0) stp)" - by(erule_tac init_halt) + assume h: "0 < x" "inv_begin1 x (l, r)" + hence "\ stp. is_final (steps0 (Suc 0, [], Oc \ x) tcopy_begin stp)" + by (rule_tac init_halt) then obtain stp where "is_final (steps (Suc 0, [], Oc\x) (tcopy_begin, 0) stp)" .. moreover have "inv_begin x (steps (Suc 0, [], Oc\x) (tcopy_begin, 0) stp)" apply(rule_tac inv_begin_steps) @@ -1004,7 +1000,7 @@ lemma dither_halts_aux: - shows "steps0 (1, Bk \ m, [Oc, Oc]) dither 3 = (0, Bk \ m, [Oc, Oc])" + shows "steps0 (1, Bk \ m, [Oc, Oc]) dither 2 = (0, Bk \ m, [Oc, Oc])" unfolding dither_def by (simp add: steps.simps step.simps numeral)