tm: scala/recs.scala@8dde2e46c69d (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)
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	9
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	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	11	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	12	case n::Nil => 0
198 d93cc4295306 tuned some files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 195 diff changeset	13	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	14	}
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 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	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 => n + 1
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("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	21	}
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	23
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	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	25	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	26	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	27	else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	29
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	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	31	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	32	if (ns.length == n) f.eval(gs.map(_.eval(ns)))
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	else throw new IllegalArgumentException("Cn: args")
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	35
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	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	37	override def eval(ns: List[Int]) =
195 f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	38	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	39	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	40	else {
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	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	42	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	43	}
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44	}
195 f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	45	else throw new IllegalArgumentException("Pr: args")
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	}
194 fc2a5e9fbb97 updated Scala files Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 193 diff changeset	47
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	48	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	49	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	50	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	51
f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	52	override def eval(ns: List[Int]) =
f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	53	if (ns.length == n) evaln(ns, 0)
f06aa4e1c25b tuned Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 194 diff changeset	54	else throw new IllegalArgumentException("Mn: args")
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	55	}
317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	56
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	57
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	58
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	59	// Recursive Function examples
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	60	def arity(f: Rec) = f 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	61	case Z => 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	62	case S => 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	63	case Id(n, _) => 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	64	case Cn(n, _, _) => 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	65	case Pr(n, _, _) => n + 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	66	case Mn(n, _) => n
193 317a2532c567 split up scala-file into separate components Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	}
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	68
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	69	val Add = Pr(1, Id(1, 0), Cn(3, S, List(Id(3, 2))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	70	val Mult = Pr(1, Z, Cn(3, Add, List(Id(3, 0), Id(3, 2))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	71	val Twice = Cn(1, Mult, List(Id(1, 0), Const(2)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	72	val Fourtimes = Cn(1, Mult, List(Id(1, 0), Const(4)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	73	val Pred = Cn(1, Pr(1, Z, Id(3, 1)), List(Id(1, 0), Id(1, 0)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	74	val Minus = Pr(1, Id(1, 0), Cn(3, Pred, List(Id(3, 2))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	75	def Const(n: Int) : Rec = n 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	76	case 0 => Z
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	77	case n => Cn(1, S, List(Const(n - 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	78	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	79
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	80	val Power = Pr(1, Const(1), Cn(3, Mult, List(Id(3, 0), Id(3, 2))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	81	val Sign = Cn(1, Minus, List(Const(1), Cn(1, Minus, List(Const(1), Id(1, 0)))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	82	val Less = Cn(2, Sign, List(Cn(2, Minus, List(Id(2, 1), Id(2, 0)))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	83	val Not = Cn(1, Minus, List(Const(1), Id(1, 0)))
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	val Eq = Cn(2, Minus, List(Cn(2, Const(1), List(Id(2, 0))),
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	Cn(2, Add, List(Cn(2, Minus, List(Id(2, 0), Id(2, 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	86	Cn(2, Minus, List(Id(2, 1), Id(2, 0)))))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	87	val Noteq = Cn(2, Not, List(Cn(2, Eq, List(Id(2, 0), Id(2, 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	88	val Conj = Cn(2, Sign, List(Cn(2, Mult, List(Id(2, 0), Id(2, 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	89	val Disj = Cn(2, Sign, List(Cn(2, Add, List(Id(2, 0), Id(2, 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	90
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	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	92	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	93	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	94	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	95
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	96	def Sigma(f: Rec) = {
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	97	val ar = arity(f)
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	98	Pr(ar - 1, Cn(ar - 1, f, Nargs(ar - 1, 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	99	List(Cn(ar - 1, Const(0), List(Id(ar - 1, 0))))),
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	Cn(ar + 1, Add, List(Id(ar + 1, ar),
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	101	Cn(ar + 1, f, Nargs(ar + 1, 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	102	List(Cn(ar + 1, S, List(Id(ar + 1, 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	103	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	104
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	105	def Accum(f: Rec) = {
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	106	val ar = arity(f)
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	107	Pr(ar - 1, Cn(ar - 1, f, Nargs(ar - 1, 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	108	List(Cn(ar - 1, Const(0), List(Id(ar - 1, 0))))),
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	109	Cn(ar + 1, Mult, List(Id(ar + 1, ar),
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	Cn(ar + 1, f, Nargs(ar + 1, 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	111	List(Cn(ar + 1, S, List(Id(ar + 1, 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	112	}
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
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	def All(t: Rec, f: Rec) = {
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	val ar = arity(f)
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	Cn(ar - 1, Sign, List(Cn(ar - 1, Accum(f), Nargs(ar - 1, ar - 1) ::: List(t))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	117	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	118
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	119	def Ex(t: Rec, f: Rec) = {
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	120	val ar = arity(f)
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	Cn(ar - 1, Sign, List(Cn(ar - 1, Sigma(f), Nargs(ar - 1, ar - 1) ::: List(t))))
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
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	124	//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	125	def Minr(f: Rec) = {
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	126	val ar = arity(f)
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	127	val rq = All(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	128	Cn(ar + 1, Not, List(Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar))))))
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	Sigma(rq)
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	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	131
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	132	//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	133	def Maxr(f: Rec) = {
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	val ar = arity(f)
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	val rt = Id(ar + 1, 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	136	val rf1 = Cn(ar + 2, Less, List(Id(ar + 2, ar + 1), Id(ar + 2, ar)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	137	val rf2 = Cn(ar + 2, Not, List(Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, 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	138	val rf = Cn(ar + 2, Disj, List(rf1, rf2))
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	val rq = All(rt, rf)
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	val Qf = Cn(ar + 1, Not, List(rq))
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	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	142	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	143
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	//Mutli-way branching statement on page 79 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	145	def Branch(rs: List[(Rec, Rec)]) = {
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	val ar = arity(rs.head._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	147
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	148	def Branch_aux(rs: List[(Rec, Rec)], l: Int) : Rec = rs 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	149	case Nil => Cn(l, Z, List(Id(l, l - 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	150	case (rg, rc)::recs => Cn(l, Add, List(Cn(l, Mult, List(rg, rc)), Branch_aux(recs, l)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	151	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	152
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	Branch_aux(rs, ar)
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	//Factorial
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	val Fact = {
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	158	val Fact_aux = Pr(1, Const(1), Cn(3, Mult, List(Id(3, 2), Cn(3, S, List(Id(3, 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	159	Cn(1, Fact_aux, List(Id(1, 0), Id(1, 0)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	160	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	161
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	//Prime test
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	163	val Prime = Cn(1, Conj, List(Cn(1, Less, List(Const(1), Id(1, 0))),
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	All(Cn(1, Minus, List(Id(1, 0), Const(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	165	All(Cn(2, Minus, List(Id(2, 0), Cn(2, Const(1), List(Id(2, 0))))),
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	166	Cn(3, Noteq, List(Cn(3, Mult, List(Id(3, 1), Id(3, 2))), Id(3, 0)))))))
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	//Returns the first prime number after 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	169	val NextPrime = {
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	val R = Cn(2, Conj, List(Cn(2, Less, List(Id(2, 0), Id(2, 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	171	Cn(2, Prime, List(Id(2, 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	172	Cn(1, Minr(R), List(Id(1, 0), Cn(1, S, List(Fact))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	173	}
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	val NthPrime = {
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	val NthPrime_aux = Pr(1, Const(2), Cn(3, NextPrime, List(Id(3, 2))))
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	Cn(1, NthPrime_aux, List(Id(1, 0), Id(1, 0)))
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
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	180	def Listsum(k: Int, m: Int) : 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	181	case 0 => Cn(k, Z, List(Id(k, 0)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	182	case n => Cn(k, Add, List(Listsum(k, n - 1), Id(k, n - 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	183	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	184
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	185	//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	186	//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	187
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	def Strt(n: Int) = {
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	def Strt_aux(l: Int, k: Int) : Rec = k 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	190	case 0 => Cn(l, Z, List(Id(l, 0)))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	191	case 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	192	val rec_dbound = Cn(l, Add, List(Listsum(l, n - 1), Cn(l, Const(n - 1), List(Id(l, 0)))))
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(l, Add, List(Strt_aux(l, n - 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	194	Cn(l, Minus, List(Cn(l, Power, List(Cn(l, Const(2), List(Id(l, 0))),
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	Cn(l, Add, List(Id(l, n - 1), rec_dbound)))),
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	196	Cn(l, Power, List(Cn(l, Const(2), List(Id(l, 0))), rec_dbound))))))
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	197	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	198	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	199
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	200	def Rmap(f: Rec, k: Int) = (0 until k).map{i => Cn(k, f, List(Id(k, i)))}.toList
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	201
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	202	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	203	}
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	204
8dde2e46c69d added all recursive functions needed for the UF Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 198 diff changeset	205	}

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Tue, 26 Feb 2013 17:39:47 +0000
changeset 200	8dde2e46c69d
parent 198	d93cc4295306
child 201	09befdf4fc99
permissions	-rw-r--r--