51 override def eval(ns: List[Int]) = |
52 override def eval(ns: List[Int]) = |
52 if (ns.length == n) evaln(ns, 0) |
53 if (ns.length == n) evaln(ns, 0) |
53 else throw new IllegalArgumentException("Mn: args") |
54 else throw new IllegalArgumentException("Mn: args") |
54 } |
55 } |
55 |
56 |
56 } |
57 |
|
58 |
|
59 // Recursive Function examples |
|
60 def arity(f: Rec) = f match { |
|
61 case Z => 1 |
|
62 case S => 1 |
|
63 case Id(n, _) => n |
|
64 case Cn(n, _, _) => n |
|
65 case Pr(n, _, _) => n + 1 |
|
66 case Mn(n, _) => n |
|
67 } |
|
68 |
|
69 val Add = Pr(1, Id(1, 0), Cn(3, S, List(Id(3, 2)))) |
|
70 val Mult = Pr(1, Z, Cn(3, Add, List(Id(3, 0), Id(3, 2)))) |
|
71 val Twice = Cn(1, Mult, List(Id(1, 0), Const(2))) |
|
72 val Fourtimes = Cn(1, Mult, List(Id(1, 0), Const(4))) |
|
73 val Pred = Cn(1, Pr(1, Z, Id(3, 1)), List(Id(1, 0), Id(1, 0))) |
|
74 val Minus = Pr(1, Id(1, 0), Cn(3, Pred, List(Id(3, 2)))) |
|
75 def Const(n: Int) : Rec = n match { |
|
76 case 0 => Z |
|
77 case n => Cn(1, S, List(Const(n - 1))) |
|
78 } |
|
79 |
|
80 val Power = Pr(1, Const(1), Cn(3, Mult, List(Id(3, 0), Id(3, 2)))) |
|
81 val Sign = Cn(1, Minus, List(Const(1), Cn(1, Minus, List(Const(1), Id(1, 0))))) |
|
82 val Less = Cn(2, Sign, List(Cn(2, Minus, List(Id(2, 1), Id(2, 0))))) |
|
83 val Not = Cn(1, Minus, List(Const(1), Id(1, 0))) |
|
84 val Eq = Cn(2, Minus, List(Cn(2, Const(1), List(Id(2, 0))), |
|
85 Cn(2, Add, List(Cn(2, Minus, List(Id(2, 0), Id(2, 1))), |
|
86 Cn(2, Minus, List(Id(2, 1), Id(2, 0))))))) |
|
87 val Noteq = Cn(2, Not, List(Cn(2, Eq, List(Id(2, 0), Id(2, 1))))) |
|
88 val Conj = Cn(2, Sign, List(Cn(2, Mult, List(Id(2, 0), Id(2, 1))))) |
|
89 val Disj = Cn(2, Sign, List(Cn(2, Add, List(Id(2, 0), Id(2, 1))))) |
|
90 |
|
91 def Nargs(n: Int, m: Int) : List[Rec] = m match { |
|
92 case 0 => Nil |
|
93 case m => Nargs(n, m - 1) ::: List(Id(n, m - 1)) |
|
94 } |
|
95 |
|
96 def Sigma(f: Rec) = { |
|
97 val ar = arity(f) |
|
98 Pr(ar - 1, Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: |
|
99 List(Cn(ar - 1, Const(0), List(Id(ar - 1, 0))))), |
|
100 Cn(ar + 1, Add, List(Id(ar + 1, ar), |
|
101 Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: |
|
102 List(Cn(ar + 1, S, List(Id(ar + 1, ar - 1)))))))) |
|
103 } |
|
104 |
|
105 def Accum(f: Rec) = { |
|
106 val ar = arity(f) |
|
107 Pr(ar - 1, Cn(ar - 1, f, Nargs(ar - 1, ar - 1) ::: |
|
108 List(Cn(ar - 1, Const(0), List(Id(ar - 1, 0))))), |
|
109 Cn(ar + 1, Mult, List(Id(ar + 1, ar), |
|
110 Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: |
|
111 List(Cn(ar + 1, S, List(Id(ar + 1, ar - 1)))))))) |
|
112 } |
|
113 |
|
114 def All(t: Rec, f: Rec) = { |
|
115 val ar = arity(f) |
|
116 Cn(ar - 1, Sign, List(Cn(ar - 1, Accum(f), Nargs(ar - 1, ar - 1) ::: List(t)))) |
|
117 } |
|
118 |
|
119 def Ex(t: Rec, f: Rec) = { |
|
120 val ar = arity(f) |
|
121 Cn(ar - 1, Sign, List(Cn(ar - 1, Sigma(f), Nargs(ar - 1, ar - 1) ::: List(t)))) |
|
122 } |
|
123 |
|
124 //Definition on page 77 of Boolos's book. |
|
125 def Minr(f: Rec) = { |
|
126 val ar = arity(f) |
|
127 val rq = All(Id(ar, ar - 1), |
|
128 Cn(ar + 1, Not, List(Cn(ar + 1, f, Nargs(ar + 1, ar - 1) ::: List(Id(ar + 1, ar)))))) |
|
129 Sigma(rq) |
|
130 } |
|
131 |
|
132 //Definition on page 77 of Boolos's book. |
|
133 def Maxr(f: Rec) = { |
|
134 val ar = arity(f) |
|
135 val rt = Id(ar + 1, ar - 1) |
|
136 val rf1 = Cn(ar + 2, Less, List(Id(ar + 2, ar + 1), Id(ar + 2, ar))) |
|
137 val rf2 = Cn(ar + 2, Not, List(Cn (ar + 2, f, Nargs(ar + 2, ar - 1) ::: List(Id(ar + 2, ar + 1))))) |
|
138 val rf = Cn(ar + 2, Disj, List(rf1, rf2)) |
|
139 val rq = All(rt, rf) |
|
140 val Qf = Cn(ar + 1, Not, List(rq)) |
|
141 Cn(ar, Sigma(Qf), Nargs(ar, ar) ::: List(Id(ar, ar - 1))) |
|
142 } |
|
143 |
|
144 //Mutli-way branching statement on page 79 of Boolos's book |
|
145 def Branch(rs: List[(Rec, Rec)]) = { |
|
146 val ar = arity(rs.head._1) |
|
147 |
|
148 def Branch_aux(rs: List[(Rec, Rec)], l: Int) : Rec = rs match { |
|
149 case Nil => Cn(l, Z, List(Id(l, l - 1))) |
|
150 case (rg, rc)::recs => Cn(l, Add, List(Cn(l, Mult, List(rg, rc)), Branch_aux(recs, l))) |
|
151 } |
|
152 |
|
153 Branch_aux(rs, ar) |
|
154 } |
|
155 |
|
156 //Factorial |
|
157 val Fact = { |
|
158 val Fact_aux = Pr(1, Const(1), Cn(3, Mult, List(Id(3, 2), Cn(3, S, List(Id(3, 1)))))) |
|
159 Cn(1, Fact_aux, List(Id(1, 0), Id(1, 0))) |
|
160 } |
|
161 |
|
162 //Prime test |
|
163 val Prime = Cn(1, Conj, List(Cn(1, Less, List(Const(1), Id(1, 0))), |
|
164 All(Cn(1, Minus, List(Id(1, 0), Const(1))), |
|
165 All(Cn(2, Minus, List(Id(2, 0), Cn(2, Const(1), List(Id(2, 0))))), |
|
166 Cn(3, Noteq, List(Cn(3, Mult, List(Id(3, 1), Id(3, 2))), Id(3, 0))))))) |
|
167 |
|
168 //Returns the first prime number after n |
|
169 val NextPrime = { |
|
170 val R = Cn(2, Conj, List(Cn(2, Less, List(Id(2, 0), Id(2, 1))), |
|
171 Cn(2, Prime, List(Id(2, 1))))) |
|
172 Cn(1, Minr(R), List(Id(1, 0), Cn(1, S, List(Fact)))) |
|
173 } |
|
174 |
|
175 val NthPrime = { |
|
176 val NthPrime_aux = Pr(1, Const(2), Cn(3, NextPrime, List(Id(3, 2)))) |
|
177 Cn(1, NthPrime_aux, List(Id(1, 0), Id(1, 0))) |
|
178 } |
|
179 |
|
180 def Listsum(k: Int, m: Int) : Rec = m match { |
|
181 case 0 => Cn(k, Z, List(Id(k, 0))) |
|
182 case n => Cn(k, Add, List(Listsum(k, n - 1), Id(k, n - 1))) |
|
183 } |
|
184 |
|
185 //strt-function on page 90 of Boolos, but our definition generalises |
|
186 //the original one in order to deal with multiple input-arguments |
|
187 |
|
188 def Strt(n: Int) = { |
|
189 def Strt_aux(l: Int, k: Int) : Rec = k match { |
|
190 case 0 => Cn(l, Z, List(Id(l, 0))) |
|
191 case n => { |
|
192 val rec_dbound = Cn(l, Add, List(Listsum(l, n - 1), Cn(l, Const(n - 1), List(Id(l, 0))))) |
|
193 Cn(l, Add, List(Strt_aux(l, n - 1), |
|
194 Cn(l, Minus, List(Cn(l, Power, List(Cn(l, Const(2), List(Id(l, 0))), |
|
195 Cn(l, Add, List(Id(l, n - 1), rec_dbound)))), |
|
196 Cn(l, Power, List(Cn(l, Const(2), List(Id(l, 0))), rec_dbound)))))) |
|
197 } |
|
198 } |
|
199 |
|
200 def Rmap(f: Rec, k: Int) = (0 until k).map{i => Cn(k, f, List(Id(k, i)))}.toList |
|
201 |
|
202 Cn(n, Strt_aux(n, n), Rmap(S, n)) |
|
203 } |
|
204 |
|
205 } |