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