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 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 rec rename old nw = function
41 | Var z -> if z = old then Var nw else Var z
42 | App (f, a) -> App (rename old nw f, rename old nw a)
43 | Lam (z, b) -> if z = old then Lam (z, b) else Lam (z, rename old nw b)
44 | Subst (z, u, b) ->
45 if z = old then Subst (z, rename old nw u, b)
46 else Subst (z, rename old nw u, rename old nw b)
47
48let step_limit = 10000
49
50let push_subst x s body =
51 let fv_s = free_variables s in
52 let rec go = function
53 | Var y -> if y = x then s else Var y
54 | App (t, u) -> App (go t, go u)
55 | Lam (y, b) ->
56 if y = x then Lam (y, b)
57 else if not (SSet.mem y fv_s) then Lam (y, go b)
58 else
59 let avoid =
60 SSet.union fv_s
61 (SSet.union (free_variables b) (free_variables s))
62 in
63 let y' = fresh avoid y in
64 Lam (y', go (rename y y' b))
65 | Subst (y, u, b) ->
66 if y = x then Subst (y, go u, b)
67 else if not (SSet.mem y fv_s) then Subst (y, go u, go b)
68 else
69 let avoid =
70 SSet.union fv_s
71 (SSet.union (free_variables b) (free_variables s))
72 in
73 let y' = fresh avoid y in
74 Subst (y', go u, go (rename y y' b))
75 in
76 go body
77
78let rec reduce = function
79 | Var x -> Var x
80 | Lam (x, b) -> Lam (x, reduce b)
81 | App (f, a) -> begin
82 let f' = reduce f in
83 let a' = reduce a in
84 match f' with Lam (x, b) -> reduce (push_subst x a' b) | _ -> App (f', a')
85 end
86 | Subst (x, s, b) -> reduce (push_subst x (reduce s) b)
87
88let normalise t =
89 let rec go n t =
90 if n >= step_limit then t
91 else
92 let t' = reduce t in
93 if t' = t then t else go (n + 1) t'
94 in
95 go 0 t
96
97let rec to_named = function
98 | Var x -> Named.Var x
99 | Lam (x, b) -> Named.Lam (x, to_named b)
100 | App (f, a) -> Named.App (to_named f, to_named a)
101 | Subst (x, s, b) -> Named.Subst (x, to_named s, to_named b)
102
103let rec of_named = function
104 | Named.Var x -> Var x
105 | Named.Lam (x, b) -> Lam (x, of_named b)
106 | Named.App (f, a) -> App (of_named f, of_named a)
107 | Named.Subst (x, s, b) -> Subst (x, of_named s, of_named b)
108
109let alpha_equivalent t1 t2 =
110 Named.alpha_equivalent (to_named (normalise t1)) (to_named (normalise t2))
111
112let alpha_equivalent_susp t1 t2 =
113 let rec go d e1 e2 a b =
114 match (a, b) with
115 | Var x, Var y -> begin
116 match (List.assoc_opt x e1, List.assoc_opt y e2) with
117 | Some i, Some j -> i = j
118 | None, None -> x = y
119 | _ -> false
120 end
121 | Lam (x, b1), Lam (y, b2) -> go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
122 | App (f1, a1), App (f2, a2) -> go d e1 e2 f1 f2 && go d e1 e2 a1 a2
123 | Subst (x, s1, b1), Subst (y, s2, b2) ->
124 go d e1 e2 s1 s2
125 && go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
126 | Subst _, _ -> go d e1 e2 (normalise a) b
127 | _, Subst _ -> go d e1 e2 a (normalise b)
128 | _ -> false
129 in
130 go 0 [] [] t1 t2
131
132let alpha_equivalent_counted t1 t2 =
133 let count = ref 0 in
134 let maxd = ref 0 in
135 let rec go d e1 e2 a b =
136 incr count;
137 if d > !maxd then maxd := d;
138 match (a, b) with
139 | Var x, Var y -> begin
140 match (List.assoc_opt x e1, List.assoc_opt y e2) with
141 | Some i, Some j -> i = j
142 | None, None -> x = y
143 | _ -> false
144 end
145 | Lam (x, b1), Lam (y, b2) -> go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
146 | App (f1, a1), App (f2, a2) -> go d e1 e2 f1 f2 && go d e1 e2 a1 a2
147 | Subst (x, s1, b1), Subst (y, s2, b2) ->
148 go d e1 e2 s1 s2
149 && go (d + 1) ((x, d) :: e1) ((y, d) :: e2) b1 b2
150 | Subst _, _ ->
151 let a' = normalise a in
152 if a' = a then false else go d e1 e2 a' b
153 | _, Subst _ ->
154 let b' = normalise b in
155 if b' = b then false else go d e1 e2 a b'
156 | _ -> false
157 in
158 let r = go 0 [] [] t1 t2 in
159 (r, !count, !maxd)
160
161let normalise_counted t =
162 let count = ref 0 in
163 let maxd = ref 0 in
164 let rec walk d t =
165 incr count;
166 if d > !maxd then maxd := d;
167 match t with
168 | Var _ -> ()
169 | Lam (_, b) -> walk (d + 1) b
170 | App (f, a) -> walk (d + 1) f; walk (d + 1) a
171 | Subst (_, s, b) -> walk (d + 1) s; walk (d + 1) b
172 in
173 walk 0 t;
174 let rec go n t =
175 if n >= step_limit then t
176 else
177 let t' = reduce t in
178 walk 0 t';
179 if t' = t then t else go (n + 1) t'
180 in
181 (go 0 t, !count, !maxd)
182
183let substitute x s body = Subst (x, s, body)
184
185let convert_from_named t = of_named t
186let convert_to_named t = to_named (normalise t)