--- 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"]}

Binary file paper.pdf has changed

--- 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 {

--- 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(_ ++ _)
     

--- 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

--- 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
     

--- 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)
 }
+
+}