pcp.ml 5.42 KB
 Frontull Samuel committed Jul 12, 2021 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 ``````(** {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)``````