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