vm.fail
Alpha equivalence checker for arbitrary lambda terms
1type t =
2 | Var of string
3 | Lam of string * t
4 | App of t * t
5 | Subst of string * t * t
6
7module SSet = Set.Make (String)
8
9let rec free_variables = function
10 | Var x -> SSet.singleton x
11 | Lam (x, b) -> SSet.remove x (free_variables b)
12 | App (f, a) -> SSet.union (free_variables f) (free_variables a)
13 | Subst (x, s, b) ->
14 let fv_b = free_variables b in
15 let fv_b' = SSet.remove x fv_b in
16 if SSet.mem x fv_b then SSet.union fv_b' (free_variables s) else fv_b'
17
18let free_variable_list t = SSet.elements (free_variables t)
19
20let rec pretty = function
21 | Var x -> x
22 | Lam (x, b) -> "\\" ^ x ^ ". " ^ pretty b
23 | App (f, a) ->
24 let pf =
25 match f with Var _ | App _ -> pretty f | _ -> "(" ^ pretty f ^ ")"
26 in
27 let pa = match a with Var _ -> pretty a | _ -> "(" ^ pretty a ^ ")" in
28 pf ^ " " ^ pa
29 | Subst (x, s, b) -> "[" ^ x ^ " := " ^ pretty s ^ "] " ^ pretty b
30
31let fresh_name avoid base =
32 if not (SSet.mem base avoid) then base
33 else
34 let rec go i =
35 let cand = base ^ string_of_int i in
36 if SSet.mem cand avoid then go (i + 1) else cand
37 in
38 go 0
39
40let rename old nw t =
41 let rec ren = function
42 | Var z -> if z = old then Var nw else Var z
43 | App (f, a) -> App (ren f, ren a)
44 | Lam (z, b) -> if z = old then Lam (z, b) else Lam (z, ren b)
45 | Subst (z, u, b) ->
46 if z = old then Subst (z, ren u, b) else Subst (z, ren u, ren b)
47 in
48 ren t
49
50let substitute x s body =
51 let fv_s = free_variables s in
52 let fv_b = free_variables body in
53 let avoid0 = SSet.union fv_s fv_b in
54 let rec sub avoid = function
55 | Var y -> if y = x then s else Var y
56 | App (f, a) -> App (sub avoid f, sub avoid a)
57 | Lam (y, b) ->
58 if y = x then Lam (y, b)
59 else if (not (SSet.mem y fv_s)) || not (SSet.mem x (free_variables b)) then
60 Lam (y, sub avoid b)
61 else
62 let y' = fresh_name avoid y in
63 Lam (y', sub (SSet.add y' avoid) (rename y y' b))
64 | Subst (y, u, b) ->
65 if y = x then Subst (y, sub avoid u, b)
66 else if (not (SSet.mem y fv_s)) || not (SSet.mem x (free_variables b)) then
67 Subst (y, sub avoid u, sub avoid b)
68 else
69 let y' = fresh_name avoid y in
70 Subst (y', sub avoid u, sub (SSet.add y' avoid) (rename y y' b))
71 in
72 sub avoid0 body
73
74let step_limit = 10000
75
76let rec elim_subst = function
77 | Var x -> Var x
78 | Lam (x, b) -> Lam (x, elim_subst b)
79 | App (f, a) -> App (elim_subst f, elim_subst a)
80 | Subst (x, s, b) -> substitute x (elim_subst s) (elim_subst b)
81
82let is_value = function Lam _ -> true | _ -> false
83
84let rec step = function
85 | App (Lam (x, b), a) -> Some (substitute x a b)
86 | App (f, a) when not (is_value f) -> begin
87 match step f with
88 | Some f' -> Some (App (f', a))
89 | None -> begin
90 match step a with Some a' -> Some (App (f, a')) | None -> None
91 end
92 end
93 | App (f, a) -> begin
94 match step a with Some a' -> Some (App (f, a')) | None -> None
95 end
96 | Lam (x, b) -> begin
97 match step b with Some b' -> Some (Lam (x, b')) | None -> None
98 end
99 | _ -> None
100
101let normalise t =
102 let t = elim_subst t in
103 let rec go n t =
104 if n >= step_limit then t
105 else match step t with Some t' -> go (n + 1) t' | None -> t
106 in
107 go 0 t
108
109let normalise_counted t =
110 let count = ref 0 in
111 let maxd = ref 0 in
112 let rec walk d t =
113 incr count;
114 if d > !maxd then maxd := d;
115 match t with
116 | Var _ -> ()
117 | Lam (_, b) -> walk (d + 1) b
118 | App (f, a) -> walk (d + 1) f; walk (d + 1) a
119 | Subst (_, s, b) -> walk (d + 1) s; walk (d + 1) b
120 in
121 let t = elim_subst t in
122 walk 0 t;
123 let rec go n t =
124 if n >= step_limit then t
125 else
126 match step t with
127 | Some t' -> walk 0 t'; go (n + 1) t'
128 | None -> t
129 in
130 (go 0 t, !count, !maxd)
131
132let convert_from_named t = t
133let convert_to_named t = t
134
135let alpha_equivalent t1 t2 =
136 let rec go d e1 e2 a b =
137 match (a, b) with
138 | Var x, Var y -> begin
139 match (List.assoc_opt x e1, List.assoc_opt y e2) with
140 | Some i, Some j -> i = j
141 | None, None -> x = y
142 | _ -> false
143 end
144 | Lam (x, b1), Lam (y, b2) -> go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
145 | App (f1, a1), App (f2, a2) -> go d e1 e2 f1 f2 && go d e1 e2 a1 a2
146 | _ -> false
147 in
148 go 0 [] [] (normalise t1) (normalise t2)
149
150let alpha_equivalent_counted t1 t2 =
151 let count = ref 0 in
152 let maxd = ref 0 in
153 let rec go d e1 e2 a b =
154 incr count;
155 if d > !maxd then maxd := d;
156 match (a, b) with
157 | Var x, Var y -> begin
158 match (List.assoc_opt x e1, List.assoc_opt y e2) with
159 | Some i, Some j -> i = j
160 | None, None -> x = y
161 | _ -> false
162 end
163 | Lam (x, b1), Lam (y, b2) -> go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
164 | App (f1, a1), App (f2, a2) -> go d e1 e2 f1 f2 && go d e1 e2 a1 a2
165 | _ -> false
166 in
167 let r = go 0 [] [] (normalise t1) (normalise t2) in
168 (r, !count, !maxd)