tm: scala/recs.scala@09befdf4fc99 (annotated)

193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	package object recs {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	3	//Recursive Functions
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	abstract class Rec {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6	def eval(ns: List[Int]) : Int
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	7	def eval(ns: Int*) : Int = eval(ns.toList)
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	8
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	9	//syntactic convenience for composition
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	10	def o(r: Rec) = Cn(r.arity, this, List(r))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	11	def o(r: Rec, f: Rec) = Cn(r.arity, this, List(r, f))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	12	def o(r: Rec, f: Rec, g: Rec) = Cn(r.arity, this, List(r, f, g))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	13
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	14	def arity : Int
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	16
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	case object Z extends Rec {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	override def eval(ns: List[Int]) = ns match {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	case n::Nil => 0
198 d93cc4295306 tuned some files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 195 diff changeset	20	case _ => throw new IllegalArgumentException("Z args: " + ns)
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21	}
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	22	override def arity = 1
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	24
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25	case object S extends Rec {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	override def eval(ns: List[Int]) = ns match {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	case n::Nil => n + 1
198 d93cc4295306 tuned some files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 195 diff changeset	28	case _ => throw new IllegalArgumentException("S args: " + ns)
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	}
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	30	override def arity = 1
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	32
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	case class Id(n: Int, m: Int) extends Rec {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	override def eval(ns: List[Int]) =
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	if (ns.length == n && m < n) ns(m)
198 d93cc4295306 tuned some files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 195 diff changeset	36	else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	37
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	38	override def arity = n
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	40
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42	override def eval(ns: List[Int]) =
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	43	if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns)))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	44	else throw new IllegalArgumentException("Cn args: " + ns + "," + n)
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	45
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	46	override def arity = n
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	47	}
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	48
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	49	// syntactic convenience
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	50	object Cn {
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	51	def apply(n: Int, f: Rec, g: Rec) : Rec = new Cn(n, f, List(g))
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	53
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	54	case class Pr(n: Int, f: Rec, g: Rec) extends Rec {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	override def eval(ns: List[Int]) =
195 f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	56	if (ns.length == n + 1) {
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	57	if (ns.last == 0) f.eval(ns.init)
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	58	else {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59	val r = Pr(n, f, g).eval(ns.init ::: List(ns.last - 1))
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60	g.eval(ns.init ::: List(ns.last - 1, r))
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	}
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	62	}
195 f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	63	else throw new IllegalArgumentException("Pr: args")
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	64
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	65	override def arity = n + 1
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	66	}
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	67
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	68	// syntactic convenience
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	69	object Pr {
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	70	def apply(r: Rec, f: Rec) : Rec = Pr(r.arity, r, f)
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	71	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	72
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	73	case class Mn(n: Int, f: Rec) extends Rec {
195 f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	74	def evaln(ns: List[Int], n: Int) : Int =
f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	75	if (f.eval(ns ::: List(n)) == 0) n else evaln(ns, n + 1)
f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	76
f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	77	override def eval(ns: List[Int]) =
f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	78	if (ns.length == n) evaln(ns, 0)
f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	79	else throw new IllegalArgumentException("Mn: args")
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	80
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	81	override def arity = n
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	82	}
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	83
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	84
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	85
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	86	// Recursive Function examples
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	87	def Const(n: Int) : Rec = n match {
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	88	case 0 => Z
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	89	case n => S o Const(n - 1)
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90	}
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	91
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	92	val Add = Pr(Id(1, 0), S o Id(3, 2))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	93	val Mult = Pr(Z, Add o (Id(3, 0), Id(3, 2)))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	94	val Twice = Mult o (Id(1, 0), Const(2))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	95	val Fourtimes = Mult o (Id(1, 0), Const(4))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	96	val Pred = Pr(Z, Id(3, 1)) o (Id(1, 0), Id(1, 0))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	97	val Minus = Pr(Id(1, 0), Pred o Id(3, 2))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	98	val Power = Pr(Const(1), Mult o (Id(3, 0), Id(3, 2)))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	99	val Fact = Pr(Const(1), Mult o (Id(3, 2), S o Id(3, 1))) o (Id(1, 0), Id(1, 0))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	100
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	101	val Sign = Minus o (Const(1), Minus o (Const(1), Id(1, 0)))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	102	val Less = Sign o (Minus o (Id(2, 1), Id(2, 0)))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	103	val Not = Minus o (Const(1), Id(1, 0))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	104	val Eq = Minus o (Const(1) o Id(2, 0),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	105	Add o (Minus o (Id(2, 0), Id(2, 1)),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	106	Minus o (Id(2, 1), Id(2, 0))))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	107	val Noteq = Not o (Eq o (Id(2, 0), Id(2, 1)))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	108	val Conj = Sign o (Mult o (Id(2, 0), Id(2, 1)))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	109	val Disj = Sign o (Add o (Id(2, 0), Id(2, 1)))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	110
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	111	def Nargs(n: Int, m: Int) : List[Rec] = m match {
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	112	case 0 => Nil
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	113	case m => Nargs(n, m - 1) ::: List(Id(n, m - 1))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	114	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	115
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	116	def Sigma(f: Rec) = {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	117	val ar = f.arity
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	118	Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	119	Add o (Id(ar + 1, ar),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	120	Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(S o (Id(ar + 1, ar - 1))))))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	121	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	122
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	123	def Accum(f: Rec) = {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	124	val ar = f.arity
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	125	Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	126	Mult o (Id(ar + 1, ar),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	127	Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(S o Id(ar + 1, ar - 1)))))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	128	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	129
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	130	def All(t: Rec, f: Rec) = {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	131	val ar = f.arity
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	132	Sign o (Cn(ar - 1, Accum(f), Nargs(ar - 1, ar - 1) ::: List(t)))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	133	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	134
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	135	def Ex(t: Rec, f: Rec) = {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	136	val ar = f.arity
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	137	Sign o (Cn(ar - 1, Sigma(f), Nargs(ar - 1, ar - 1) ::: List(t)))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	138	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	139
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	140	//Definition on page 77 of Boolos's book.
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	141	def Minr(f: Rec) = {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	142	val ar = f.arity
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	143	Sigma(All(Id(ar, ar - 1), Not o (Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar))))))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	144	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	145
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	146	//Definition on page 77 of Boolos's book.
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	147	def Maxr(f: Rec) = {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	148	val ar = f.arity
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	149	val rt = Id(ar + 1, ar - 1)
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	150	val rf1 = Less o (Id(ar + 2, ar + 1), Id(ar + 2, ar))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	151	val rf2 = Not o (Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1))))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	152	val Qf = Not o All(rt, Disj o (rf1, rf2))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	153	Cn(ar, Sigma(Qf), Nargs(ar, ar) ::: List(Id(ar, ar - 1)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	154	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	155
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	156
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	157	//Prime test
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	158	val Prime = Conj o (Less o (Const(1), Id(1, 0)),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	159	All(Minus o (Id(1, 0), Const(1)),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	160	All(Minus o (Id(2, 0), Const(1) o Id(2, 0)),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	161	Noteq o (Mult o (Id(3, 1), Id(3, 2)), Id(3, 0)))))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	162
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	163	//Returns the first prime number after n (very slow for n > 4)
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	164	val NextPrime = {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	165	val R = Conj o (Less o (Id(2, 0), Id(2, 1)), Prime o Id(2, 1))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	166	Minr(R) o (Id(1, 0), S o Fact)
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	167	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	168
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	169	val NthPrime = Pr(Const(2), NextPrime o Id(3, 2)) o (Id(1, 0), Id(1, 0))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	170
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	171	def Listsum(k: Int, m: Int) : Rec = m match {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	172	case 0 => Z o Id(k, 0)
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	173	case n => Add o (Listsum(k, n - 1), Id(k, n - 1))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	174	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	175
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	176	//strt-function on page 90 of Boolos, but our definition generalises
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	177	//the original one in order to deal with multiple input-arguments
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	178
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	179	def Strt(n: Int) = {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	180
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	181	def Strt_aux(l: Int, k: Int) : Rec = k match {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	182	case 0 => Z o Id(l, 0)
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	183	case n => {
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	184	val rec_dbound = Add o (Listsum(l, n - 1), Const(n - 1) o Id(l, 0))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	185	Add o (Strt_aux(l, n - 1),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	186	Minus o (Power o (Const(2) o Id(l, 0), Add o (Id(l, n - 1), rec_dbound)),
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	187	Power o (Const(2) o Id(l, 0), rec_dbound)))
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	188	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	189	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	190
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	191	def Rmap(f: Rec, k: Int) = (0 until k).map{i => f o Id(k, i)}.toList
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	192
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	193	Cn(n, Strt_aux(n, n), Rmap(S, n))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	194	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	195
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	196
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	197	//Mutli-way branching statement on page 79 of Boolos's book
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	198	def Branch(rs: List[(Rec, Rec)]) = {
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	199
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	200	def Branch_aux(rs: List[(Rec, Rec)], l: Int) : Rec = rs match {
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	201	case Nil => Z o Id(l, l - 1)
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	202	case (rg, rc)::recs => Add o (Mult o (rg, rc), Branch_aux(recs, l))
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	203	}
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	204
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	205	Branch_aux(rs, rs.head._1.arity)
200 8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	206	}
201 09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	207
09befdf4fc99 syntactic convenience for recursive functions Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 200 diff changeset	208	}

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 26 Feb 2013 23:44:57 +0000
changeset 201	09befdf4fc99
parent 200	8dde2e46c69d
child 238	6ea1062da89a
permissions	-rw-r--r--