39 } |
39 } |
40 |
40 |
41 case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec { |
41 case class Cn(n: Int, f: Rec, gs: List[Rec]) extends Rec { |
42 override def eval(ns: List[Int]) = |
42 override def eval(ns: List[Int]) = |
43 if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns))) |
43 if (ns.length == n && gs.forall(_.arity == n) && f.arity == gs.length) f.eval(gs.map(_.eval(ns))) |
44 else throw new IllegalArgumentException("Cn args: " + ns + "," + n) |
44 else { |
|
45 val msg = List("Cn f: " + f, |
|
46 "n: " + n, |
|
47 "f arity: " + f.arity, |
|
48 "ns-args: " + ns, |
|
49 "gs arities: " + gs.map(_.arity).mkString("\n"), |
|
50 "gs: " + gs.mkString(", ") |
|
51 ) |
|
52 throw new IllegalArgumentException(msg.mkString("\n")) |
|
53 } |
45 |
54 |
46 override def arity = n |
55 override def arity = n |
|
56 override def toString = f.toString + gs.map(_.toString).mkString ("(",", ", ")") |
47 } |
57 } |
48 |
58 |
49 // syntactic convenience |
59 // syntactic convenience |
50 object Cn { |
60 object Cn { |
51 def apply(n: Int, f: Rec, g: Rec) : Rec = new Cn(n, f, List(g)) |
61 def apply(n: Int, f: Rec, g: Rec) : Rec = new Cn(n, f, List(g)) |
58 else { |
68 else { |
59 val r = Pr(n, f, g).eval(ns.init ::: List(ns.last - 1)) |
69 val r = Pr(n, f, g).eval(ns.init ::: List(ns.last - 1)) |
60 g.eval(ns.init ::: List(ns.last - 1, r)) |
70 g.eval(ns.init ::: List(ns.last - 1, r)) |
61 } |
71 } |
62 } |
72 } |
63 else throw new IllegalArgumentException("Pr: args") |
73 else { |
|
74 val msg = List("Pr f: " + f, |
|
75 "g: " + g, |
|
76 "n: " + n, |
|
77 "f arity: " + f.arity, |
|
78 "g arity: " + g.arity, |
|
79 "ns-args: " + ns) |
|
80 throw new IllegalArgumentException(msg.mkString("\n")) |
|
81 } |
64 |
82 |
65 override def arity = n + 1 |
83 override def arity = n + 1 |
|
84 override def toString = "Pr(" + f.toString + ", " + g.toString + ")" |
66 } |
85 } |
67 |
86 |
68 // syntactic convenience |
87 // syntactic convenience |
69 object Pr { |
88 object Pr { |
70 def apply(r: Rec, f: Rec) : Rec = Pr(r.arity, r, f) |
89 def apply(r: Rec, f: Rec) : Rec = Pr(r.arity, r, f) |
105 Add o (Minus o (Id(2, 0), Id(2, 1)), |
124 Add o (Minus o (Id(2, 0), Id(2, 1)), |
106 Minus o (Id(2, 1), Id(2, 0)))) |
125 Minus o (Id(2, 1), Id(2, 0)))) |
107 val Noteq = Not o (Eq o (Id(2, 0), Id(2, 1))) |
126 val Noteq = Not o (Eq o (Id(2, 0), Id(2, 1))) |
108 val Conj = Sign o (Mult o (Id(2, 0), Id(2, 1))) |
127 val Conj = Sign o (Mult o (Id(2, 0), Id(2, 1))) |
109 val Disj = Sign o (Add o (Id(2, 0), Id(2, 1))) |
128 val Disj = Sign o (Add o (Id(2, 0), Id(2, 1))) |
|
129 val Le = Disj o (Less, Eq) |
110 |
130 |
111 def Nargs(n: Int, m: Int) : List[Rec] = m match { |
131 def Nargs(n: Int, m: Int) : List[Rec] = m match { |
112 case 0 => Nil |
132 case 0 => Nil |
113 case m => Nargs(n, m - 1) ::: List(Id(n, m - 1)) |
133 case m => Nargs(n, m - 1) ::: List(Id(n, m - 1)) |
114 } |
134 } |
115 |
135 |
116 def Sigma(f: Rec) = { |
136 def Sigma(f: Rec) = { |
117 val ar = f.arity |
137 val ar = f.arity |
|
138 println("sigma f-ar: " + ar) |
118 Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))), |
139 Pr(Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: List(Const(0) o Id(ar - 1, 0))), |
119 Add o (Id(ar + 1, ar), |
140 Add o (Id(ar + 1, ar), |
120 Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(S o (Id(ar + 1, ar - 1)))))) |
141 Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(S o (Id(ar + 1, ar - 1)))))) |
121 } |
142 } |
122 |
143 |
138 } |
159 } |
139 |
160 |
140 //Definition on page 77 of Boolos's book. |
161 //Definition on page 77 of Boolos's book. |
141 def Minr(f: Rec) = { |
162 def Minr(f: Rec) = { |
142 val ar = f.arity |
163 val ar = f.arity |
|
164 println("f-arity " + ar) |
|
165 println("Nargs " + Nargs(ar + 1, ar - 1) + " and " + List(Id(ar + 1, ar))) |
143 Sigma(All(Id(ar, ar - 1), Not o (Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar)))))) |
166 Sigma(All(Id(ar, ar - 1), Not o (Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar)))))) |
144 } |
167 } |
145 |
168 |
146 //Definition on page 77 of Boolos's book. |
169 //Definition on page 77 of Boolos's book. |
147 def Maxr(f: Rec) = { |
170 def Maxr(f: Rec) = { |
148 val ar = f.arity |
171 val ar = f.arity |
149 val rt = Id(ar + 1, ar - 1) |
172 val rt = Id(ar + 1, ar - 1) |
150 val rf1 = Less o (Id(ar + 2, ar + 1), Id(ar + 2, ar)) |
173 val rf1 = Le o (Id(ar + 2, ar + 1), Id(ar + 2, ar)) |
151 val rf2 = Not o (Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1)))) |
174 val rf2 = Not o (Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1)))) |
152 val Qf = Not o All(rt, Disj o (rf1, rf2)) |
175 val Qf = Not o All(rt, Disj o (rf1, rf2)) |
153 Cn(ar, Sigma(Qf), Nargs(ar, ar) ::: List(Id(ar, ar - 1))) |
176 Cn(ar, Sigma(Qf), Nargs(ar, ar) ::: List(Id(ar, ar - 1))) |
154 } |
177 } |
155 |
178 |
204 |
227 |
205 Branch_aux(rs, rs.head._1.arity) |
228 Branch_aux(rs, rs.head._1.arity) |
206 } |
229 } |
207 |
230 |
208 val Lg = { |
231 val Lg = { |
209 val rec_lgR = Less o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0)) |
232 val lgR = Le o (Power o (Id(3, 1), Id(3, 2)), Id(3, 0)) |
210 val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0)), |
233 val conR1 = Conj o (Less o (Const(1) o (Id(2, 0), Id(2, 0))), |
211 Less o (Const(1) o (Id(2, 0)), Id(2, 1)))) |
234 Less o (Const(1) o (Id(2, 0), Id(2, 1)))) |
212 val conR2 = Not o ConR1 |
235 val conR2 = Not o (conR1) |
213 Add o (Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), |
236 Add o (Mult o (conR1, Maxr(lgR) o (Id(2, 0), Id(2, 1), Id(2, 0))), |
214 Mult o (conR2, Constn(0) o (Id(2, 0)))) |
237 Mult o (conR2, Const(0) o (Id(2, 0)))) |
215 } |
238 } |
216 |
239 |
217 |
240 |
218 } |
241 } |