193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
package object recs {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
3 |
//Recursive Functions
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
abstract class Rec {
|
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>
diff
changeset
|
7 |
def eval(ns: Int*) : Int = eval(ns.toList)
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
9 |
//syntactic convenience for composition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
def o(r: Rec) = Cn(r.arity, this, List(r))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
def o(r: Rec, f: Rec) = Cn(r.arity, this, List(r, f))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
def o(r: Rec, f: Rec, g: Rec) = Cn(r.arity, this, List(r, f, g))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
def arity : Int
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
case object Z extends Rec {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
override def eval(ns: List[Int]) = ns match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
case n::Nil => 0
|
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
case _ => throw new IllegalArgumentException("Z args: " + ns)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
override def arity = 1
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
case object S extends Rec {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
override def eval(ns: List[Int]) = ns match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
case n::Nil => n + 1
|
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
case _ => throw new IllegalArgumentException("S args: " + ns)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
override def arity = 1
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
case class Id(n: Int, m: Int) extends Rec {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
override def eval(ns: List[Int]) =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
if (ns.length == n && m < n) ns(m)
|
198
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
36 |
else throw new IllegalArgumentException("Id args: " + ns + "," + n + "," + m)
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
37 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
override def arity = n
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
40 |
|
193
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 {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
override def eval(ns: List[Int]) =
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns)))
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
else {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
val msg = List("Cn f: " + f,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
46 |
"n: " + n,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
"f arity: " + f.arity,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
"ns-args: " + ns,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
"gs arities: " + gs.map(_.arity).mkString("\n"),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
"gs: " + gs.mkString(", ")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
throw new IllegalArgumentException(msg.mkString("\n"))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
55 |
override def arity = n
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
56 |
override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")")
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
57 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
59 |
// syntactic convenience
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
object Cn {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
def apply(n: Int, f: Rec, g: Rec) : Rec = new Cn(n, f, List(g))
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
case class Pr(n: Int, f: Rec, g: Rec) extends Rec {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
override def eval(ns: List[Int]) =
|
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
if (ns.length == n + 1) {
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
if (ns.last == 0) f.eval(ns.init)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
else {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
val r = Pr(n, f, g).eval(ns.init ::: List(ns.last - 1))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
g.eval(ns.init ::: List(ns.last - 1, r))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
71 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
}
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
73 |
else {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
74 |
val msg = List("Pr f: " + f,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
"g: " + g,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
76 |
"n: " + n,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
77 |
"f arity: " + f.arity,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
78 |
"g arity: " + g.arity,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
79 |
"ns-args: " + ns)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
80 |
throw new IllegalArgumentException(msg.mkString("\n"))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
81 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
82 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
83 |
override def arity = n + 1
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
84 |
override def toString = "Pr(" + f.toString + ", " + g.toString + ")"
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
85 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
// syntactic convenience
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
88 |
object Pr {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
def apply(r: Rec, f: Rec) : Rec = Pr(r.arity, r, f)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
90 |
}
|
194
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
92 |
case class Mn(n: Int, f: Rec) extends Rec {
|
195
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
def evaln(ns: List[Int], n: Int) : Int =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
94 |
if (f.eval(ns ::: List(n)) == 0) n else evaln(ns, n + 1)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
95 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
override def eval(ns: List[Int]) =
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
if (ns.length == n) evaln(ns, 0)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
else throw new IllegalArgumentException("Mn: args")
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
100 |
override def arity = n
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
102 |
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
104 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
105 |
// Recursive Function examples
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
106 |
def Const(n: Int) : Rec = n match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
107 |
case 0 => Z
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
case n => S o Const(n - 1)
|
193
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
}
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
110 |
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
111 |
val Add = Pr(Id(1, 0), S o Id(3, 2))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
112 |
val Mult = Pr(Z, Add o (Id(3, 0), Id(3, 2)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
113 |
val Twice = Mult o (Id(1, 0), Const(2))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
114 |
val Fourtimes = Mult o (Id(1, 0), Const(4))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
115 |
val Pred = Pr(Z, Id(3, 1)) o (Id(1, 0), Id(1, 0))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
116 |
val Minus = Pr(Id(1, 0), Pred o Id(3, 2))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
117 |
val Power = Pr(Const(1), Mult o (Id(3, 0), Id(3, 2)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
118 |
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>
diff
changeset
|
119 |
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
120 |
val Sign = Minus o (Const(1), Minus o (Const(1), Id(1, 0)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
121 |
val Less = Sign o (Minus o (Id(2, 1), Id(2, 0)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
val Not = Minus o (Const(1), Id(1, 0))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
123 |
val Eq = Minus o (Const(1) o Id(2, 0),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
124 |
Add o (Minus o (Id(2, 0), Id(2, 1)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
125 |
Minus o (Id(2, 1), Id(2, 0))))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
126 |
val Noteq = Not o (Eq o (Id(2, 0), Id(2, 1)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
127 |
val Conj = Sign o (Mult o (Id(2, 0), Id(2, 1)))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
128 |
val Disj = Sign o (Add o (Id(2, 0), Id(2, 1)))
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
129 |
val Le = Disj o (Less, Eq)
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
130 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
131 |
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>
diff
changeset
|
132 |
case 0 => Nil
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
133 |
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>
diff
changeset
|
134 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
135 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
136 |
def Sigma(f: Rec) = {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
137 |
val ar = f.arity
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
println("sigma f-ar: " + ar)
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
139 |
Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
140 |
Add o (Id(ar + 1, ar),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
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>
diff
changeset
|
142 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
143 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
144 |
def Accum(f: Rec) = {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
val ar = f.arity
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
146 |
Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
Mult o (Id(ar + 1, ar),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
148 |
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>
diff
changeset
|
149 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
150 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
151 |
def All(t: Rec, f: Rec) = {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
152 |
val ar = f.arity
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
153 |
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>
diff
changeset
|
154 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
155 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
156 |
def Ex(t: Rec, f: Rec) = {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
157 |
val ar = f.arity
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
158 |
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>
diff
changeset
|
159 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
160 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
161 |
//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>
diff
changeset
|
162 |
def Minr(f: Rec) = {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
val ar = f.arity
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
164 |
println("f-arity " + ar)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
165 |
println("Nargs " + Nargs(ar + 1, ar - 1) + " and " + List(Id(ar + 1, ar)))
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
166 |
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>
diff
changeset
|
167 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
168 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
//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>
diff
changeset
|
170 |
def Maxr(f: Rec) = {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
171 |
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>
diff
changeset
|
172 |
val rt = Id(ar + 1, ar - 1)
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
val rf1 = Le o (Id(ar + 2, ar + 1), Id(ar + 2, ar))
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
174 |
val rf2 = Not o (Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1))))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
175 |
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>
diff
changeset
|
176 |
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>
diff
changeset
|
177 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
178 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
179 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
180 |
//Prime test
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
181 |
val Prime = Conj o (Less o (Const(1), Id(1, 0)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
182 |
All(Minus o (Id(1, 0), Const(1)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
183 |
All(Minus o (Id(2, 0), Const(1) o Id(2, 0)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
184 |
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>
diff
changeset
|
185 |
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
186 |
//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>
diff
changeset
|
187 |
val NextPrime = {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
188 |
val R = Conj o (Less o (Id(2, 0), Id(2, 1)), Prime o Id(2, 1))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
189 |
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>
diff
changeset
|
190 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
191 |
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
192 |
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>
diff
changeset
|
193 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
194 |
def Listsum(k: Int, m: Int) : Rec = m match {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
195 |
case 0 => Z o Id(k, 0)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
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>
diff
changeset
|
197 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
198 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
199 |
//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>
diff
changeset
|
200 |
//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>
diff
changeset
|
201 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
202 |
def Strt(n: Int) = {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
203 |
|
200
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
204 |
def Strt_aux(l: Int, k: Int) : Rec = k match {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
205 |
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>
diff
changeset
|
206 |
case n => {
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
207 |
val rec_dbound = Add o (Listsum(l, n - 1), Const(n - 1) o Id(l, 0))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
208 |
Add o (Strt_aux(l, n - 1),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
209 |
Minus o (Power o (Const(2) o Id(l, 0), Add o (Id(l, n - 1), rec_dbound)),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
210 |
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>
diff
changeset
|
211 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
212 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
213 |
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
214 |
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>
diff
changeset
|
215 |
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
216 |
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>
diff
changeset
|
217 |
}
|
8dde2e46c69d
added all recursive functions needed for the UF
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
218 |
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
219 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
220 |
//Mutli-way branching statement on page 79 of Boolos's book
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
221 |
def Branch(rs: List[(Rec, Rec)]) = {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
222 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
223 |
def Branch_aux(rs: List[(Rec, Rec)], l: Int) : Rec = rs match {
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
224 |
case Nil => Z o Id(l, l - 1)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
225 |
case (rg, rc)::recs => Add o (Mult o (rg, rc), Branch_aux(recs, l))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
226 |
}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
227 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
228 |
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>
diff
changeset
|
229 |
}
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
230 |
|
238
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
231 |
val Lg = {
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
232 |
val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
233 |
val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))),
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
234 |
Less o (Const(1) o (Id(2, 0), Id(2, 1))))
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
235 |
val conR2 = Not o (conR1)
|
238
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
236 |
Add o (Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))),
|
239
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
237 |
Mult o (conR2, Const(0) o (Id(2, 0))))
|
201
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
238 |
}
|
238
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
239 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
240 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
241 |
}
|