vm.fail
Alpha equivalence checker for arbitrary lambda terms
1type t =
2 | BVar of int
3 | FVar of string
4 | Lam of t
5 | App of t * t
6
7module SSet = Set.Make (String)
8
9exception Not_locally_closed
10
11let rec free_variables = function
12 | BVar _ -> SSet.empty
13 | FVar x -> SSet.singleton x
14 | Lam b -> free_variables b
15 | App (f, a) -> SSet.union (free_variables f) (free_variables a)
16
17let free_variable_list t = SSet.elements (free_variables t)
18
19let rec pretty = function
20 | BVar i -> "#" ^ string_of_int i
21 | FVar x -> x
22 | Lam b -> "\\. " ^ pretty b
23 | App (f, a) ->
24 let pf =
25 match f with
26 | BVar _ | FVar _ | App _ -> pretty f
27 | _ -> "(" ^ pretty f ^ ")"
28 in
29 let pa =
30 match a with BVar _ | FVar _ -> pretty a | _ -> "(" ^ pretty a ^ ")"
31 in
32 pf ^ " " ^ pa
33
34let rec open_at k x = function
35 | BVar i -> if i = k then FVar x else BVar i
36 | FVar y -> FVar y
37 | Lam b -> Lam (open_at (k + 1) x b)
38 | App (f, a) -> App (open_at k x f, open_at k x a)
39
40let open_top t x = open_at 0 x t
41
42let rec close_at k x = function
43 | BVar i -> BVar i
44 | FVar y -> if y = x then BVar k else FVar y
45 | Lam b -> Lam (close_at (k + 1) x b)
46 | App (f, a) -> App (close_at k x f, close_at k x a)
47
48let close_top t x = close_at 0 x t
49
50let rec lc_at depth = function
51 | BVar i -> i < depth
52 | FVar _ -> true
53 | Lam b -> lc_at (depth + 1) b
54 | App (f, a) -> lc_at depth f && lc_at depth a
55
56let lc t = lc_at 0 t
57
58let require_lc t =
59 if not (lc t) then raise Not_locally_closed
60
61let rec subst_bvar j s = function
62 | BVar i -> if i = j then s else if i > j then BVar (i - 1) else BVar i
63 | FVar x -> FVar x
64 | Lam b -> Lam (subst_bvar (j + 1) (shift s) b)
65 | App (f, a) -> App (subst_bvar j s f, subst_bvar j s a)
66
67and shift t =
68 let rec go cutoff = function
69 | BVar i -> if i >= cutoff then BVar (i + 1) else BVar i
70 | FVar x -> FVar x
71 | Lam b -> Lam (go (cutoff + 1) b)
72 | App (f, a) -> App (go cutoff f, go cutoff a)
73 in
74 go 0 t
75
76let rec subst_fvar x s = function
77 | BVar i -> BVar i
78 | FVar y -> if y = x then s else FVar y
79 | Lam b -> Lam (subst_fvar x s b)
80 | App (f, a) -> App (subst_fvar x s f, subst_fvar x s a)
81
82let convert_from_named t =
83 let rec go env = function
84 | Named.Var x -> begin
85 match List.assoc_opt x env with
86 | Some i -> BVar i
87 | None -> FVar x
88 end
89 | Named.Lam (x, b) ->
90 Lam (go ((x, 0) :: List.map (fun (v, i) -> (v, i + 1)) env) b)
91 | Named.App (f, a) -> App (go env f, go env a)
92 | Named.Subst (x, s, b) ->
93 go env (Named.substitute x s b)
94 in
95 go [] t
96
97let convert_to_named t =
98 require_lc t;
99 let fv = free_variables t in
100 let fresh_avoid avoid base =
101 if not (SSet.mem base avoid) then base
102 else
103 let rec go i =
104 let cand = base ^ string_of_int i in
105 if SSet.mem cand avoid then go (i + 1) else cand
106 in
107 go 0
108 in
109 let rec go env = function
110 | BVar i -> Named.Var (List.nth env i)
111 | FVar x -> Named.Var x
112 | Lam b ->
113 let avoid =
114 List.fold_left (fun a x -> SSet.add x a) fv env
115 in
116 let x = fresh_avoid avoid "v" in
117 Named.Lam (x, go (x :: env) b)
118 | App (f, a) -> Named.App (go env f, go env a)
119 in
120 go [] t
121
122let is_value = function Lam _ -> true | _ -> false
123
124let rec step = function
125 | App (Lam b, a) -> Some (subst_bvar 0 a b)
126 | App (f, a) when not (is_value f) -> begin
127 match step f with
128 | Some f' -> Some (App (f', a))
129 | None -> begin
130 match step a with Some a' -> Some (App (f, a')) | None -> None
131 end
132 end
133 | App (f, a) -> begin
134 match step a with Some a' -> Some (App (f, a')) | None -> None
135 end
136 | Lam b -> begin
137 match step b with Some b' -> Some (Lam b') | None -> None
138 end
139 | _ -> None
140
141let step_limit = 10000
142
143let normalise t =
144 require_lc t;
145 let rec go n t =
146 if n >= step_limit then t
147 else match step t with Some t' -> go (n + 1) t' | None -> t
148 in
149 go 0 t
150
151let normalise_counted t =
152 require_lc t;
153 let count = ref 0 in
154 let maxd = ref 0 in
155 let rec walk d t =
156 incr count;
157 if d > !maxd then maxd := d;
158 match t with
159 | BVar _ | FVar _ -> ()
160 | Lam b -> walk (d + 1) b
161 | App (f, a) -> walk (d + 1) f; walk (d + 1) a
162 in
163 walk 0 t;
164 let rec go n t =
165 if n >= step_limit then t
166 else
167 match step t with
168 | Some t' -> walk 0 t'; go (n + 1) t'
169 | None -> t
170 in
171 (go 0 t, !count, !maxd)
172
173let substitute x s body = subst_fvar x s body
174
175let alpha_equivalent t1 t2 =
176 require_lc t1;
177 require_lc t2;
178 normalise t1 = normalise t2
179
180let alpha_equivalent_counted t1 t2 =
181 require_lc t1;
182 require_lc t2;
183 let count = ref 0 in
184 let maxd = ref 0 in
185 let rec go d a b =
186 incr count;
187 if d > !maxd then maxd := d;
188 match (a, b) with
189 | BVar i, BVar j -> i = j
190 | FVar x, FVar y -> x = y
191 | Lam b1, Lam b2 -> go (d + 1) b1 b2
192 | App (f1, a1), App (f2, a2) -> go (d + 1) f1 f2 && go (d + 1) a1 a2
193 | _ -> false
194 in
195 let r = go 0 (normalise t1) (normalise t2) in
196 (r, !count, !maxd)