X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems%2Fp;h=27315d04a1f84867e2e4fe649ed9a3b032eb577f;hb=cc3341c4762822e934e694fed7b7757166fd34f2;hp=5e7283cbec99277c0bc13524f2fdfd094af0d2ed;hpb=0b5ad58b1454d58219dca88bd1d3e94f14ac50fc;p=fireball-separation.git diff --git a/ocaml/problems/p b/ocaml/problems/p index 5e7283c..27315d0 100644 --- a/ocaml/problems/p +++ b/ocaml/problems/p @@ -1,170 +1,172 @@ -# p2 -N x y - x z - x (y z) -# p4 -N x y - x (a. a x) - y (y z) +$! p2 +N x y Z + x z Z + x (y z) Z -# p5 -N a (x. x a) b - b (x. x b) a +$! p4 +N x y Z + x (a. a x) Z + y (y z) Z -# p6 -N a (x. x a) b - b (x. x b) (c a) +$! p5 +N a (x. x a) b Z + b (x. x b) a Z -# p7 -N a (x. (x a) (a x x a) (x x) ) +$! p6 +N a (x. x a) b Z + b (x. x b) (c a) Z -# p8 -N x x (x x) +$! p7 +N a (x. (x a) (a x x a) (x x) ) Z -# p9 -N x x (x x x) (x x (x x)) (x x (x x x)) x x +$! p8 +N x x (x x) Z -# p10 -N x (y (x a b c)) +$! p9 +N x x (x x x) (x x (x x)) (x x (x x x)) x x Z -# p11 -N x x - x (y.y) +$! p10 +N x (y (x a b c)) Z -# p12 -N x x (x x) - x x (x (y.y)) +$! p11 +N x x Z + x (y.y) Z -# p13 -N x x (x x (x x x x x (x x))) +$! p12 +N x x (x x) Z + x x (x (y.y)) Z -# p14 -N a (a a (a (a a)) (a (a a))) +$! p13 +N x x (x x (x x x x x (x x))) Z -# p15 -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))) +$! p14 +N a (a a (a (a a)) (a (a a))) Z -# p16: -N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) +$! p15 +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 -# p17 -N b a - b (c.a) +$! p16: +N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a)) Z -# p18 -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) +$! p17 +N b a Z + b (c.a) Z -# p19 -N a (a a) (a a a (a (a (a a) a)) a) +$! p18 +N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a)))) Z + a a Z + a (a a) Z -# p20 -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))))) +$! p19 +N a (a a) (a a a (a (a (a a) a)) a) Z -# p21 -N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) - (((z z) x) (y z)) - ((z (y z)) ((y z) (z z))) +$! p20 +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 -# p22 -N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) - ((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))))) - (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) +$! p21 +N (((y z) (y z)) ((z (y z)) ((y z) (z z)))) Z + (((z z) x) (y z)) Z + ((z (y z)) ((y z) (z z))) Z -# p23 - (* diverging tests *) (* test p23 leads to test p24 *) -N z z z - z (z z) (x. x) +$! p22 +N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z + ((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 + (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z)))) Z -# p24 - (* because of the last term, the magic number is 1 and we diverge +$! p23 +# (* diverging tests *) (* test p23 leads to test p24 *) +N z z z Z + z (z z) (x. x) Z + +$! p24 +# (* because of the last term, the magic number is 1 and we diverge but setting the magic number to 0 allows to solve the problem thus our strategy is incomplete *) -N b b - b f - f b - a (x.x) +N b b Z + b f Z + f b Z + a (x.x) Z -# p25 - (* because of the last term, the magic number is 1 and we diverge +$! p25 +# (* because of the last term, the magic number is 1 and we diverge but setting the magic number to 0 allows to solve the problem thus our strategy is incomplete *) -N b b - b f - f b - f (x.x) +N b b Z + b f Z + f b Z + f (x.x) Z -# p26 +$! p26 (* BUG: 0 (n (d (o.n) ...))) After instantiating n, the magic number (for d) should be 2, not 1! *) -N (((x y) (z. (y. (y. z)))) (z. y)) - (((x y) x) (y y)) - -# p27 -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 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)) - -# p28 -N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x))))) - (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x))))) - -# p29 -N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y)) - (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) - -# p30 -N ((b c) (b. (z a))) - ((v (a. (z v))) ((y (b c)) ((z a) (v y)))) - ((v (v. c)) z) - ((v y) (v (a. (z v)))) - ((y (b c)) ((z a) (v y))) - -# p31 -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))) - ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) - (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) - (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) - ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) - -# p32 -N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) - (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) - (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) - ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) - ((((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))))))) - -# p33 +N (((x y) (z. (y. (y. z)))) (z. y)) Z + (((x y) x) (y y)) Z + +$! p27 +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 + ((((((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 + (((((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 + +$! p28 +N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x))))) Z + (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x))))) Z + +$! p29 +N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y)) Z + (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) Z + +$! p30 +N ((b c) (b. (z a))) Z + ((v (a. (z v))) ((y (b c)) ((z a) (v y)))) Z + ((v (v. c)) z) Z + ((v y) (v (a. (z v)))) Z + ((y (b c)) ((z a) (v y))) Z + +$! p31 +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 + ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) Z + (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c)) Z + (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) Z + ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w)) Z + +$? p32 +# should fail because the first and second terms are eta-eq +N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y))) Z + (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a) Z + (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v))) Z + ((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) Z + ((((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 + +$! p33 (* Shows an error when the strategy that minimizes special_k is NOT used *) -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))))))) - ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y)) - (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) - (((((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)))) +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 + ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y)) Z + (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) Z + (((((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 # (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *) -# p34 -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 - d (j. e) e (j. c f) (j. c j) b a - d (j. e) e (j. c f) b (b c (b c) (j. c f)) a - d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a - d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a +$! p34 +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 + d (j. e) e (j. c f) (j. c j) b a Z + d (j. e) e (j. c f) b (b c (b c) (j. c f)) a Z + d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a Z + d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a Z -# p35 -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))))))) - ((((((((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)))))))))) - ((((((((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))) +$! p35 +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 + ((((((((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 + ((((((((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 -# p36 -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 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 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)) +$! p36 +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 + (((((((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 + (((((((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 -# p37 +$! p37 issue with eta-equality of terms in ps -N x (a y) z - x (a z. y z) w - a c +N x (a y) z Z + x (a z. y z) w Z + a c Z