ocaml/problems/w

   1 $?\r
   2 D x y\r
   3 C x BOMB\r
   4 \r
   5 $?\r
   6 D x y z\r
   7 C x BOMB z\r
   8   x y y\r
   9 \r
  10 $!\r
  11  (* DISPLAY PROBLEM (main) - measure=965\r
  12     Discriminating sets (deltas):\r
  13     0 <> 1 <> 2 <> 3 <> 4\r
  14  *)(* DIVERGENT  *)\r
  15 D 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)) (k. b c d (l. c (l k)) (b c (l. e e) (b c d (l. e l) (e e (b (l. m. b)) d (l. d))) (l. c)))\r
  16 #   (* CONVERGENT *) [\r
  17 C 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. e e) (k. g (l. g (m. b c)) (l. i (f g)))\r
  18 C 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)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h))) (b c (k. c (e h)))\r
  19 C 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. e e)\r
  20 C 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)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h)))\r
  21 C b (k. l. b) (e f) (b c d) (e e (b (k. l. b)) d) (e (k. l. b c) (k. l. b k) (b c)) d (e e (e e) (d (k. f)) (b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))))) (e e (b (k. l. b)) (b (k. l. b) (e f) (b c d)) (e e (b (k. l. b)) d (k. d) (b (k. l. b))) (k. b c k (l. e l) (e e (b (l. m. b)) k (l. k)) (f g (c (e h))) (k b (l. b) (f g (e f))) (c (e h))) (k. i (f g) (l. l)))\r
  22 #  ] (* NUMERIC    *) [\r
  23 N 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)) (d b (k. b)) (k. l. c (l k)) a\r
  24   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)) a\r
  25   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\r
  26   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\r
  27   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\r
  28 #  ];\r
  29 \r
  30 $!\r
  31  problem_of\r
  32  (* DISPLAY PROBLEM (main) - measure=561\r
  33     Discriminating sets (deltas):\r
  34     0 <> 1 <> 2 <> 3 <> 4\r
  35  *)(* DIVERGENT  *)\r
  36 D b (c b) (k. d) (e f (k. e) (k. b) (f d)) (e f (k. g k) d) (k. c k (c k g))\r
  37 #   (* CONVERGENT *) [\r
  38 C c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g) (e f (k. k (g e) h) b (e (k. g) (h c (g c) f)))\r
  39   e f (k. k) (k. l. c b) (k. l. l (k b) g) (k. e f (l. l)) (h c (c (k. l. l b k) (k. l. d) (e f (k. k) (g e))) (k. g e (g e))) (k. g (l. e f g) (l. h c) (g (l. e f g) (l. h c)))\r
  40   e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (k. l. g l (g l) (m. c b))\r
  41   c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g)\r
  42   e f (k. k) (g e) (e f (k. e)) (e f (k. e)) (h c (b (g e) h (k. c (l. m. m k l))))\r
  43 # ] (* NUMERIC    *) [\r
  44 N c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. i) a\r
  45   e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) a\r
  46   e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) a\r
  47   e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) a\r
  48   g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f a\r
  49 #  ]\r
  50  ];\r
  51 \r
  52 # This fails, but shouldnt: commented out\r
  53 # $!\r
  54  D x PAC PAC PAC PAC PAC a\r
  55  C x PAC PAC PAC PAC PAC b\r
  56  N y x\r
  57    y z\r
  58 # In general:\r
  59   DIV x (n times PAC) a\r
  60   CON x (n times PAC) b\r
  61   1 y (m times lambda. x) 0\r
  62   2 y z 0\r
  63   when x steps on the n+1-th argument,\r
  64   y must apply n+m+1 variables\r
  65   Thus special_k must be >=n+m+1\r
  66 \r
  67 # todo:\r
  68   (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)\r