ocaml/problems.ml

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