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")
 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")
 226  ["(y. x)"]
 227  ["x"]
 228  ;;
 229
 230 let q6 () = problem_of
 231  (Some"x")
 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  ]; problem_of
 380  (* DISPLAY PROBLEM (main) - measure=561
 381     Discriminating sets (deltas):
 382     0 <> 1 <> 2 <> 3 <> 4
 383  *)(* DIVERGENT  *)
 384       (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))")
 385    (* CONVERGENT *) [
 386    (* _ *) "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)))";
 387    (* _ *) "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)))";
 388    (* _ *) "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))";
 389    (* _ *) "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)";
 390    (* _ *) "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))))";
 391  ] (* NUMERIC    *) [
 392    (* 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";
 393    (* 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";
 394    (* 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";
 395    (* 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";
 396    (* 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";
 397  ]
 398 ];;
 399
 400 failwith "OKAy";;
 401
 402 solve_many ([
 403  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;
 404  p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ;
 405  p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ;
 406  p34 ;
 407  p35 ;
 408  p36 ;
 409  p37 ;
 410  p24 ; p25 ;
 411 ] @ List.map ((|>) ()) ([
 412  q1 ; q2; q3; q4 ; q5 ; q6 ;
 413  q7 ;
 414  q8 ;
 415  q9 ;
 416  q10 ;
 417  q11 ;
 418  m1 ;
 419  m2 ;
 420 ] @ [
 421  n1 ;
 422  n2 ;
 423  n3
 424 ]));;