ocaml/problems/p

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