ocaml/problems.ml

   1 let use_lambda3 = Array.length Sys.argv = 1;;
   2
   3 let discriminator =
   4  if use_lambda3 then (module Lambda3 : Discriminator.Discriminator) else (module Lambda4);;
   5 module Pippo = (val discriminator);;
   6 open Pippo;;
   7
   8 let p2 = magic [ "x y"; "x z" ; "x (y z)"] ["*"]
   9
  10 let p4 = magic
  11   [ "x y"; "x (a. a x)" ; "y (y z)" ] ["*"]
  12
  13 let p5 = magic
  14   ["a (x. x a) b"; "b (x. x b) a"]
  15   ["*"]
  16 ;;
  17
  18 let p6 = magic
  19   ["a (x. x a) b"; "b (x. x b) (c a)"]
  20   ["*"]
  21 ;;
  22
  23 let p7 = magic
  24   ["a (x. (x a)(a x x a)(x x) )"]
  25   ["*"]
  26 ;;
  27
  28 let p8 = magic
  29   ["x x (x x)"]
  30   ["*"]
  31 ;;
  32
  33 let p9 = magic
  34   ["x x (x x x) (x x (x x)) (x x (x x x)) x x"]
  35   ["*"]
  36 ;;
  37
  38 let p10 = magic
  39   ["x (y (x a b c))"]
  40   ["*"]
  41 ;;
  42
  43 let p11 = magic
  44   ["x x"; "x (y.y)"]
  45   ["*"]
  46 ;;
  47
  48 let p12 = magic
  49   ["x x (x x)"; "x x (x (y.y))"]
  50   ["*"]
  51 ;;
  52
  53 let p13 = magic
  54   ["x x (x x (x x x x x (x x)))"]
  55   ["*"]
  56 ;;
  57
  58 let p14 = magic
  59   ["a (a a (a (a a)) (a (a a)))"]
  60   ["*"]
  61 ;;
  62
  63 let p15 = magic
  64   ["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)))"]
  65   ["*"]
  66 ;;
  67
  68 let p16 = magic
  69   ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"]
  70   ["*"]
  71 ;;
  72
  73 let p17 = magic
  74   ["b a"; "b (c.a)"]
  75   ["*"]
  76 ;;
  77
  78 let p18 = magic
  79   ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"]
  80   ["*"]
  81 ;;
  82
  83 let p19 = magic
  84   ["a (a a) (a a a (a (a (a a) a)) a)"]
  85   ["*"]
  86 ;;
  87
  88 let p20 = magic
  89   ["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)))))"]["*"];;
  90
  91 let p21 = magic
  92   ["(((y z) (y z)) ((z (y z)) ((y z) (z z))))";
  93    "(((z z) x) (y z))";
  94    "((z (y z)) ((y z) (z z)))"
  95 ] ["*"];;
  96
  97 let p22 = magic
  98 ["((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))";
  99 "((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)))))";
 100 "(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ["*"];;
 101
 102 (* diverging tests *)
 103 (* test p23 leads to test p24 *)
 104 let p23 = magic
 105 ["z z z"; "z (z z) (x. x)"] ["*"];;
 106
 107 (* because of the last term, the magic number is 1 and we diverge;
 108    but setting the magic number to 0 allows to solve the problem;
 109    thus our strategy is incomplete *)
 110 let p24 = magic
 111 ["b b"; "b f"; "f b"; "a (x.x)"] ["*"];;
 112
 113 (* because of the last term, the magic number is 1 and we diverge;
 114    but setting the magic number to 0 allows to solve the problem;
 115    thus our strategy is incomplete *)
 116 let p25 = magic
 117 ["b b"; "b f"; "f b"; "f (x.x)"] ["*"];;
 118
 119 (* BUG:
 120    0 (n (d (o.n) ...)))
 121    After instantiating n, the magic number (for d) should be 2, not 1! *)
 122 let p26 = magic
 123 ["(((x y) (z. (y. (y. z)))) (z. y))";
 124 "(((x y) x) (y y))"] ["*"];;
 125
 126 let p27 = magic
 127 ["(((((((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))))";
 128 "((((((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)))";
 129 "(((((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))"] ["*"];;
 130
 131 let p28 = magic
 132 ["((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))";
 133  "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ["*"];;
 134
 135 let p29 = magic
 136 ["((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))";
 137 "(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ["*"];;
 138
 139 let p30 = magic
 140 ["((b c) (b. (z a)))";
 141 "((v (a. (z v))) ((y (b c)) ((z a) (v y))))";
 142 "((v (v. c)) z)";
 143 "((v y) (v (a. (z v))))";
 144 "((y (b c)) ((z a) (v y)))"] ["*"];;
 145
 146 let p31 = magic
 147 [" (((((((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)))";
 148 "((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))";
 149 "(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))";
 150 "(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))";
 151 "((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"] ["*"];;
 152
 153 let p32 = magic
 154 ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
 155 "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)";
 156 "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
 157 "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
 158 "((((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)))))))"
 159 ] ["*"];;
 160
 161 (* Shows an error when the strategy that minimizes special_k is NOT used *)
 162 let p33 = magic
 163 [
 164 "((((((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)))))))";
 165 "((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))";
 166 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))";
 167 "(((((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))))";
 168 (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)
 169 ] ["*"];;
 170
 171 let p34 = magic [
 172 "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";
 173 "d (j. e) e (j. c f) (j. c j) b a";
 174 "d (j. e) e (j. c f) b (b c (b c) (j. c f)) a";
 175 "d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a";
 176 "d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a";
 177 ] ["*"];;
 178 (* 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)
 179 1: (d j.e e j.(c f) j.(c j) b a)
 180 2: (d j.e e j.(c f) b (b c (b c) j.(c f)) a)
 181 3: (d j.e e j.(c f) b (b c (b c) j.(c f) (g b)) a)
 182 4: (d j.e e j.(c f) b j.k.(j l.e e l.(k f) b) a) *)
 183
 184 let p35 = magic [
 185 "(((((((((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)))))))";
 186 "((((((((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))))))))))";
 187 "((((((((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)))"
 188 ] ["*"];;
 189
 190 let p36 = magic
 191 [
 192 "(((((((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))))))))";
 193 "(((((((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)))";
 194 "(((((((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))"
 195 ] ["*"];;
 196
 197 (* issue with eta-equality of terms in ps *)
 198 let p37 = magic
 199   ["x (a y) z"; "x (a z. y z) w"; "a c"]
 200   ["*"];;
 201
 202 (**********************)
 203
 204 let q1 () = magic_conv
 205  None
 206  ["a d e"]
 207  ["a b"; "a c"]
 208  ["*"];;
 209
 210 let q2 () = magic_conv
 211  None
 212  ["a d e"]
 213  ["a b" ]
 214  ["*"];;
 215
 216 let q3 () = magic_conv
 217  (Some "x")
 218  ["a d e f"]
 219  ["a b" ]
 220  ["*"];;
 221
 222 let q4 () = magic_conv
 223  None
 224  ["f (x.a b c d)"]
 225  ["a b" ]
 226  ["*"];;
 227
 228 let q5 () = magic_conv
 229  (Some"x")
 230  ["(y. x)"]
 231  ["x"]
 232  ["*"];;
 233
 234 let q6 () = magic_conv
 235  (Some"x")
 236  ["(y. x z)"]
 237  ["y"]
 238  ["*"];;
 239
 240 let q7 () = magic_conv
 241  (Some "(b (c d (e f f k.(g e))) f)")
 242  ["(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)))";
 243   "(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)))))";
 244   "(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)))))"]
 245  ["(f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)";
 246   "(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)";
 247   "(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)"]
 248  ["*"];;
 249
 250 (**********************)
 251
 252 let q8 () = magic_conv
 253  (Some"x a")
 254  ["y (x b c)"] ["j"] ["*"]
 255 ;;
 256
 257 let q9 () = magic_conv
 258  (Some"x a")
 259  ["y x"] ["a (y a b b b)"] ["*"]
 260 ;;
 261
 262 let q11 () = magic_conv
 263  (Some "x y")
 264  ["a (x z)"] [] ["*"];;
 265
 266 let q10 () = magic_conv
 267  (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)
 268 (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
 269  (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c)))")
 270 ["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))";
 271 "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))";
 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))) (k. b (l. c))";
 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))) (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)))";
 274 "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)))"]
 275 [
 276 "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)))";
 277 "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))";
 278 "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)";
 279 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)";
 280 "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)))";
 281 ] ["*"];;
 282
 283 let m1 () = magic_conv None []
 284  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 285  ["*"]
 286 ;;
 287
 288 let m2 () = magic_conv None []
 289  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 290  ["*"]
 291 ;;
 292
 293 main ([
 294  (* p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ; p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ; p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ; p34 ; p35 ; p36 ; p37 ; *)
 295  p24 ; p25 ;
 296 ] @ if use_lambda3 then [] else List.map ((|>) ()) [
 297  q1 ; q2; q3; q4 ; q5 ; q6 ;
 298  (* q7 ; *)
 299  q8 ;
 300  q9 ;
 301  q10 ;
 302  q11 ;
 303  m1 ;
 304 ]);;