X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems.ml;h=b49cf7733578832c022cc994b87ccc6599660a3e;hb=79e9bd64d15490dd5abc353cc5b09378d3c640d1;hp=a11453d28119478f9fbb438f97e6f8775686738b;hpb=0991fc5486c3158fc361e84cbba5aefa67893ba4;p=fireball-separation.git diff --git a/ocaml/problems.ml b/ocaml/problems.ml index a11453d..b49cf77 100644 --- a/ocaml/problems.ml +++ b/ocaml/problems.ml @@ -1,201 +1,109 @@ open Lambda4;; -let magic strings = problem_of None [] strings;; let solve_many = List.iter solve;; -let p2 = magic [ "x y"; "x z" ; "x (y z)"] - -let p4 = magic - [ "x y"; "x (a. a x)" ; "y (y z)" ] - -let p5 = magic - ["a (x. x a) b"; "b (x. x b) a"] -;; - -let p6 = magic - ["a (x. x a) b"; "b (x. x b) (c a)"] - -;; - -let p7 = magic - ["a (x. (x a)(a x x a)(x x) )"] - -;; - -let p8 = magic - ["x x (x x)"] - -;; - -let p9 = magic - ["x x (x x x) (x x (x x)) (x x (x x x)) x x"] - -;; - -let p10 = magic - ["x (y (x a b c))"] - -;; - -let p11 = magic - ["x x"; "x (y.y)"] - -;; - -let p12 = magic - ["x x (x x)"; "x x (x (y.y))"] - -;; - -let p13 = magic - ["x x (x x (x x x x x (x x)))"] - -;; - -let p14 = magic - ["a (a a (a (a a)) (a (a a)))"] - -;; - -let p15 = magic - ["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)))"] - -;; - -let p16 = magic - ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"] - -;; - -let p17 = magic - ["b a"; "b (c.a)"] - -;; - -let p18 = magic - ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"] - -;; - -let p19 = magic - ["a (a a) (a a a (a (a (a a) a)) a)"] - -;; - -let p20 = magic - ["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)))))"];; - -let p21 = magic +(* p-series problems *) +let f x = problem_of None [] x in +solve_many (List.map f [ + (* 2 *) [ "x y"; "x z" ; "x (y z)"]; + (* 4 *) [ "x y"; "x (a. a x)" ; "y (y z)" ]; + (* 5 *) ["a (x. x a) b"; "b (x. x b) a"]; + (* 6 *) ["a (x. x a) b"; "b (x. x b) (c a)"]; + (* 7 *) ["a (x. (x a) (a x x a) (x x) )"]; + (* 8 *) ["x x (x x)"]; + (* 9 *) ["x x (x x x) (x x (x x)) (x x (x x x)) x x"]; + (* 10 *) ["x (y (x a b c))"]; + (* 11 *) ["x x"; "x (y.y)"]; + (* 12 *) ["x x (x x)"; "x x (x (y.y))"]; + (* 13 *) ["x x (x x (x x x x x (x x)))"]; + (* 14 *) ["a (a a (a (a a)) (a (a a)))"]; + (* 15 *) ["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)))"]; + (* 16 *) ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"]; + (* 17 *) ["b a"; "b (c.a)"]; + (* 18 *) ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"]; + (* 19 *) ["a (a a) (a a a (a (a (a a) a)) a)"]; + (* 20 *) ["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)))))"]; + (* 21 *) ["(((y z) (y z)) ((z (y z)) ((y z) (z z))))"; - "(((z z) x) (y z))"; - "((z (y z)) ((y z) (z z)))" -] ;; - -let p22 = magic -["((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))))"] ;; - -(* diverging tests *) -(* test p23 leads to test p24 *) -let p23 = magic -["z z z"; "z (z z) (x. x)"] ;; - -(* 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 *) -let p24 = magic -["b b"; "b f"; "f b"; "a (x.x)"] ;; - -(* 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 *) -let p25 = magic -["b b"; "b f"; "f b"; "f (x.x)"] ;; - -(* BUG: - 0 (n (d (o.n) ...))) - After instantiating n, the magic number (for d) should be 2, not 1! *) -let p26 = magic -["(((x y) (z. (y. (y. z)))) (z. y))"; -"(((x y) x) (y y))"] ;; - -let p27 = magic -["(((((((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))"] ;; - -let p28 = magic -["((((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)))))" ] ;; - -let p29 = magic -["((((((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)"] ;; - -let p30 = magic -["((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)))"] ;; + "(((z z) x) (y z))"; + "((z (y z)) ((y z) (z z)))"]; + (* 22 *) + ["((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))))"]; + (* 23 *) (* diverging tests *) (* test p23 leads to test p24 *) + ["z z z"; "z (z z) (x. x)"]; + (* 24 *) + (* 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 *) + ["b b"; "b f"; "f b"; "a (x.x)"]; + (* 25 *) + (* 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 *) + ["b b"; "b f"; "f b"; "f (x.x)"]; + (* 26 *) + (* BUG: + 0 (n (d (o.n) ...))) + After instantiating n, the magic number (for d) should be 2, not 1! *) + ["(((x y) (z. (y. (y. z)))) (z. y))"; + "(((x y) x) (y y))"]; + (* 27 *) + ["(((((((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))"]; + (* 28 *) + ["((((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)))))" ]; + (* 29 *) + ["((((((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)"]; + (* 30 *) + ["((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)))"]; + (* 31 *) + [" (((((((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))"]; + (* 32 *) + ["(((((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)))))))" + ]; + (* 33 *) + (* Shows an error when the strategy that minimizes special_k is NOT used *) + [ "((((((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))))"; + (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *) ]; + (* 34 *) + [ "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";]; + (* 35 *) + [ "(((((((((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)))"]; + (* 36 *) + [ "(((((((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))"]; + (* 37 *) (* issue with eta-equality of terms in ps *) + ["x (a y) z"; "x (a z. y z) w"; "a c"]; -let p31 = magic -[" (((((((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))"] ;; - -let p32 = magic -["(((((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)))))))" -] ;; - -(* Shows an error when the strategy that minimizes special_k is NOT used *) -let p33 = magic -[ -"((((((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))))"; -(* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *) -] ;; - -let p34 = magic [ -"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"; -] ;; -(* 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) -1: (d j.e e j.(c f) j.(c j) b a) -2: (d j.e e j.(c f) b (b c (b c) j.(c f)) a) -3: (d j.e e j.(c f) b (b c (b c) j.(c f) (g b)) a) -4: (d j.e e j.(c f) b j.k.(j l.e e l.(k f) b) a) *) - -let p35 = magic [ -"(((((((((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)))" -] ;; - -let p36 = magic -[ -"(((((((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))" -] ;; +]);; -(* issue with eta-equality of terms in ps *) -let p37 = magic - ["x (a y) z"; "x (a z. y z) w"; "a c"] - ;; - -(**********************) +(* q-series problems *) let q1 () = problem_of None @@ -210,7 +118,7 @@ let q2 () = problem_of ;; let q3 () = problem_of - (Some "x") + (Some "x y") ["a d e f"] ["a b" ] ;; @@ -222,13 +130,13 @@ let q4 () = problem_of ;; let q5 () = problem_of - (Some"x") + (Some"x y") ["(y. x)"] ["x"] ;; let q6 () = problem_of - (Some"x") + (Some"x w") ["(y. x z)"] ["y"] ;; @@ -376,7 +284,8 @@ solve_many [ (* 2 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) a"; (* 3 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) a"; (* 4 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) a"; - ]; problem_of + ]; + problem_of (* DISPLAY PROBLEM (main) - measure=561 Discriminating sets (deltas): 0 <> 1 <> 2 <> 3 <> 4 @@ -397,18 +306,22 @@ solve_many [ ] ];; -failwith "OKAy";; - -solve_many ([ - 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 ; - p24 ; p25 ; -] @ List.map ((|>) ()) ([ +(* This fails *) +(* solve (problem_of + (Some"x PAC PAC PAC PAC PAC a") + ["x PAC PAC PAC PAC PAC b"] + ["y x"; "y z"] + (* In general: + DIV x (n times PAC) a + CON x (n times PAC) b + 1 y (m times lambda. x) 0 + 2 y z 0 + when x steps on the n+1-th argument, + y must apply n+m+1 variables + Thus special_k must be >=n+m+1 *) +);; *) + +solve_many (List.map ((|>) ()) ([ q1 ; q2; q3; q4 ; q5 ; q6 ; q7 ; q8 ;