# HG changeset patch # User Christian Urban # Date 1366793340 -3600 # Node ID ac3309722536f885763ef5354ed02273d1fb6773 # Parent 6ea1062da89a1bb1e66ad286445defa117c09a2e updated diff -r 6ea1062da89a -r ac3309722536 Paper/Paper.thy --- a/Paper/Paper.thy Mon Apr 22 10:33:40 2013 +0100 +++ b/Paper/Paper.thy Wed Apr 24 09:49:00 2013 +0100 @@ -191,75 +191,10 @@ apply(arith)+ done -(* -lemma "run tcopy (1, [], <0::nat>) = (0, [Bk], [Oc, Bk, Oc])" -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral del: run.simps) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral nth_of.simps del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) -apply(simp add: step.simps tcopy_def tcopy_begin_def tcopy_loop_def tcopy_end_def tm_comp.simps adjust.simps shift.simps tape_of_nat_abv fetch.simps numeral numeral2 del: run.simps) -apply(simp only: numeral[symmetric]) -apply(simp) -apply(subst run.simps) -apply(simp) +lemma tm_wf_simps: + "tm_wf0 p = (2 <=length p \ is_even(length p) \ (\(a,s) \ set p. s <= (length p) div 2))" +apply(simp add: tm_wf.simps) done -*) (*>*) @@ -420,7 +355,7 @@ turn recursive functions to abacus machines. The universal Turing machine can then be constructed by translating from a (universal) recursive function. The part of mechanising the translation of recursive function to register -machines has already been done by Zammit in HOL \cite{Zammit99}, +machines has already been done by Zammit in HOL4 \cite{Zammit99}, although his register machines use a slightly different instruction set than the one described in \cite{Boolos87}. @@ -506,12 +441,8 @@ \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l} @{text "a"} & $::=$ & @{term "W0"} & (write blank, @{term Bk})\\ & $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\ - \end{tabular} - \begin{tabular}[t]{rcl@ {\hspace{2mm}}l} & $\mid$ & @{term L} & (move left)\\ & $\mid$ & @{term R} & (move right)\\ - \end{tabular} - \begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}} & $\mid$ & @{term Nop} & (do-nothing operation)\\ \end{tabular} \end{center} @@ -645,7 +576,7 @@ satisfies the following three properties: \begin{center} - @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]} + @{thm tm_wf_simps[where p="p", THEN eq_reflection]} \end{center} \noindent @@ -903,17 +834,17 @@ \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} \begin{tabular}[t]{@ {}l@ {}} \colorbox{mygrey}{@{thm (lhs) Hoare_halt_def}} @{text "\"}\\[1mm] - \hspace{5mm}@{text "\"} @{term "(l, r)"}.\\ - \hspace{7mm}if @{term "P (l, r)"} holds then\\ - \hspace{7mm}@{text "\"} @{term n}. such that\\ - \hspace{7mm}@{text "is_final (steps (1, (l, r)) p n)"} \hspace{1mm}@{text "\"}\\ - \hspace{7mm}@{text "Q holds_for (steps (1, (l, r)) p n)"} + \hspace{5mm}@{text "\"}@{term "tp"}.\\ + \hspace{7mm}if @{term "P tp"} holds then\\ + \hspace{7mm}@{text "\"}@{term n}. such that\\ + \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\"}\\ + \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"} \end{tabular} & \begin{tabular}[t]{@ {}l@ {}} \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\"}\\[1mm] - \hspace{5mm}@{text "\"} @{term "(l, r)"}.\\ - \hspace{7mm}if @{term "P (l, r)"} holds then\\ - \hspace{7mm}@{text "\"} @{term n}. @{text "\ is_final (steps (1, (l, r)) p n)"} + \hspace{5mm}@{text "\"}@{term "tp"}.\\ + \hspace{7mm}if @{term "P tp"} holds then\\ + \hspace{7mm}@{text "\"}@{term n}. @{text "\ is_final (steps (1, tp) p n)"} \end{tabular} \end{tabular} \end{center} @@ -998,7 +929,7 @@ \end{center} \noindent - We can prove the following Hoare-statements: + We can prove the following two Hoare-statements: \begin{center} \begin{tabular}{l} @@ -1308,7 +1239,7 @@ Turing machine programs. Registers and their content are represented by standard tapes (see definition shown in \eqref{standard}). Because of the jumps in abacus programs, it is impossible to build Turing machine programs out of components - using our @{text "\"}-operation shown in the previous section. + using our @{text ";"}-operation shown in the previous section. To overcome this difficulty, we calculate a \emph{layout} of an abacus program as follows @@ -1465,13 +1396,13 @@ other is the ``packed version'' of the arguments of the Turing machine. We can then consider how this universal function is translated to a Turing machine and from this construct the universal Turing machine, - written @{term UTM}. @{text UTM} is defined as + written @{term UTM}. It is defined as the composition of the Turing machine that packages the arguments and the translated recursive function @{text UF}: \begin{center} - @{text "UTM \ arg_coding \ (translate UF)"} + @{text "UTM \ arg_coding ; (translate UF)"} \end{center} \noindent @@ -1656,11 +1587,11 @@ formula @{term "P \ \P"}. For reasoning about computability we need to formalise a concrete model of computations. We could have followed Norrish \cite{Norrish11} using the $\lambda$-calculus as - the starting point for computability theory, but then we would have + the starting point for formalising computability theory, but then we would have to reimplement on the ML-level his infrastructure for rewriting $\lambda$-terms modulo $\beta$-equality: HOL4 has a simplifer that can rewrite terms modulo an arbitrary equivalence relation, which - Isabelle unfortunately does not yet have. Even though we would + Isabelle unfortunately does not yet have. Even though, we would still need to connect $\lambda$-terms somehow to Turing machines for proofs that make essential use of them (for example the undecidability proof for Wang's tiling problem \cite{Robinson71}). diff -r 6ea1062da89a -r ac3309722536 paper.pdf Binary file paper.pdf has changed diff -r 6ea1062da89a -r ac3309722536 scala/ex.scala --- a/scala/ex.scala Mon Apr 22 10:33:40 2013 +0100 +++ b/scala/ex.scala Wed Apr 24 09:49:00 2013 +0100 @@ -5,6 +5,16 @@ import comp1._ import comp2._ +val Lg = { + val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0)) + val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), + Less o (Const(1) o (Id(2, 0), Id(2, 1)))) + val conR2 = Not o (conR1) + Add o (recs.Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), + recs.Mult o (conR2, Const(0) o (Id(2, 0)))) +} + + // Turing machine examples val TMCopy = TM((WBk, 5), (R, 2), (R, 3), (R, 2), (WOc, 3), @@ -65,6 +75,9 @@ println("Less 4 4: " + Less.eval(4, 4)) println("Less 4 6: " + Less.eval(4, 6)) println("Less 6 4: " + Less.eval(6, 4)) +println("Le 4 4: " + recs.Le.eval(4, 4)) +println("Le 4 6: " + recs.Le.eval(4, 6)) +println("Le 6 4: " + recs.Le.eval(6, 4)) println("Not 0: " + Not.eval(0)) println("Not 6: " + Not.eval(6)) println("Eq 4 4: " + Eq.eval(4, 4)) @@ -84,8 +97,16 @@ println("NextPrime 3: " + NextPrime.eval(3)) println("NthPrime 1: " + NthPrime.eval(1)) println("Listsum [2, 3, 4 , 5, 6]: " + Listsum(5, 4).eval(2, 3, 4, 5, 6)) -println("Strt: " + Strt(2).eval(2,3)) - +println("Strt: " + Strt(2).eval(2, 3)) +println("(<=5) 1: " + (Less o (Id(1, 0), Const(5))).eval(1)) +println("(<=5) 5: " + (Less o (Id(1, 0), Const(5))).eval(5)) +println("(<=5) 6: " + (Less o (Id(1, 0), Const(5))).eval(6)) +println("Max (<=9): " + Maxr(Le o (Id(1, 0), Const(9))).eval(10)) +println("Max (>=9): " + Maxr(Le o (Const(9), Id(1, 0))).eval(8)) +println("Min (>=9): " + Minr(Le o (Const(9), Id(1, 0))).eval(10)) +println("Min (<=9): " + Minr(Le o (Id(1, 0), Const(9))).eval(10)) +println("Min (>=9): " + Minr(Le o (Const(9), Id(1, 0))).eval(8)) +//println("Lg 4 2: " + Lg.eval(4, 2)) // compilation of rec to abacus tests def test_comp2(f: Rec, ns: Int*) = { diff -r 6ea1062da89a -r ac3309722536 scala/recs.scala --- a/scala/recs.scala Mon Apr 22 10:33:40 2013 +0100 +++ b/scala/recs.scala Wed Apr 24 09:49:00 2013 +0100 @@ -41,9 +41,19 @@ case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec { override def eval(ns: List[Int]) = if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns))) - else throw new IllegalArgumentException("Cn args: " + ns + "," + n) + else { + val msg = List("Cn f: " + f, + "n: " + n, + "f arity: " + f.arity, + "ns-args: " + ns, + "gs arities: " + gs.map(_.arity).mkString("\n"), + "gs: " + gs.mkString(", ") + ) + throw new IllegalArgumentException(msg.mkString("\n")) + } override def arity = n + override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")") } // syntactic convenience @@ -60,9 +70,18 @@ g.eval(ns.init ::: List(ns.last - 1, r)) } } - else throw new IllegalArgumentException("Pr: args") + else { + val msg = List("Pr f: " + f, + "g: " + g, + "n: " + n, + "f arity: " + f.arity, + "g arity: " + g.arity, + "ns-args: " + ns) + throw new IllegalArgumentException(msg.mkString("\n")) + } override def arity = n + 1 + override def toString = "Pr(" + f.toString + ", " + g.toString + ")" } // syntactic convenience @@ -107,6 +126,7 @@ val Noteq = Not o (Eq o (Id(2, 0), Id(2, 1))) val Conj = Sign o (Mult o (Id(2, 0), Id(2, 1))) val Disj = Sign o (Add o (Id(2, 0), Id(2, 1))) +val Le = Disj o (Less, Eq) def Nargs(n: Int, m: Int) : List[Rec] = m match { case 0 => Nil @@ -115,6 +135,7 @@ def Sigma(f: Rec) = { val ar = f.arity + println("sigma f-ar: " + ar) Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))), Add o (Id(ar + 1, ar), Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(S o (Id(ar + 1, ar - 1)))))) @@ -140,6 +161,8 @@ //Definition on page 77 of Boolos's book. def Minr(f: Rec) = { val ar = f.arity + println("f-arity " + ar) + println("Nargs " + Nargs(ar + 1, ar - 1) + " and " + List(Id(ar + 1, ar))) Sigma(All(Id(ar, ar - 1), Not o (Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar)))))) } @@ -147,7 +170,7 @@ def Maxr(f: Rec) = { val ar = f.arity val rt = Id(ar + 1, ar - 1) - val rf1 = Less o (Id(ar + 2, ar + 1), Id(ar + 2, ar)) + val rf1 = Le o (Id(ar + 2, ar + 1), Id(ar + 2, ar)) val rf2 = Not o (Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1)))) val Qf = Not o All(rt, Disj o (rf1, rf2)) Cn(ar, Sigma(Qf), Nargs(ar, ar) ::: List(Id(ar, ar - 1))) @@ -206,12 +229,12 @@ } val Lg = { - val rec_lgR = Less o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0)) - val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0)), - Less o (Const(1) o (Id(2, 0)), Id(2, 1)))) - val conR2 = Not o ConR1 + val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0)) + val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), + Less o (Const(1) o (Id(2, 0), Id(2, 1)))) + val conR2 = Not o (conR1) Add o (Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), - Mult o (conR2, Constn(0) o (Id(2, 0)))) + Mult o (conR2, Const(0) o (Id(2, 0)))) } diff -r 6ea1062da89a -r ac3309722536 thys/UF.thy --- a/thys/UF.thy Mon Apr 22 10:33:40 2013 +0100 +++ b/thys/UF.thy Wed Apr 24 09:49:00 2013 +0100 @@ -533,10 +533,9 @@ where "rec_Minr rf = (let vl = arity rf - in let rq = rec_all (id vl (vl - 1)) (Cn (Suc vl) - rec_not [Cn (Suc vl) rf - (get_fstn_args (Suc vl) (vl - 1) @ - [id (Suc vl) (vl)])]) + in let rq = rec_all (id vl (vl - 1)) + (Cn (Suc vl) rec_not [Cn (Suc vl) rf + (get_fstn_args (Suc vl) (vl - 1) @ [id (Suc vl) vl])]) in rec_sigma rq)" lemma length_getpren_params[simp]: "length (get_fstn_args m n) = n" @@ -766,13 +765,12 @@ "rec_maxr rr = (let vl = arity rr in let rt = id (Suc vl) (vl - 1) in let rf1 = Cn (Suc (Suc vl)) rec_le - [id (Suc (Suc vl)) - ((Suc vl)), id (Suc (Suc vl)) (vl)] in + [id (Suc (Suc vl)) (Suc vl), id (Suc (Suc vl)) vl] in let rf2 = Cn (Suc (Suc vl)) rec_not [Cn (Suc (Suc vl)) rr (get_fstn_args (Suc (Suc vl)) (vl - 1) @ - [id (Suc (Suc vl)) ((Suc vl))])] in + [id (Suc (Suc vl)) (Suc vl)])] in let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in let Qf = Cn (Suc vl) rec_not [rec_all rt rf] in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @ @@ -1948,10 +1946,8 @@ where "rec_lg = (let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in - let conR1 = Cn 2 rec_conj [Cn 2 rec_less - [Cn 2 (constn 1) [id 2 0], id 2 0], - Cn 2 rec_less [Cn 2 (constn 1) - [id 2 0], id 2 1]] in + let conR1 = Cn 2 rec_conj [Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 0], + Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 1]] in let conR2 = Cn 2 rec_not [conR1] in Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR) [id 2 0, id 2 1, id 2 0]],