# HG changeset patch # User Christian Urban # Date 1361543494 0 # Node ID fc2a5e9fbb97a4a880fcf149e160a33728278330 # Parent 317a2532c567486b3ef62d2acd0beed385ee8cf8 updated Scala files diff -r 317a2532c567 -r fc2a5e9fbb97 Paper/Paper.thy --- a/Paper/Paper.thy Thu Feb 21 16:07:40 2013 +0000 +++ b/Paper/Paper.thy Fri Feb 22 14:31:34 2013 +0000 @@ -1220,7 +1220,10 @@ This gives us a list of natural numbers specifying how many states are needed to translate each abacus instruction. This information is needed in order to calculate the state where the Turing machine program - of one abacus instruction ends and the next starts. + of one abacus instruction starts. + + {\it add something here about address} + The @{text Goto} instruction is easiest to translate requiring only one state, namely the Turing machine program: @@ -1315,17 +1318,19 @@ \noindent where @{text n} indicates the function expects @{term n} arguments - (@{text z} and @{term s} expect one argument), and @{text rs} stands - for a list of recursive functions. Since we know in each case - the arity, say @{term l}, we can define an inductive evaluation relation that - relates a recursive function @{text r} and a list @{term ns} of natural numbers of length @{text l}, - to what the result of the recursive function is, say @{text n}. We omit the - definition of @{term "rec_calc_rel r ns n"}. Because of space reasons, we also omit the - definition of translating - recursive functions into abacus programs. We can prove, however, the following - theorem about the translation: If - @{thm (prem 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} - holds for the recursive function @{text r}, then the following Hoare-triple holds + (in \cite{Boolos87} both @{text z} and @{term s} expect one + argument), and @{text rs} stands for a list of recursive + functions. Since we know in each case the arity, say @{term l}, we + can define an inductive evaluation relation that relates a recursive + function @{text r} and a list @{term ns} of natural numbers of + length @{text l}, to what the result of the recursive function is, + say @{text n}. We omit the definition of @{term "rec_calc_rel r ns + n"}. Because of space reasons, we also omit the definition of + translating recursive functions into abacus programs. We can prove, + however, the following theorem about the translation: If @{thm (prem + 1) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and + r="n"]} holds for the recursive function @{text r}, then the + following Hoare-triple holds \begin{center} @{thm (concl) recursive_compile_to_tm_correct3[where recf="r" and args="ns" and r="n"]} diff -r 317a2532c567 -r fc2a5e9fbb97 paper.pdf Binary file paper.pdf has changed diff -r 317a2532c567 -r fc2a5e9fbb97 scala/abacus.scala --- a/scala/abacus.scala Thu Feb 21 16:07:40 2013 +0000 +++ b/scala/abacus.scala Fri Feb 22 14:31:34 2013 +0000 @@ -2,7 +2,7 @@ import lib._ -// Abacus machines +// Abacus instructions sealed abstract class AInst case class Inc(n: Int) extends AInst case class Dec(n: Int, l: Int) extends AInst @@ -11,10 +11,13 @@ type AProg = List[AInst] type Regs = Map[Int, Int] +// Abacus configurations case class AConfig(s: Int, regs: Regs) +// Abacus machines case class Abacus(p: AProg) { + //simple composition def ++ (that: Abacus) = Abacus(this.p ::: that.p) def shift(offset: Int, jump: Int) = Abacus(p.map(_ match { diff -r 317a2532c567 -r fc2a5e9fbb97 scala/comp1.scala --- a/scala/comp1.scala Thu Feb 21 16:07:40 2013 +0000 +++ b/scala/comp1.scala Fri Feb 22 14:31:34 2013 +0000 @@ -1,51 +1,52 @@ package object comp1 { +// Abacus to TM translation + import lib._ import turing._ import abacus._ // TMs used in the translation -val TMInc = TM(List((WOc, 1), (R, 2), (WOc, 3), (R, 2), (WOc, 3), (R, 4), - (L, 7), (WBk, 5), (R, 6), (WBk, 5), (WOc, 3), (R, 6), - (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (WBk, 9))) +val TMInc = TM((WOc, 1), (R, 2), (WOc, 3), (R, 2), (WOc, 3), (R, 4), + (L, 7), (WBk, 5), (R, 6), (WBk, 5), (WOc, 3), (R, 6), + (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (WBk, 9)) -val TMDec = TM(List((WOc, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3), - (R, 5), (WBk, 4), (R, 6), (WBk, 5), (L, 7), (L, 8), - (L, 11), (WBk, 7), (WOc, 8), (R, 9), (L, 10), (R, 9), - (R, 5), (WBk, 10), (L, 12), (L, 11), (R, 13), (L, 11), - (R, 17), (WBk, 13), (L, 15), (L, 14), (R, 16), (L, 14), - (R, 0), (WBk, 16))) +val TMDec = TM((WOc, 1), (R, 2), (L, 14), (R, 3), (L, 4), (R, 3), + (R, 5), (WBk, 4), (R, 6), (WBk, 5), (L, 7), (L, 8), + (L, 11), (WBk, 7), (WOc, 8), (R, 9), (L, 10), (R, 9), + (R, 5), (WBk, 10), (L, 12), (L, 11), (R, 13), (L, 11), + (R, 17), (WBk, 13), (L, 15), (L, 14), (R, 16), (L, 14), + (R, 0), (WBk, 16)) -val TMGoto = TM(List((Nop, 1), (Nop, 1))) +val TMGoto = TM((Nop, 1), (Nop, 1)) + +val TMMopup_aux = TM((R, 2), (R, 1), (L, 5), (WBk, 3), (R, 4), (WBk, 3), + (R, 2), (WBk, 3), (L, 5), (L, 6), (R, 0), (L, 6)) def TMFindnth(n: Int) : TM = n match { case 0 => TM(Nil) - case n => TMFindnth(n - 1) ++ TM(List((WOc, 2 * n - 1), (R, 2 * n), (R, 2 * n + 1), (R, 2 * n))) + case n => TMFindnth(n - 1) ++ TM((WOc, 2 * n - 1), (R, 2 * n), (R, 2 * n + 1), (R, 2 * n)) } def TMMopup(n: Int) = { def TMMopup1(n: Int) : TM = n match { case 0 => TM(Nil) - case n => TMMopup1(n - 1) ++ TM(List((R, 2 * n + 1), (WBk, 2 * n), (R, 2 * n - 1), (WOc, 2 * n))) + case n => TMMopup1(n - 1) ++ TM((R, 2 * n + 1), (WBk, 2 * n), (R, 2 * n - 1), (WOc, 2 * n)) } - - val TMMopup2 = TM(List((R, 2), (R, 1), (L, 5), (WBk, 3), (R, 4), (WBk, 3), - (R, 2), (WBk, 3), (L, 5), (L, 6), (R, 0), (L, 6))) - - TMMopup1(n) ++ TMMopup2.shift(2 * n) + TMMopup1(n) ++ TMMopup_aux.shift(2 * n) } - -// Abacus to TM translation -def layout(p: AProg) = p.map(_ match { - case Inc(n) => 2 * n + 9 - case Dec(n, _) => 2 * n + 16 - case Goto(n) => 1 -}) - -def start(p: AProg, n: Int) = layout(p).take(n).sum + 1 +// start address of the nth instruction +def address(p: AProg, n: Int) = { + def layout(p: AProg) = p.map(_ match { + case Inc(n) => 2 * n + 9 + case Dec(n, _) => 2 * n + 16 + case Goto(n) => 1 + }) + layout(p).take(n).sum + 1 +} def compile_Inc(s: Int, n: Int) = TMFindnth(n).shift(s - 1) ++ TMInc.shift(2 * n).shift(s - 1) @@ -57,15 +58,13 @@ def compile(p: AProg, s: Int, i: AInst) = i match { case Inc(n) => compile_Inc(s, n) - case Dec(n, e) => compile_Dec(s, n, start(p, e)) - case Goto(e) => compile_Goto(start(p, e)) + case Dec(n, e) => compile_Dec(s, n, address(p, e)) + case Goto(e) => compile_Goto(address(p, e)) } // component TMs for each instruction -def TMs(p: AProg) = { - val ss = (0 until p.length).map (start(p,_)) - (ss zip p).map{case (n, i) => compile(p, n, i)} -} +def TMs(p: AProg) = + p.zipWithIndex.map{case (i, n) => compile(p, address(p, n), i)} def toTM(p: AProg) = TMs(p).reduceLeft(_ ++ _) diff -r 317a2532c567 -r fc2a5e9fbb97 scala/ex.scala --- a/scala/ex.scala Thu Feb 21 16:07:40 2013 +0000 +++ b/scala/ex.scala Fri Feb 22 14:31:34 2013 +0000 @@ -4,16 +4,16 @@ import comp1._ // Turing machine examples -val TMCopy = TM(List((WBk, 5), (R, 2), (R, 3), (R, 2), (WOc, 3), - (L, 4), (L, 4), (L, 5), (R, 11), (R, 6), - (R, 7), (WBk, 6), (R, 7), (R, 8), (WOc, 9), - (R, 8), (L, 10), (L, 9), (L, 10), (L, 5), - (L, 0), (R, 12), (WOc, 13), (L, 14), (R, 12), - (R, 12), (L, 15), (WBk, 14), (R, 0), (L, 15))) +val TMCopy = TM((WBk, 5), (R, 2), (R, 3), (R, 2), (WOc, 3), + (L, 4), (L, 4), (L, 5), (R, 11), (R, 6), + (R, 7), (WBk, 6), (R, 7), (R, 8), (WOc, 9), + (R, 8), (L, 10), (L, 9), (L, 10), (L, 5), + (L, 0), (R, 12), (WOc, 13), (L, 14), (R, 12), + (R, 12), (L, 15), (WBk, 14), (R, 0), (L, 15)) println("TMCopy: " + (TMCopy.run(Tape(3)))) println("TMfindnth: " + (TMFindnth(3).run(Tape(1,2,3,4,5)))) -println("TMMopup: " + (TMMopup(3).run(Tape(1,2,3,4,5)))) +println("TMMopup: " + (TMMopup(3).run(Tape(1,2,3,4,5)))) // Abacus machine examples @@ -32,10 +32,10 @@ Copy(tmp2, out, -1).shift(10, -1). adjust(-1, 1) } -println("Copy: 3 " + (Copy(0, 1, -1).run(Map(0 -> 3, 1 -> 0)))) -println("Plus: 3 + 4 " + (Plus(0, 1, 2, -1).run(Map(0 -> 3, 1 -> 4, 2 -> 0)))) -println("Mult: 3 * 5 " + (Mult(0, 1, 2, 3, -1).run(Map(0 -> 3, 1 -> 5, 2 -> 0, 3 -> 0)))) -println("Expo: 3 ^ 4 " + (Expo(0, 1, 2, 3, 4, -1).run(Map(0 -> 4, 1 -> 3, 2 -> 0, 3 -> 0, 4 -> 0)))) +println("Copy 3: " + (Copy(0, 1, -1).run(Map(0 -> 3, 1 -> 0)))) +println("Plus 3 + 4: " + (Plus(0, 1, 2, -1).run(Map(0 -> 3, 1 -> 4, 2 -> 0)))) +println("Mult 3 * 5: " + (Mult(0, 1, 2, 3, -1).run(Map(0 -> 3, 1 -> 5, 2 -> 0, 3 -> 0)))) +println("Expo 3 ^ 4: " + (Expo(0, 1, 2, 3, 4, -1).run(Map(0 -> 4, 1 -> 3, 2 -> 0, 3 -> 0, 4 -> 0)))) // Abacus-to-TM translation examples diff -r 317a2532c567 -r fc2a5e9fbb97 scala/recs.scala --- a/scala/recs.scala Thu Feb 21 16:07:40 2013 +0000 +++ b/scala/recs.scala Fri Feb 22 14:31:34 2013 +0000 @@ -1,32 +1,37 @@ package object recs { +//Recursive Functions -//Recursive Functions abstract class Rec { def eval(ns: List[Int]) : Int } + case object Z extends Rec { override def eval(ns: List[Int]) = ns match { case n::Nil => 0 case _ => throw new IllegalArgumentException("Z: args") } } + case object S extends Rec { override def eval(ns: List[Int]) = ns match { case n::Nil => n + 1 case _ => throw new IllegalArgumentException("S: args") } } + case class Id(n: Int, m: Int) extends Rec { override def eval(ns: List[Int]) = if (ns.length == n && m < n) ns(m) else throw new IllegalArgumentException("Id: args") } + case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec { override def eval(ns: List[Int]) = if (ns.length == n) f.eval(gs.map(_.eval(ns))) else throw new IllegalArgumentException("Cn: args") } + case class Pr(n: Int, f: Rec, g: Rec) extends Rec { override def eval(ns: List[Int]) = if (ns.length == n - 1) { @@ -38,6 +43,7 @@ } else throw new IllegalArgumentException("Cn: args") } + case class Mn(n: Int, f: Rec) extends Rec { override def eval(ns: List[Int]) = 0 diff -r 317a2532c567 -r fc2a5e9fbb97 scala/turing.scala --- a/scala/turing.scala Thu Feb 21 16:07:40 2013 +0000 +++ b/scala/turing.scala Fri Feb 22 14:31:34 2013 +0000 @@ -3,6 +3,7 @@ import scala.annotation.tailrec import lib._ +// tape cells sealed abstract class Cell { def * (n: Int) : List[Cell] = n match { case 0 => Nil @@ -12,6 +13,7 @@ case object Bk extends Cell { override def toString = "0" } case object Oc extends Cell { override def toString = "1" } +// actions sealed abstract class Action case object WBk extends Action case object WOc extends Action @@ -23,7 +25,7 @@ type Inst = (Action, State) type Prog = List[Inst] -//tapes +// tapes case class Tape(l: List[Cell], r: List[Cell]) { def update(a: Action) = a match { @@ -42,13 +44,12 @@ override def toString = join(l.reverse) + ">" + join(r) } -//standard tapes +// standard tapes object Tape { def apply(ns: Int*) : Tape = Tape(Nil, ns.map(n => Oc * (n + 1)).reduceLeft(_ ::: List(Bk) ::: _)) } - // configurations case class Config(s: State, tp: Tape) { def is_final = s == 0 @@ -56,10 +57,10 @@ override def toString = tp.toString } - // Turing machines case class TM(p: Prog) { + // simple composition def ++ (that: TM) = TM(this.p ::: that.p) def shift(n: Int) = @@ -97,4 +98,9 @@ def run(tp: Tape) : Tape = run(Config(1, tp)).tp } +// some syntactical convenience +object TM { + def apply(is: Inst*) : TM = TM(is.toList) } + +}