1 package object recs2 {

     2 

     3 //Recursive Functions

     4 

     5 abstract class Rec {

     6   def eval(ns: List[Int]) : Int

     7   def eval(ns: Int*) : Int = eval(ns.toList)

     8 

     9   //syntactic convenience for composition

    10   def o(r: Rec) = Cn(r.arity, this, List(r))

    11   def o(r: Rec, f: Rec) = Cn(r.arity, this, List(r, f))

    12   def o(r: Rec, f: Rec, g: Rec) = Cn(r.arity, this, List(r, f, g))

    13   def o(r: Rec, f: Rec, g: Rec, h: Rec) = Cn(r.arity, this, List(r, f, g, h))

    14   def arity : Int

    15 }

    16 

    17 case object Z extends Rec {

    18   override def eval(ns: List[Int]) = ns match {

    19     case n::Nil => 0

    20     case _ => throw new IllegalArgumentException("Z args: " + ns)

    21   }

    22   override def arity = 1

    23 } 

    24 

    25 case object S extends Rec {

    26   override def eval(ns: List[Int]) = ns match {

    27     case n::Nil => n + 1

    28     case _ => throw new IllegalArgumentException("S args: " + ns)

    29   }

    30   override def arity = 1 

    31 } 

    32 

    33 case class Id(n: Int, m: Int) extends Rec {

    34   require(m < n, println("Id m < n:" + m + " " + n))

    35 

    36   override def eval(ns: List[Int]) = 

    37     if (ns.length == n && m < n) ns(m)

    38     else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)

    39 

    40   override def arity = n

    41 }

    42 

    43 case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {

    44   require(f.arity == gs.length, 

    45           println("CN " + f + "  " + gs.mkString(",") + "\n" + 

    46                   "f.arity gs.length:" + f.arity + " " + gs.length))

    47   

    48   override def eval(ns: List[Int]) = 

    49     if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns)))

    50     else { 

    51       val msg = List("Cn f: " + f, 

    52                      "n: " + n,

    53                      "f arity: " + f.arity, 

    54                      "ns-args: " + ns,

    55                      "gs arities: " + gs.map(_.arity).mkString(", "),

    56                      "gs: " + gs.mkString(", "),

    57                      "ns.length == n " + (ns.length == n).toString,

    58                      "gs.forall(_.arity == n) " + (gs.forall(_.arity == n)).toString,

    59                      "f.arity == gs.length " + (f.arity == gs.length).toString

    60                     )

    61       throw new IllegalArgumentException(msg.mkString("\n"))

    62     }

    63 

    64   override def arity = n

    65   override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")")

    66 }

    67 

    68 // syntactic convenience

    69 object Cn {

    70   def apply(n: Int, f: Rec, g: Rec) : Rec = new Cn(n, f, List(g))

    71 }

    72 

    73 case class Pr(n: Int, f: Rec, g: Rec) extends Rec {

    74   override def eval(ns: List[Int]) = 

    75     if (ns.length == n + 1) {

    76       if (ns.head == 0) f.eval(ns.tail)

    77       else {

    78         val r = Pr(n, f, g).eval(ns.head - 1 :: ns.tail)

    79         g.eval(ns.head - 1 :: r :: ns.tail)

    80       }

    81     }

    82     else {

    83       val msg = List("Pr f: " + f, 

    84                      "g: " + g,

    85                      "n: " + n,

    86                      "f arity: " + f.arity,

    87                      "g arity: " + g.arity,

    88                      "ns-args: " + ns)

    89       throw new IllegalArgumentException(msg.mkString("\n"))

    90     }

    91 

    92   override def arity = n + 1

    93   override def toString = "Pr(" + f.toString + ", " + g.toString + ")"

    94 }

    95 

    96 // syntactic convenience

    97 object Pr {

    98   def apply(r: Rec, f: Rec) : Rec = Pr(r.arity, r, f) 

    99 }

   100 

   101 case class Mn(n: Int, f: Rec) extends Rec {

   102   def evaln(ns: List[Int], n: Int) : Int = 

   103     if (f.eval(n :: ns) == 0) n else evaln(ns, n + 1)

   104 

   105   override def eval(ns: List[Int]) = 

   106     if (ns.length == n) evaln(ns, 0) 

   107     else throw new IllegalArgumentException("Mn: args")

   108 

   109   override def arity = n

   110 }

   111 

   112 object Mn {

   113   def apply(f: Rec) : Rec = Mn(f.arity - 1, f)

   114 }

   115 

   116 

   117 

   118 

   119 // Recursive Function examples

   120 def Const(n: Int) : Rec = n match {

   121   case 0 => Z

   122   case n => S o Const(n - 1)

   123 }

   124 

   125 def Swap(f: Rec) = f o (Id(2, 1), Id(2, 0))

   126 val Add = Pr(Id(1, 0), S o Id(3, 1))

   127 val Mult = Pr(Z, Add o (Id(3, 1), Id(3, 2)))

   128 val Power = Swap(Pr(Const(1), Mult o (Id(3, 1), Id(3, 2))))

   129 val Fact = (Pr (Const(1), Mult o (S o Id(3, 0), Id(3, 1)))) o (Id(1, 0), Id(1, 0))

   130 val Pred = Pr(Z, Id(3, 0)) o (Id(1, 0), Id(1, 0))

   131 val Minus = Swap(Pr(Id(1, 0), Pred o Id(3, 1)))

   132 

   133 val Sign = Minus o (Const(1), Minus o (Const(1), Id(1, 0)))

   134 val Not = Minus o (Const(1), Id(1, 0))

   135 val Eq = Minus o (Const(1) o Id(2, 0), Add o (Minus, Swap(Minus))) 

   136 val Noteq = Not o Eq 

   137 val Conj = Sign o Mult

   138 val Disj = Sign o Add 

   139 val Imp = Disj o (Not o Id(2, 0), Id(2, 1))

   140 val Ifz = Pr(Id(2, 0), Id(4, 3))

   141 val If = Ifz o (Not o Id(3, 0), Id(3, 1), Id (3, 2))

   142 

   143 val Less = Sign o (Swap(Minus))

   144 val Le = Disj o (Less, Eq)

   145 

   146 def Sigma1(f: Rec) = Pr(f o (Z o (Id(1, 0)), Id(1, 0)), 

   147                         Add o (Id(3, 1), f o (S o Id(3, 0), Id(3, 2))))

   148 def Sigma2(f: Rec) = Pr(f o (Z o (Id(2, 0)), Id(2, 0), Id(2, 1)), 

   149                         Add o (Id(4, 1), f o (S o Id(4, 0), Id(4, 2), Id(4, 3))))

   150 

   151 def Accum1(f: Rec) = Pr(f o (Z o (Id(1, 0)), Id(1, 0)), 

   152                         Mult o (Id(3, 1), f o (S o Id(3, 0), Id(3, 2))))

   153 def Accum2(f: Rec) = Pr(f o (Z o (Id(2, 0)), Id(2, 0), Id(2, 1)), 

   154                         Mult o (Id(4, 1), f o (S o Id(4, 0), Id(4, 2), Id(4, 3))))

   155 def Accum3(f: Rec) = Pr(f o (Z o (Id(3, 0)), Id(3, 0), Id(3, 1), Id(3, 2)), 

   156                         Mult o (Id(5, 1), f o (S o Id(5, 0), Id(5, 2), Id(5, 3), Id(5, 4))))

   157 

   158 def All1(f: Rec) = Sign o (Accum1(f))

   159 def All2(f: Rec) = Sign o (Accum2(f))

   160 def All3(f: Rec) = Sign o (Accum3(f))

   161 

   162 def All1_less(f: Rec) = {

   163   val cond1 = Eq o (Id(3, 0), Id(3, 1))

   164   val cond2 = f o (Id(3, 0), Id(3, 2))

   165   All2(Disj o (cond1, cond2)) o (Id(2, 0), Id(2, 0), Id(2, 1))

   166 }

   167 

   168 def All2_less(f: Rec) = {

   169   val cond1 = Eq o (Id(4, 0), Id(4, 1))

   170   val cond2 = f o (Id(4, 0), Id(4, 2), Id(4, 3))

   171   All3(Disj o (cond1, cond2)) o (Id(3, 0), Id(3, 0), Id(3, 1), Id(3, 2))

   172 }

   173 

   174 def Ex1(f: Rec) = Sign o (Sigma1(f))

   175 def Ex2(f: Rec) = Sign o (Sigma2(f))

   176 

   177 val Quo = {

   178   val lhs = S o (Id(3, 0))

   179   val rhs = Mult o (Id(3, 2), S o (Id(3, 1)))

   180   val cond = Eq o (lhs, rhs)

   181   val if_stmt = If o (cond, S o (Id(3, 1)), Id(3, 1))

   182   Pr(Z, if_stmt)

   183 }

   184 

   185 def Iter(f: Rec) = Pr(Id(1, 0), f o (Id(3, 1)))

   186 

   187 def Max1(f: Rec) = Pr(Z, Ifz o (f o (S o (Id(3, 0)), Id(3, 2)), S o (Id(3, 0)), Id(3, 1)))

   188 def Max2(f: Rec) = Pr(Z, Ifz o (f o (S o (Id(4, 0)), Id(4, 2), Id(4, 3)), S o (Id(4, 0)), Id(4, 1)))

   189  

   190 val Triangle = Quo o (Mult o (Id(1, 0), S), Const(2))

   191 

   192 val MaxTriangle = {

   193   val cond = Not o (Le o (Triangle o (Id(2, 0)), Id(2, 1))) 

   194   Max1(cond) o (Id(1, 0), Id(1, 0))

   195 }

   196 

   197 val MaxTriangle2 = {

   198   Pred o Mn(Le o (Triangle o (Id(2, 0)), Id(2, 1)))

   199 }

   200 

   201 case object MaxTriangleFast extends Rec {

   202   def triangle(n: Int) : Int = (n * (n + 1)) / 2

   203 

   204   def search(m: Int, n: Int) : Int = {

   205     if (triangle(n) > m) n - 1 else search(m, n + 1)

   206   }

   207 

   208   override def eval(ns: List[Int]) = ns match {

   209     case n::Nil => search(n, 0)

   210     case _ => throw new IllegalArgumentException("MT args: " + ns)

   211   }

   212 

   213   override def arity = 1

   214 }

   215 

   216 case object TriangleFast extends Rec {

   217   def triangle(n: Int) : Int = (n * (n + 1)) / 2

   218 

   219   override def eval(ns: List[Int]) = ns match {

   220     case n::Nil => triangle(n)

   221     case _ => throw new IllegalArgumentException("Tr args: " + ns)

   222   }

   223 

   224   override def arity = 1

   225 }

   226 

   227 //(0 until 200).map(MaxTriangleFast.eval(_))

   228 

   229 

   230 val Penc = Add o (TriangleFast o (Add o (Id(2, 0), Id(2, 1))), Id(2, 0))

   231 val Pdec1 = Minus o (Id(1, 0), Triangle o (MaxTriangle o (Id(1, 0)))) 

   232 val Pdec2 = Minus o (MaxTriangle o (Id(1, 0)), Pdec1 o (Id(1, 0))) 

   233 

   234 def Lenc(fs: List[Rec]) : Rec = fs match {

   235   case Nil => Z

   236   case f::fs => Penc o (S o (f), Lenc(fs))

   237 }

   238 

   239 val Ldec = Pred o (Pdec1 o (Swap (Iter(Pdec2))))

   240 

   241 val Within = Less o (Z o (Id(2, 0)), Swap (Iter(Pdec2)))

   242 val Enclen = (Max1(Not o (Within o (Id(2, 1), Pred o (Id(2, 0)))))) o (Id(1, 0), Id(1, 0))

   243  

   244 

   245 val Read = Ldec o (Id(1, 0), Const(0))

   246 val Write = Penc o (S o (Id(2, 0)), Pdec2 o (Id(2, 1)))

   247 

   248 val Newleft = {

   249   val cond0 = Eq o (Id(3, 2), Const(0))

   250   val cond1 = Eq o (Id(3, 2), Const(1))

   251   val cond2 = Eq o (Id(3, 2), Const(2))

   252   val cond3 = Eq o (Id(3, 2), Const(3))

   253   val case3 = Penc o (S o (Read o (Id(3, 1))), Id(3, 0)) 

   254   If o (cond0, 

   255         Id(3, 0),

   256         If o (cond1, 

   257               Id(3, 0),  

   258               If o (cond2, 

   259                     Pdec2 o (Id(3, 0)),

   260                     If o (cond3, case3, Id(3, 0)))))

   261 }

   262 

   263 val Newright = {

   264   val cond0 = Eq o (Id(3, 2), Const(0))

   265   val cond1 = Eq o (Id(3, 2), Const(1))

   266   val cond2 = Eq o (Id(3, 2), Const(2))

   267   val cond3 = Eq o (Id(3, 2), Const(3))

   268   val case2 = Penc o (S o (Read o (Id(3, 0))), Id(3, 1))

   269   If o (cond0, 

   270         Write o (Const(0), Id(3, 1)),

   271         If o (cond1, 

   272               Write o (Const(1), Id(3, 1)),  

   273               If o (cond2, 

   274                     case2,

   275                     If o (cond3, Pdec2 o (Id(3, 1)), Id(3, 0)))))

   276 }

   277 

   278 val Actn = Swap (Pr(Pdec1 o (Pdec1 o (Id(1, 0))), Pdec1 o (Pdec2 o (Id(3, 2)))))

   279 

   280 val Action = {

   281   val cond1 = Noteq o (Id(3, 1), Z)

   282   val cond2 = Within o (Id(3, 0), Pred o (Id(3, 1)))

   283   val if_branch = Actn o (Ldec o (Id(3, 0), Pred o (Id(3, 1))), Id(3, 2))

   284   If o (Conj o (cond1, cond2), if_branch, Const(4))

   285 }

   286 

   287 val Newstat = Swap (Pr (Pdec2 o (Pdec1 o (Id(1, 0))),

   288                         Pdec2 o (Pdec2 o (Id(3, 2)))))

   289 

   290 val Newstate = {

   291   val cond = Noteq o (Id(3, 1), Z)

   292   val if_branch = Newstat o (Ldec o (Id(3, 0), Pred o (Id(3, 1))), Id(3, 2))

   293   If o (cond, if_branch, Z)

   294 }

   295 

   296 val Conf = Lenc (List(Id(3, 0), Id(3, 1), Id(3, 2)))

   297 

   298 val State = Ldec o (Id(1, 0), Z)

   299 

   300 val Left = Ldec o (Id(1, 0), Const(1))

   301 

   302 val Right = Ldec o (Id(1, 0), Const(2))

   303 

   304 val Step = {

   305   val left = Left o (Id(2, 0))

   306   val right = Right o (Id(2, 0))

   307   val state = State o (Id(2, 0))

   308   val read = Read o (right)

   309   val action = Action o (Id(2, 1), state, read)

   310   val newstate = Newstate o (Id(2, 1), state, read)

   311   val newleft = Newleft o (left, right, action)

   312   val newright = Newright o (left, right, action) 

   313   Conf o (newstate, newleft, newright)

   314  } 

   315 

   316 val Steps = Pr (Id(2, 0), Step o (Id(4, 1), Id(4, 3)))

   317 

   318 val Stknum = Minus o (Sigma1(Ldec o (Id(2, 1), Id(2, 0))) o (Enclen o (Id(1, 0)), Id(1, 0)),

   319                       Ldec o (Id(1, 0), Enclen o (Id(1, 0))))

   320 

   321 val Right_std = {

   322   val bound = Enclen o (Id(1, 0))

   323   val cond1 = Le o (Const(1) o (Id(2, 0)), Id(2, 0))

   324   val cond2 = All1_less (Eq o (Ldec o (Id(2, 1), Id(2, 0)), Const(1)))

   325   val bound2 = Minus o (Enclen o (Id(2, 1)), Id(2, 0))

   326   val cond3 = 

   327     (All2_less (Eq o (Ldec o (Id(3, 2), Add o (Id(3, 1), Id(3, 0))), Z))) o (bound2, Id(2, 0), Id(2, 1)) 

   328   Ex1(Conj o (Conj o (cond1, cond2), cond3)) o (bound, Id(1, 0))

   329 }

   330 

   331 val Left_std = {

   332   val cond = Eq o (Ldec o (Id(2, 1), Id(2, 0)), Z)

   333   (All1_less(cond)) o (Enclen o (Id(1, 0)), Id(1, 0))

   334 }

   335 

   336 val Std = Conj o (Left_std o (Left o (Id(1, 0))), Right_std o (Right o (Id(1, 0))))

   337 

   338 val Final = Eq o (State o (Id(1, 0)), Z)

   339 

   340 val Stop = {

   341   val stps = Steps o (Id(3, 2), Id(3, 1), Id(3, 0))

   342   Conj o (Final o (stps), Std o (stps))

   343 }

   344 

   345 val Halt = Mn (Not o (Stop o (Id(3, 1), Id(3, 2), Id(3, 0))))

   346 

   347 val UF = Pred o (Stknum o (Right o (Steps o (Halt o (Id(2, 0), Id(2, 1)), Id(2, 1), Id(2, 0)))))

   348 

   349 }