From c8d9c2fda6b135b29e81e3bea95520ba449b86e3 Mon Sep 17 00:00:00 2001 From: acondolu Date: Fri, 14 Jul 2017 10:57:22 +0200 Subject: [PATCH] Tidying up problems.ml --- ocaml/problems.ml | 309 ++++++++++++++++------------------------------ 1 file changed, 104 insertions(+), 205 deletions(-) diff --git a/ocaml/problems.ml b/ocaml/problems.ml index ca3a0d0..34245f0 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))"] ;; + "(((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 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)))"] ;; - -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 @@ -398,8 +306,8 @@ solve_many [ ]*) ];; -(* This now fails *) -solve (problem_of +(* This fails *) +(* solve (problem_of (Some"x PAC PAC PAC PAC PAC a") ["x PAC PAC PAC PAC PAC b"] ["y x"; "y z"] @@ -411,18 +319,9 @@ solve (problem_of 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 ([ - 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 ((|>) ()) ([ +solve_many (List.map ((|>) ()) ([ q1 ; q2; q3; q4 ; q5 ; q6 ; q7 ; q8 ; -- 2.39.2