ocaml/problems/p

   1 \r
   2 $! p2\r
   3 N x y Z\r
   4   x z Z\r
   5   x (y z) Z\r
   6 \r
   7 $! p4\r
   8 N x y Z\r
   9   x (a. a x) Z\r
  10   y (y z) Z\r
  11 \r
  12 $! p5\r
  13 N a (x. x a) b Z\r
  14   b (x. x b) a Z\r
  15 \r
  16 $! p6\r
  17 N a (x. x a) b Z\r
  18   b (x. x b) (c a) Z\r
  19 \r
  20 $! p7\r
  21 N a (x. (x a) (a x x a) (x x) ) Z\r
  22 \r
  23 $! p8\r
  24 N x x (x x) Z\r
  25 \r
  26 $! p9\r
  27 N x x (x x x) (x x (x x)) (x x (x x x)) x x Z\r
  28 \r
  29 $! p10\r
  30 N x (y (x a b c)) Z\r
  31 \r
  32 $! p11\r
  33 N x x Z\r
  34   x (y.y) Z\r
  35 \r
  36 $! p12\r
  37 N x x (x x) Z\r
  38   x x (x (y.y)) Z\r
  39 \r
  40 $! p13\r
  41 N x x (x x (x x x x x (x x))) Z\r
  42 \r
  43 $! p14\r
  44 N a (a a (a (a a)) (a (a a))) Z\r
  45 \r
  46 $! p15\r
  47 N 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))) Z\r
  48 \r
  49 $! p16:\r
  50 N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) Z\r
  51 \r
  52 $! p17\r
  53 N b a Z\r
  54   b (c.a) Z\r
  55 \r
  56 $! p18\r
  57 N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a)))) Z\r
  58   a a Z\r
  59   a (a a) Z\r
  60 \r
  61 $! p19\r
  62 N a (a a) (a a a (a (a (a a) a)) a) Z\r
  63 \r
  64 $! p20\r
  65 N 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))))) Z\r
  66 \r
  67 $! p21\r
  68 N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) Z\r
  69   (((z z) x) (y z)) Z\r
  70   ((z (y z)) ((y z) (z z))) Z\r
  71 \r
  72 $! p22\r
  73 N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z\r
  74   ((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))))) Z\r
  75   (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z\r
  76 \r
  77 $! p23\r
  78 # (* diverging tests *) (* test p23 leads to test p24 *)\r
  79 N z z z Z\r
  80   z (z z) (x. x) Z\r
  81 \r
  82 $! p24\r
  83 # (* because of the last term, the magic number is 1 and we diverge\r
  84      but setting the magic number to 0 allows to solve the problem\r
  85      thus our strategy is incomplete *)\r
  86 N b b Z\r
  87   b f Z\r
  88   f b Z\r
  89   a (x.x) Z\r
  90 \r
  91 $! p25\r
  92 # (* because of the last term, the magic number is 1 and we diverge\r
  93      but setting the magic number to 0 allows to solve the problem\r
  94      thus our strategy is incomplete *)\r
  95 N b b Z\r
  96   b f Z\r
  97   f b Z\r
  98   f (x.x) Z\r
  99 \r
 100 $! p26\r
 101   (* BUG:\r
 102      0 (n (d (o.n) ...)))\r
 103      After instantiating n, the magic number (for d) should be 2, not 1! *)\r
 104 N (((x y) (z. (y. (y. z)))) (z. y)) Z\r
 105   (((x y) x) (y y)) Z\r
 106 \r
 107 $! p27\r
 108 N (((((((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)))) Z\r
 109   ((((((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\r
 110   (((((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\r
 111 \r
 112 $! p28\r
 113 N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x))))) Z\r
 114   (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x))))) Z\r
 115 \r
 116 $! p29\r
 117 N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y)) Z\r
 118   (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) Z\r
 119 \r
 120 $! p30\r
 121 N ((b c) (b. (z a))) Z\r
 122   ((v (a. (z v))) ((y (b c)) ((z a) (v y)))) Z\r
 123   ((v (v. c)) z) Z\r
 124   ((v y) (v (a. (z v)))) Z\r
 125   ((y (b c)) ((z a) (v y))) Z\r
 126 \r
 127 $! p31\r
 128 N  (((((((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))) Z\r
 129    ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) Z\r
 130    (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) Z\r
 131     (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) Z\r
 132       ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) Z\r
 133 \r
 134 $? p32\r
 135 # should fail because the first and second terms are eta-eq\r
 136 N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) Z\r
 137   (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) Z\r
 138   (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) Z\r
 139   ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) Z\r
 140   ((((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))))))) Z\r
 141 \r
 142 $! p33\r
 143   (* Shows an error when the strategy that minimizes special_k is NOT used *)\r
 144 N ((((((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))))))) Z\r
 145   ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y)) Z\r
 146   (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) Z\r
 147   (((((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)))) Z\r
 148 #  (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)\r
 149 \r
 150 $! p34\r
 151 N 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 Z\r
 152   d (j. e) e (j. c f) (j. c j) b a Z\r
 153   d (j. e) e (j. c f) b (b c (b c) (j. c f)) a Z\r
 154   d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a Z\r
 155   d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a Z\r
 156 \r
 157 $! p35\r
 158 N (((((((((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))))))) Z\r
 159   ((((((((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)) Z (((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)))))))))) Z\r
 160   ((((((((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))) Z\r
 161 \r
 162 $! p36\r
 163 N (((((((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)))))))) Z\r
 164   (((((((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))) Z\r
 165   (((((((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)) Z\r
 166 \r
 167 \r
 168 $! p37\r
 169   issue with eta-equality of terms in ps\r
 170 N x (a y) z Z\r
 171   x (a z. y z) w Z\r
 172   a c Z\r