some optimizations

exp/naive.ml

@@ -28,11 +28,13 @@ let () =
     Printf.printf "Term: %s\n" (Core.a_term_to_string term);
     let t = Unix.gettimeofday () in
     let c1 = !Core.counter in
+    let bc1 = !Core.beta_counter in
     let s = Core.nf Core.cpsubst term in
     let c2 = !Core.counter in
+    let bc2 = !Core.beta_counter in
     let diff = Unix.gettimeofday () -. t in
-    Printf.printf "Execution time (%d): %f seconds\nAlpha conversions: %d"
+    Printf.printf "Execution time (%d): %f seconds\nAlpha conversions: %d\nBeta conversions: %d"
       (String.length (Core.a_term_to_string s))
-      diff (c2 - c1)
+      diff (c2 - c1) (bc2 - bc1)
 
 (* Printf.printf "%s\n" (Core.a_term_to_string (List.hd (List.rev reduction))); *)

exp/nocapture.ml

@@ -34,13 +34,16 @@ let () =
     Printf.printf "Term: %s\n" (Core.a_term_to_string term);
     let t = Unix.gettimeofday () in
     let c1 = !Core.counter in
+    let bc1 = !Core.beta_counter in
     let s = Core.nf Core.casubst term in
     let c2 = !Core.counter in
+    let bc2 = !Core.beta_counter in
     let diff = Unix.gettimeofday () -. t in
     Printf.printf "Execution time (%d): %f seconds\n"
       (String.length (Core.a_term_to_string s))
       diff;
     Printf.printf "Alpha conversions: %d (%d)\n" (c2 - c1)
-      (predict_conversions b n)
+      (predict_conversions b n);
+    Printf.printf "Beta conversions: %d\n" (bc2 - bc1)
 
 (* Printf.printf "%s\n" (Core.a_term_to_string (List.hd (List.rev reduction))); *)

lib/core.ml

@@ -683,6 +683,8 @@ let rec cpsubst var ex term =
       if var = fst xs then term else ALam ((xs, cpsubst var ex e), t)
   | AApp (e1, e2, t) -> AApp (cpsubst var ex e1, cpsubst var ex e2, t)
 
+let beta_counter = ref 0
+
 let counter = ref 0
 
 let next_fresh () =
@@ -744,6 +746,7 @@ let default_names term = default_names_r term "e"
 
 let beta subst term =
   (* Printf.printf "beta: %s\n" (a_term_to_string term); *)
+  beta_counter := !beta_counter + 1;
   match term with
   | AApp (ALam (((var,_), e1), _), e2, _) ->
     (* Printf.printf "subst: %s by %s in %s\n" var (a_term_to_string e2) (a_term_to_string e1); *)
@@ -780,6 +783,19 @@ let rec _reduce_lo subst term =
 
 let reduce_lo subst term = _reduce_lo subst term
 
+let rec _reduce_ri subst term =
+  match term with
+  | AVar (s, t) -> term
+  | ALam ((xs, e), t) -> ALam ((xs, _reduce_ri subst e), t)
+  | AApp (e1, e2, t) -> (
+      let right = _reduce_ri subst e2 in
+      let left = _reduce_ri subst e1 in
+      match e1 with
+      | ALam _ -> beta subst (AApp (left, right, t))
+      | _ -> (AApp (left, right, t)))
+
+let reduce_ri subst term = _reduce_ri subst term
+
 let rec _extract_first_redex_pos path =
   match path with
   | [] -> []

pcp/pcp.ml

@@ -65,6 +65,10 @@ let _isprefix = "(/r x y."^s_ite^" ("^s_isempty^" x) ("^s_true^") ("^s_and^" ("^
 let s_isprefix = ("(/a b."^s_ycomb^" " ^_isprefix ^ " a b)")
 let t_isprefix = tree_of_string s_isprefix
 
+(* LIST with TUPLE (e,e) *)
+let s_mkpair = "(/x y." ^ s_pair ^ " x y)"
+let t_mkpair = tree_of_string s_mkpair
+
 (* LISTS *)
 let s_cons = "(/x y.(/a b c.c a b) (/x y.y) ((/a b c.c a b) x y))"
 let t_cons = tree_of_string s_cons
@@ -77,12 +81,18 @@ let t_nil = tree_of_string s_nil
 let s_isnil = "(/p.p (/x y.x))"
 let t_isnil = tree_of_string s_isnil
 
+(* let _map = "(/r f xs."^s_ite^" ("^s_isnil^" xs) ("^s_nil^") ("^s_cons^" (f ("^s_lhd^" xs)) (r f ("^s_ltl^" xs))))"
+let s_map = "(/f xs."^s_ycomb^" "^_map^" f xs)" *)
+
+let _simplify = "(/r x y."^s_ite^" ("^s_or^" ("^s_isempty^" x) ("^s_isempty^" y)) ("^s_mkpair^" x y) (r ("^s_tl^" x) ("^s_tl^" y)))"
+let s_simplify = "(/p."^s_ycomb^" "^_simplify^" ("^s_first^" p) ("^s_second^" p))"
+
 let s_pcppair = "(/p."^s_or^" ("^s_isprefix^" ("^s_first^" p) ("^s_second^" p)) ("^s_isprefix^" ("^s_second^" p) ("^s_first^" p)))"
 let t_pcppair = tree_of_string s_pcppair
 
-let _filter = "(/r f xs."^s_ite^" ("^s_isnil^" xs) ("^s_nil^") ("^s_ite^" (f ("^s_lhd^" xs)) ("^s_cons^" ("^s_lhd^" xs) (r f ("^s_ltl^" xs))) (r f ("^s_ltl^" xs))))"
+(* let _filter = "(/r f xs."^s_ite^" ("^s_isnil^" xs) ("^s_nil^") ("^s_ite^" (f ("^s_lhd^" xs)) ("^s_cons^" ("^s_lhd^" xs) (r f ("^s_ltl^" xs))) (r f ("^s_ltl^" xs))))"
 let s_filter = "(/f xs."^s_ycomb^" " ^_filter ^ " f xs)"
-let t_filter = tree_of_string s_filter
+let t_filter = tree_of_string s_filter *)
 
 (* STRINGS *)
 let s_e = "(/x a b.x)"
@@ -95,15 +105,11 @@ let s_aa = "(/x a b.a (a x))"
 let s_ba = "(/x a b.b (a x))"
 let s_baba = "(/x a b.b (a (b (a x))))"
 
-(* LIST with TUPLE (e,e) *)
-let s_mkpair = "(/x y." ^ s_pair ^ " x y)"
-let t_mkpair = tree_of_string s_mkpair
-
 (* LIST OF TILES *)
 (* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.a (b x)) (/x a b.a x))"
 let t_tile1 = tree_of_string s_tile1
 
-let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.b (a x)))"
+let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.b (b (a x))))"
 let t_tile2 = tree_of_string s_tile2
 
 let s_tiles = "(" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ "))" *)
@@ -117,18 +123,32 @@ let t_tile2 = tree_of_string s_tile2
 let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.a (b x)))"
 let t_tile3 = tree_of_string s_tile3 *)
 
-let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b (a (a x))) (/x a b.b x))"
+(* SOLUTION 2113 *)
+let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.b (b (b x))))"
+let t_tile1 = tree_of_string s_tile1
+
+let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.b (a (b (b (b x))))) (/x a b.b (a x)))"
+let t_tile2 = tree_of_string s_tile2
+
+let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b (a x)) (/x a b.a x))"
+let t_tile3 = tree_of_string s_tile3
+
+
+(* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b (a (a x))) (/x a b.b x))"
 let t_tile1 = tree_of_string s_tile1
 
 let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.b (a (a x))))"
 let t_tile2 = tree_of_string s_tile2
 
 let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.a (a x)))"
-let t_tile3 = tree_of_string s_tile3
+let t_tile3 = tree_of_string s_tile3 *)
 
 let s_tiles = "(" ^ s_cons ^ " " ^ s_tile3 ^ " (" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ ")))"
 let t_tiles = tree_of_string s_tiles
 
+
+(* let tmp = tree_of_string (s_map ^ " " ^ s_simplify ^ " " ^ s_tiles) *)
+
 let s__find_eq = "(/r xs."^s_ite^" ("^s_isnil^" xs) "^s_false^" ("^s_or^" ("^s_eq_str^" ("^s_first^" ("^s_lhd^" xs)) ("^s_second^" ("^s_lhd^" xs))) (r ("^s_ltl^" xs))))"
 let s_find_eq = "(/xs."^s_ycomb^" "^s__find_eq^" xs)"
 let t_find_eq = tree_of_string s_find_eq
@@ -136,31 +156,46 @@ let t_find_eq = tree_of_string s_find_eq
 let s_concat_pairs = "(/p s."^s_mkpair^" ("^s_concat^" ("^s_first^" p) ("^s_first^" s)) ("^s_concat^" ("^s_second^" p) ("^s_second^" s)))"
 let t_concat_pairs = tree_of_string s_concat_pairs
 
-let s__combine = "(/r x ys."^s_ite^" ("^s_isnil^" ys) ("^s_nil^") ("^s_cons^" ("^s_concat_pairs^" x ("^s_lhd^" ys)) (r x ("^s_ltl^" ys))))"
-let s_combine = "(/x ys."^s_ycomb^" "^s__combine^" x ys)"
-let t_combine = tree_of_string s_combine
-
 let s__append = "(/r xs ys."^s_ite^" ("^s_isnil^" xs) ys ("^s_cons^" ("^s_lhd^" xs) (r ("^s_ltl^" xs) ys)))"
 let s_append = "(/xs ys."^s_ycomb^" "^s__append^" xs ys)"
 
+let s__combine = "(/r x ys."^s_ite^" ("^s_isnil^" ys) ("^s_nil^") ((/cp."^s_ite^" ("^s_pcppair^" cp) ("^s_cons^" ("^s_simplify^" cp) (r x ("^s_ltl^" ys))) (r x ("^s_ltl^" ys))) ("^s_concat_pairs^" x ("^s_lhd^" ys))))"
+(* let s__combine = "(/r x ys."^s_ite^" ("^s_isnil^" ys) ("^s_nil^") ("^s_cons^" ("^s_concat_pairs^" x ("^s_lhd^" ys)) (r x ("^s_ltl^" ys))))" *)
+let s_combine = "(/x ys."^s_ycomb^" "^s__combine^" x ys)"
+let t_combine = tree_of_string s_combine
+
 let s__cross_append = "(/r xs ys."^s_ite^" ("^s_isnil^" xs) ("^s_nil^") ("^s_append^" ("^s_combine^" ("^s_lhd^" xs) ys) (r ("^s_ltl^" xs) ys)))"
-let s_cross_append = "(/xs ys."^s_filter^" "^s_pcppair^" ("^s_ycomb^" "^s__cross_append^" xs ys))"
+(* let s_cross_append = "(/xs ys."^s_map^" "^s_simplify^" ("^s_filter^" "^s_pcppair^" ("^s_ycomb^" "^s__cross_append^" xs ys)))" *)
+let s_cross_append = "(/xs ys."^s_ycomb^" "^s__cross_append^" xs ys)"
 let t_cross_append = tree_of_string s_cross_append
 
 let s__pcp = "(/r xs ts."^s_ite^" ("^s_isnil^" xs) ("^s_false^") ("^s_ite^" ("^s_find_eq^" xs) ("^s_true^") (r ("^s_cross_append^" xs ts) ts)))"
 let s_pcp = "(/ts."^s_ycomb^" "^s__pcp^" ts ts)"
 let t_pcp = tree_of_string s_pcp
 
-let tmp = Core.AApp(t_pcp, t_tiles, UnT)
+
+let ls = tree_of_string ("(/c.(c (/x./y.y)) (/c.(c (/c.(c (/x./a./b.b x)) (/x./a./b.x))) (/c.(c (/x./y.y)) (/c.(c (/c.(c (/x./a./b.x)) (/x./a./b.b (b (b (b x)))))) (/x.x)))))")
+
+(* let tmp = t_tiles *)
+(* let tmp = Core.AApp(t_pcp, t_tiles, UnT) *)
+(* let tmp = Core.AApp(Core.AApp(t_cross_append,Core.AApp(t_filter,Core.AApp(Core.AApp(t_cross_append, Core.AApp(Core.AApp(t_filter, t_pcppair, UnT),Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT), UnT), t_tiles, UnT), UnT), UnT), t_tiles, UnT) *)
+(* let tmp = Core.AApp(Core.AApp(t_cross_append, Core.AApp(Core.AApp(t_filter, t_pcppair, UnT,Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT), UnT), t_tiles, UnT) *)
+(* let tmp = Core.AApp(Core.AApp(t_cross_append, Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT), t_tiles, UnT) *)
+(* let tmp = tree_of_string ("(/p."^ s_eq_str ^ " ("^s_first^" p) ("^s_second^" p)) (" ^s_simplify ^ " ("^s_mkpair^" ("^s_ab^") ("^s_ab^")))") *)
 (* let tmp = Core.AApp(Core.AApp(t_cross_append,
-    Core.AApp(Core.AApp(t_filter, t_pcppair, UnT), Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT),
-    UnT), t_tiles, UnT)
-(* let tmp = Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT) *) *)
+     Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT),
+    UnT), t_tiles, UnT) *)
+
+let tilestiles = Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT)
+let tmp = Core.AApp(Core.AApp(t_cross_append, tilestiles, UnT), t_tiles, UnT)
+(* let tmp = tilestiles *)
 let pcpp = tree_of_string (s_pcp ^" "^s_tiles^" y")
 
 let () =
   Printf.printf "PCP\n";
   Printf.printf "-----------------------------\n%s\n-----------------------------\n" (Core.a_term_to_string tmp);
+  Printf.printf "tiles: %s\n" (s_tiles);
   Printf.printf "res_tmp: %s\n" (Core.a_term_to_string (Core.nf Core.casubst tmp));
   (* Printf.printf "pcpp: %s\n" (Core.a_term_to_string (Core.nf Core.casubst pcpp)); *)
   Printf.printf "Alpha conversions: %d\n" (!Core.counter);
+  Printf.printf "Beta conversions: %d\n" (!Core.beta_counter);