string equality in lambda calculus

lib/core.ml

@@ -743,9 +743,13 @@ let rec default_names_r term pos =
 let default_names term = default_names_r term "e"
 
 let beta subst term =
-  (* Printf.printf "beta: %s" (a_term_to_string term); *)
+  (* Printf.printf "beta: %s\n" (a_term_to_string term); *)
   match term with
-  | AApp (ALam ((xs, e1), _), e2, _) -> subst (fst xs) e2 e1
+  | 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); *)
+    let res = subst var e2 e1 in
+    (* Printf.printf "res: %s\n" (a_term_to_string res); *)
+    res
   | _ -> failwith "beta: Not a redex."
 
 let rec _reduce_at_pos subst term pos current =

pcp/dune

+(executable
+ (name pcp)
+ (libraries alpha))

pcp/pcp.ml

+(** {1 PCP in lambda calculus}
+This terms can be used to test and experiment. *)
+
+open Alpha
+
+let tree_of_string s = Grammar.input Lexer.token (Lexing.from_string (s^"\n"))
+let t_ite = tree_of_string "/c a b.c a b"
+let t_true = tree_of_string "/x y.x"
+let t_false = tree_of_string "/x y.y"
+let t_pair = tree_of_string "/a b c.c a b"
+let t_first = tree_of_string "/p.p (/x y.x)"
+let t_second = tree_of_string "/p.p (/x y.y)"
+let t_empty = tree_of_string "/x a b.x"
+let t_at = tree_of_string "/x./x y.x"
+let t_af = tree_of_string "/x./x y.y"
+let t_concat = tree_of_string "/y z x a b.y (z x a b) a b"
+let t_isempty = tree_of_string "/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)"
+let t_prepa = tree_of_string "/s x a b.a (s x a b)"
+let t_prepb = tree_of_string "/s x a b.b (s x a b)"
+let t_nexta = tree_of_string "/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)"
+let t_nextb = tree_of_string "/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)"
+let t_tl = tree_of_string "/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))"
+let t_hd = tree_of_string "/s x a b.s x (/y.a x) (/y.b x)"
+let t_hd_a = tree_of_string "/s.s (/x y.y) (/x./x y.x) (/x./x y.y)"
+let t_hd_b = tree_of_string "/s.s (/x y.y) (/x./x y.x) (/x./x y.x)"
+let t_is_e = tree_of_string "/s.s (/x y.x) (/x./x y.y) (/x./x y.y)"
+let t_and = tree_of_string "/x y.x y x"
+let t_or = tree_of_string "/x y.x x y"
+let t_hd_eq = tree_of_string "/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y))"
+let t_ycomb = tree_of_string "/f.(/x.f (x x)) (/x.f (x x))"
+let t_zcomb = tree_of_string "/f.(/x.f (/y.x x y)) (/x.f (/y.x x y))"
+
+let s_e = tree_of_string "/x a b.x"
+let s_a = tree_of_string "/x a b.a x"
+let s_b = tree_of_string "/x a b.b x"
+let s_ab = tree_of_string "/x a b.a (b x)"
+let s_aa = tree_of_string "/x a b.a (a x)"
+let s_ba = tree_of_string "/x a b.b (a x)"
+let s_baba = tree_of_string "/x a b.b (a (b (a x)))"
+
+(* let _all_a = tree_of_string "/f x.(/c a b.c a b) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) (/x y.x) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) (f ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x)))"
+let all_a = tree_of_string "/a.(/f.(/x.f (/y.x x y)) (/x.f (/y.x x y))) (/f x.(/c a b.c a b) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) (/x y.x) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) (f ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x)))) a" *)
+
+let _eq_str = tree_of_string "/rec x y.(/c a b.c a b) ((/x y.x x y) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y))) x y) (rec ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x) ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) y)))";;
+let eq_str = tree_of_string "/a b.(/f.(/x.f (x x)) (/x.f (x x))) (/rec x y.(/c a b.c a b) ((/x y.x x y) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y))) x y) (rec ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x) ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) y)))) a b";;
+
+let tmp = Core.AApp(Core.AApp(eq_str, s_baba, UnT), s_baba, UnT)
+let res = Core.nf (Core.casubst) tmp
+
+(* let tmp = Core.AApp(Core.AApp(t_and, t_true, UnT), t_true, UnT)
+let res = Core.nf (Core.casubst) tmp *)
+
+(* let tmp = Core.AApp(t_tl, s_baba, UnT)
+let res = Core.nf (Core.casubst) tmp *)
+
+let () = Printf.printf "res: %s" (Core.a_term_to_string res)