pcp.ml 5.42 KB
Newer Older
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)