]> matita.cs.unibo.it Git - fireball-separation.git/blob - ocaml/problems.ml
New failing problem, which shows that we need to change special_k
[fireball-separation.git] / ocaml / problems.ml
1 open Lambda4;;
2 let magic strings = problem_of None [] strings;;
3 let solve_many = List.iter solve;;
4
5 let p2 = magic [ "x y"; "x z" ; "x (y z)"]
6
7 let p4 = magic
8   [ "x y"; "x (a. a x)" ; "y (y z)" ]
9
10 let p5 = magic
11   ["a (x. x a) b"; "b (x. x b) a"]
12 ;;
13
14 let p6 = magic
15   ["a (x. x a) b"; "b (x. x b) (c a)"]
16
17 ;;
18
19 let p7 = magic
20   ["a (x. (x a)(a x x a)(x x) )"]
21
22 ;;
23
24 let p8 = magic
25   ["x x (x x)"]
26
27 ;;
28
29 let p9 = magic
30   ["x x (x x x) (x x (x x)) (x x (x x x)) x x"]
31
32 ;;
33
34 let p10 = magic
35   ["x (y (x a b c))"]
36
37 ;;
38
39 let p11 = magic
40   ["x x"; "x (y.y)"]
41
42 ;;
43
44 let p12 = magic
45   ["x x (x x)"; "x x (x (y.y))"]
46
47 ;;
48
49 let p13 = magic
50   ["x x (x x (x x x x x (x x)))"]
51
52 ;;
53
54 let p14 = magic
55   ["a (a a (a (a a)) (a (a a)))"]
56
57 ;;
58
59 let p15 = magic
60   ["a (a (a a)) (a a (a a) (a (a (a a))) (a (a a)) (a a (a a) (a (a (a a))) (a (a a)))) (a a (a a) (a (a (a a))) (a (a a)))"]
61
62 ;;
63
64 let p16 = magic
65   ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"]
66
67 ;;
68
69 let p17 = magic
70   ["b a"; "b (c.a)"]
71
72 ;;
73
74 let p18 = magic
75   ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"]
76
77 ;;
78
79 let p19 = magic
80   ["a (a a) (a a a (a (a (a a) a)) a)"]
81
82 ;;
83
84 let p20 = magic
85   ["a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))"];;
86
87 let p21 = magic
88   ["(((y z) (y z)) ((z (y z)) ((y z) (z z))))";
89    "(((z z) x) (y z))";
90    "((z (y z)) ((y z) (z z)))"
91 ] ;;
92
93 let p22 = magic
94 ["((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))";
95 "((z y) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) ((x y) (z z)))))";
96 "(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ;;
97
98 (* diverging tests *)
99 (* test p23 leads to test p24 *)
100 let p23 = magic
101 ["z z z"; "z (z z) (x. x)"] ;;
102
103 (* because of the last term, the magic number is 1 and we diverge;
104    but setting the magic number to 0 allows to solve the problem;
105    thus our strategy is incomplete *)
106 let p24 = magic
107 ["b b"; "b f"; "f b"; "a (x.x)"] ;;
108
109 (* because of the last term, the magic number is 1 and we diverge;
110    but setting the magic number to 0 allows to solve the problem;
111    thus our strategy is incomplete *)
112 let p25 = magic
113 ["b b"; "b f"; "f b"; "f (x.x)"] ;;
114
115 (* BUG:
116    0 (n (d (o.n) ...)))
117    After instantiating n, the magic number (for d) should be 2, not 1! *)
118 let p26 = magic
119 ["(((x y) (z. (y. (y. z)))) (z. y))";
120 "(((x y) x) (y y))"] ;;
121
122 let p27 = magic
123 ["(((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))))";
124 "((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))";
125 "(((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))"] ;;
126
127 let p28 = magic
128 ["((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))";
129  "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ;;
130
131 let p29 = magic
132 ["((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))";
133 "(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ;;
134
135 let p30 = magic
136 ["((b c) (b. (z a)))";
137 "((v (a. (z v))) ((y (b c)) ((z a) (v y))))";
138 "((v (v. c)) z)";
139 "((v y) (v (a. (z v))))";
140 "((y (b c)) ((z a) (v y)))"] ;;
141
142 let p31 = magic
143 [" (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))";
144 "((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))";
145 "(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))";
146 "(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))";
147 "((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"] ;;
148
149 let p32 = magic
150 ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
151 "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)";
152 "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
153 "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
154 "((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))"
155 ] ;;
156
157 (* Shows an error when the strategy that minimizes special_k is NOT used *)
158 let p33 = magic
159 [
160 "((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b))) (((y (y (v w))) z) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)))) (b c)) (((v w) (z (a (c. y)))) ((y b) (b (z (a (c. y)))))))";
161 "((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))";
162 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))";
163 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) (b (z (a (c. y))))) ((c b) (b. (b w))))";
164 (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)
165 ] ;;
166
167 let p34 = magic [
168 "b c (b c) (c (d (j. e))) (b c (b c) (j.c f)) (b f (j. k. d)) (b (j. k. l. b c (b c)) (b g)) a";
169 "d (j. e) e (j. c f) (j. c j) b a";
170 "d (j. e) e (j. c f) b (b c (b c) (j. c f)) a";
171 "d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a";
172 "d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a";
173 ] ;;
174 (* 0: (b c (b c) (c (d j.e)) (b c (b c) j.(c f)) (b f j.k.d) (b j.k.l.(b c (b c)) (b g)) a)
175 1: (d j.e e j.(c f) j.(c j) b a)
176 2: (d j.e e j.(c f) b (b c (b c) j.(c f)) a)
177 3: (d j.e e j.(c f) b (b c (b c) j.(c f) (g b)) a)
178 4: (d j.e e j.(c f) b j.k.(j l.e e l.(k f) b) a) *)
179
180 let p35 = magic [
181 "(((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (z (z b))) ((y y) (((b z) v) (a ((v (y y)) (v (y y)))))))";
182 "((((((((a b) z) w) (((b z) v) (a ((v (y y)) (v (y y)))))) ((y y) ((y (v (y y))) b))) ((((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) (((((c (a b)) (y y)) (y (v (y y)))) (z w)) ((w (((v (y y)) (v (y y))) a)) (w (z ((y (v (y y))) b)))))) (z w))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (c (a b)))) (((((b z) (c b)) (c ((v (y y)) (v (y y))))) (((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) ((c b) (z (z b))))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b)))))) (((((w ((a b) z)) (a ((v (y y)) (v (y y))))) (((v (y y)) (v (y y))) a)) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b))))))) (b z))) ((x ((c b) (c b))) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y))))))))))";
183 "((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (v (y y)))"
184 ] ;;
185
186 let p36 = magic
187 [
188 "(((((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (((y c) (x a)) (v (((y a) (((z v) (y a)) (b a))) z)))) ((b a) (b a))) ((a c) (b (((y a) (((z v) (y a)) (b a))) (z a))))) ((((((b (((y a) (((z v) (y a)) (b a))) z)) (c ((y (x a)) ((z v) (y a))))) (v (((y a) (((z v) (y a)) (b a))) z))) (((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))) ((x a) (((y a) (((z v) (y a)) (b a))) z)))) ((c ((y (x a)) ((z v) (y a)))) (b (((y a) (((z v) (y a)) (b a))) z)))) ((((b (z a)) (y a)) (y c)) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))))))))";
189 "(((((((z v) (y a)) (b a)) w) b) (((b a) ((((z v) (y a)) (b a)) w)) ((((z v) (y a)) (b a)) w))) (((b a) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) w)) (((c y) a) v)))";
190 "(((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x))"
191 ] ;;
192
193 (* issue with eta-equality of terms in ps *)
194 let p37 = magic
195   ["x (a y) z"; "x (a z. y z) w"; "a c"]
196   ;;
197
198 (**********************)
199
200 let q1 () = problem_of
201  None
202  ["a d e"]
203  ["a b"; "a c"]
204  ;;
205
206 let q2 () = problem_of
207  None
208  ["a d e"]
209  ["a b" ]
210  ;;
211
212 let q3 () = problem_of
213  (Some "x y")
214  ["a d e f"]
215  ["a b" ]
216  ;;
217
218 let q4 () = problem_of
219  None
220  ["f (x.a b c d)"]
221  ["a b" ]
222  ;;
223
224 let q5 () = problem_of
225  (Some"x y")
226  ["(y. x)"]
227  ["x"]
228  ;;
229
230 let q6 () = problem_of
231  (Some"x w")
232  ["(y. x z)"]
233  ["y"]
234  ;;
235
236 let q7 () = problem_of
237  (Some "(b (c d (e f f k.(g e))) f)")
238  ["(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (f d k.g (b (g (e f)) (b (g (e f)) (e f)) (g (e f) (g e h)))) k.l.(h f (b i)))";
239   "(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (b (g (e f))) k.l.(g f (k f f (k f f m.(g k)))))";
240   "(b (g (e f)) f k.e k.l.(f d (e f)) (c d (e f f k.(g e)) (g k.(e f f))) (h f (i (h k.(i b l.m.n.e)))))"]
241  ["(f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)";
242   "(f d (e f) k.e k.l.(c d) (b (g e) k.h) (d k.e) (f d (e f) k.e) a)";
243   "(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (g e h) (g f (e f f (e f f k.(g e))) (g (e f)) (b (c d (e f f k.(g e))) (b (g (e f)) (e f)) (b (g (e f)) k.l.e))) a)"]
244  ;;
245
246 (**********************)
247
248 let q8 () = problem_of
249  (Some"x a")
250  ["y (x b c)"] ["j"]
251 ;;
252
253 let q9 () = problem_of
254  (Some"x a")
255  ["y x"] ["a (y a b b b)"]
256 ;;
257
258 let q11 () = problem_of
259  (Some "x y")
260  ["a (x z)"] [] ;;
261
262 let q10 () = problem_of
263  (Some "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f)
264 (k. e (f g))) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b
265  (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c)))")
266 ["e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c))) (c f (k. b (l. c)) (k. l. b (m. c))) (k. l. b (m. c) d (l (f k) (m. k)) (m. n. c)) (c f (k. b (l. c)) (k. b (l. c) d) (k. c k))";
267 "e (f g) (k. g) (c f) (k. i) (k. l. h) (k. l. m. n. m) (b (k. c) (k. l. b (m. c)) (k. c f)) (k. l. m. k (f g) (n. g) (c f) (n. k))";
268 "b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c))";
269 "b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (b (k. c) (k. e) (k. l. m. b (n. c))) (e (f g) (k. g) (c f) (k. i) (k. l. h) (k. l. m. n. m) (b (k. c) (k. l. b (m. c)) (k. c f)) (k. l. m. k (f g) (n. g) (c f) (n. k)))";
270 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f) (k. e (f g)))"]
271 [
272 "b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))";
273 "b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c)))) (k. e (f g) (l. g) (c f) (l. k) (l. m. h))";
274 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. m. n. o. p. o) (e (f g) (k. g) (c f) (k. i) f)";
275 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)";
276 "e (f g) (k. g) (c f) (k. e) (k. b (l. c)) (c f (k. b (l. c)) (k. l. b (m. k))) (k. b (l. k)) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))";
277 ] ;;
278
279 let m1 () = problem_of None []
280  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
281
282 ;;
283
284 let m2 () = problem_of None []
285  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
286
287 ;;
288
289
290 let n1 () = problem_of (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (g (k. c e) (k. i) (c b) (f c) b)")
291 [
292 "b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. i))";
293 "g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. l. g (m. c e) (m. i) (c b) (l c) b) (e c (d d (d c)) (c e (k. f)) (b (c b) (k. l. c b d) (c e) (k. l. m. f)))";
294 "b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e))";
295 "b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. l. m. c c g) (e c (b (k. f))) (k. f c)";
296 "c (c e) (e c (d d (d c)) (k. c e (f c))) (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. c e (l. f) (k (l. c e) (l. i)))) (k. l. l (m. c e) (m. i) (c b) (f c) b) (k. l. c k) (f (f c) (b (c b) (k. l. c b d) (c e)) (b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. l. m. c c g) (e c (b (k. f)))))";
297 ] [
298 "b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (h (g (k. c e) (k. i) (c b) (c (c e)))) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a";
299 "c c g (k. b (c b) (l. m. c b k) (c e)) (k. b (c b) (l. m. c b d) (c k) b) (k. e c (d h) k) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a";
300 "d h (b (c b) (k. l. c b d) (c e)) (k. g (l. c e) (l. i) (c b) (k c) b) d b (b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (k. c)) a";
301 "g (k. c e) (k. d d) (k. k k) (e c (d d (d c)) i) (k. g (l. k e) (l. d d)) (g i (b (c b) (k. l. c b d) (e c (d d (d c)) (k. c e (f c)) (k. k (c k) (l. m. c k d) (c e) k (g (l. c e) (l. i) (c k)) (l. c))))) (c b) a";
302 "g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e) a"
303 ] ;;
304
305 let n2 () = problem_of
306 (Some"b b (c d) (k. d e) (k. k) (k. l. b)")
307 [
308 "b b (d e (k. d e)) (g (k. e) (k. k)) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (k. k (k k) (l. l))) (f (e (c d))) (b b (d e (k. d e)) (b b) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))))) (d e (k. d e) g (i (k. k)))";
309 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (d (g (de) (g (k. e)) h) (g (k. b b)))";
310 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. l. l) (k. g (d e) (l. m. m))";
311 "b b (d e (k. d e)) (g (k. e) (k. k)) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (k. k (k k) (l. l))) (f (e (c d))) (b b (d e (k. d e)) (b b) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h)))))";
312 "d (g (d e) (g (k. e)) h) (g (g (d e)) (d e (k. d e) (k. b (l. h)) (k. l. d e))) (b (k. h) (k. k e (l. m. b b)) (k. k (k k) (l. l))) (k. b) (b b (k. l. i)(k. c))";
313 ] [
314 "b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (e (b b (c d))) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (g (k. e) (k. k))) (k. l. d (g (d k) (g (m. k)) h) (d k (m. n. b b))) (e (c d) (e (c d))) a";
315 "d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) a";
316 "d e (k. d e) (k. b (l. h)) (k. l. d e) (d (g (d e) (g (k. e)) h) (g (d e) (k. l. l))) a";
317 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (k. l. m. b b) a";
318 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (b (b b) (d (g(d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (e (b b (c d))) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (g (k. e) (k. k)))) (k. d e (l. d e) f) a";
319 ]
320 ;;
321
322 let n3 () = problem_of
323 (Some"b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))")
324 [
325 "b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) (k. l. l (m. l))";
326 "c d e (f i) (e e) (g e) (k. l. e) (k. c (g (k (l. i)))) (c d e (k. k))";
327 "f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (c d e (f i) (e e) (f (k. h))) (g e (b (k. i)) (e e (e e)))";
328 "f (k. f) (k. f) (k. e) (c d e (f i) (e e) (g e)) (k. e e) (k. l. m. e) (k. e)";
329 "g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f)";
330 ][
331 "b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) a";
332 "c d e (f i) (e e) (g e) (b (g (k. e e)) (k. c (g (h (l. i))) (l. f l))) (k. f (l. f) (l. f)) a";
333 "e e (k. k d e (l. l)) (g e) (c d e b (e e (c (c d e f)))) (d (e e (k. k d e (l. l))) (k. k i)) (k. i (l. c (c d e f))) (k. h) a";
334 "f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a";
335 "g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f) (f (k. f) (k. f) (k. l. l) (c (k. i (l. c (c d e f))))) a";
336 ] ;;
337
338 (* ************************************************************************** *)
339
340 let o1 () = problem_of None [] ["x a b"; "x (_. BOT) c"] ;;
341 let o2 () = problem_of None [] ["x (y (_. BOT) a) c"; "x (y a PAC) d"] ;;
342 let o3 () = problem_of
343  (Some"y (x a1 BOMB c) (x BOMB b1 d)")
344  [ "y (x a2 BOMB c) (x BOMB b1 d)";
345  "y (x a1 BOMB c) (x BOMB b2 d)";] [] ;;
346 let o4 () = problem_of (Some"x BOMB a1 c")
347  [ "x y BOMB d"; "x BOMB a2 c" ] [] ;;
348 let o5 () = problem_of (Some"BOT") [] [] ;;
349 let o6 () = problem_of (Some"x BOMB") ["x y"] [];;
350
351 solve_many (List.map ((|>) ()) [
352  o1; o2; o3; o4; o5; o6
353 ]);;
354
355 should_fail(fun () -> problem_of None ["BOT"] []);;
356 should_fail(fun () -> problem_of (Some"x y") ["x BOMB"] []);;
357 should_fail(fun () -> problem_of (Some"x y z") ["x BOMB z"; "x y y"] []);;
358
359 solve_many [
360  problem_of
361  (* DISPLAY PROBLEM (main) - measure=965
362     Discriminating sets (deltas):
363     0 <> 1 <> 2 <> 3 <> 4
364  *)(* DIVERGENT  *)
365       (Some"b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (k. b c d (l. c (l k)) (b c (l. e e) (b c d (l. e l) (e e (b (l. m. b)) d (l. d))) (l. c)))")
366    (* CONVERGENT *) [
367    (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e) (k. g (l. g (m. b c)) (l. i (f g)))";
368    (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h))) (b c (k. c (e h)))";
369    (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e)";
370    (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h)))";
371    (* _ *) "b (k. l. b) (e f) (b c d) (e e (b (k. l. b)) d) (e (k. l. b c) (k. l. b k) (b c)) d (e e (e e) (d (k. f)) (b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))))) (e e (b (k. l. b)) (b (k. l. b) (e f) (b c
372  d)) (e e (b (k. l. b)) d (k. d) (b (k. l. b))) (k. b c k (l. e l) (e e (b (l. m. b)) k (l. k)) (f g (c (e h))) (k b (l. b) (f g (e f))) (c (e h))) (k. i (f g) (l. l)))";
373  ] (* NUMERIC    *) [
374    (* 0 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) a";
375    (* 1 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) a";
376    (* 2 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) a";
377    (* 3 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) a";
378    (* 4 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) a";
379  ];
380  (*problem_of
381  (* DISPLAY PROBLEM (main) - measure=561
382     Discriminating sets (deltas):
383     0 <> 1 <> 2 <> 3 <> 4
384  *)(* DIVERGENT  *)
385       (Some"b (c b) (k. d) (e f (k. e) (k. b) (f d)) (e f (k. g k) d) (k. c k (c k g))")
386    (* CONVERGENT *) [
387    (* _ *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g) (e f (k. k (g e) h) b (e (k. g) (h c (g c) f)))";
388    (* _ *) "e f (k. k) (k. l. c b) (k. l. l (k b) g) (k. e f (l. l)) (h c (c (k. l. l b k) (k. l. d) (e f (k. k) (g e))) (k. g e (g e))) (k. g (l. e f g) (l. h c) (g (l. e f g) (l. h c)))";
389    (* _ *) "e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (k. l. g l (g l) (m. c b))";
390    (* _ *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g)";
391    (* _ *) "e f (k. k) (g e) (e f (k. e)) (e f (k. e)) (h c (b (g e) h (k. c (l. m. m k l))))";
392  ] (* NUMERIC    *) [
393    (* 0 *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. i) a";
394    (* 1 *) "e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) a";
395    (* 2 *) "e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) a";
396    (* 3 *) "e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) a";
397    (* 4 *) "g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f a";
398  ]*)
399 ];;
400
401 (* This now fails *)
402 solve (problem_of
403  (Some"x PAC PAC PAC PAC PAC a")
404  ["x PAC PAC PAC PAC PAC b"]
405  ["y x"; "y z"]
406  (* In general:
407  DIV x (n times PAC) a
408  CON x (n times PAC) b
409  1 y (m times lambda. x) 0
410  2 y z 0
411  when x steps on the n+1-th argument,
412  y must apply n+m+1 variables
413  Thus special_k must be >=n+m+1 *)
414 );;
415
416 solve_many ([
417  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;
418  p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ;
419  p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ;
420  p34 ;
421  p35 ;
422  p36 ;
423  p37 ;
424  p24 ; p25 ;
425 ] @ List.map ((|>) ()) ([
426  q1 ; q2; q3; q4 ; q5 ; q6 ;
427  q7 ;
428  q8 ;
429  q9 ;
430  q10 ;
431  q11 ;
432  m1 ;
433  m2 ;
434 ] @ [
435  n1 ;
436  n2 ;
437  n3
438 ]));;