vm.fail
Alpha equivalence checker for arbitrary lambda terms
1#!/usr/bin/env python3
2import json, random, os, sys
3import sys; sys.setrecursionlimit(1000000)
4
5OUT = os.path.dirname(os.path.abspath(__file__))
6
7def var(n): return {"tag":"Var","name":n}
8def lam(n,b): return {"tag":"Lam","param":n,"body":b}
9def app(f,a): return {"tag":"App","fun":f,"arg":a}
10def subst(n,s,t): return {"tag":"Subst","var":n,"repl":s,"body":t}
11
12def gen(rng, scope, fv_pool, depth, binder_density, shadow_freq, fv_freq):
13 if depth <= 0:
14 if scope and rng.random() > fv_freq:
15 return var(rng.choice(scope))
16 return var(rng.choice(fv_pool) if rng.random() < 0.8 else "z")
17 r = rng.random()
18 if r < binder_density:
19 if scope and rng.random() < shadow_freq:
20 n = rng.choice(scope)
21 else:
22 n = "v" + str(rng.randrange(8))
23 return lam(n, gen(rng, scope+[n], fv_pool, depth-1, binder_density, shadow_freq, fv_freq))
24 if r < binder_density + 0.25:
25 if rng.random() < 0.15:
26 n = rng.choice(scope) if scope else "u"
27 s = gen(rng, scope, fv_pool, depth-1, binder_density, shadow_freq, fv_freq)
28 t = gen(rng, scope, fv_pool, depth-1, binder_density, shadow_freq, fv_freq)
29 return subst(n, s, t)
30 return app(gen(rng, scope, fv_pool, depth-1, binder_density, shadow_freq, fv_freq),
31 gen(rng, scope, fv_pool, depth-1, binder_density, shadow_freq, fv_freq))
32 if scope and rng.random() > fv_freq:
33 return var(rng.choice(scope))
34 return var(rng.choice(fv_pool))
35
36def rename_chain(rng, t, depth):
37 names = ["a","b","c","d","e","f","g","h"]
38 out = t
39 for i in range(depth):
40 out = lam(rng.choice(names), out)
41 return out
42
43corpus = []
44
45def add(name, t1, t2, expected):
46 corpus.append({"name":name, "t1":t1, "t2":t2, "expected":expected})
47
48add("identical-var", var("x"), var("x"), True)
49add("identical-lam", lam("x", var("x")), lam("x", var("x")), True)
50add("renamed-binder", lam("x", var("x")), lam("y", var("y")), True)
51add("nested-renamed", lam("x", lam("y", app(var("x"), var("y")))),
52 lam("a", lam("b", app(var("a"), var("b")))), True)
53add("shadowing-same", lam("x", lam("x", var("x"))), lam("y", lam("y", var("y"))), True)
54add("shadowing-diff-binding", lam("x", lam("x", var("x"))), lam("x", lam("y", var("x"))), False)
55add("free-match", app(var("f"), lam("x", var("x"))), app(var("f"), lam("y", var("y"))), True)
56add("free-mismatch", app(var("f"), var("x")), app(var("g"), var("x")), False)
57add("binder-collides-free", lam("x", app(var("x"), var("y"))), lam("y", app(var("y"), var("y"))), False)
58add("binder-collides-free2", lam("y", app(var("y"), var("x"))), lam("z", app(var("z"), var("x"))), True)
59add("deep-nest", lam("a", lam("b", lam("c", lam("d", app(var("a"), var("d")))))),
60 lam("w", lam("x", lam("y", lam("z", app(var("w"), var("z")))))), True)
61add("subst-basic", subst("x", var("y"), lam("z", var("x"))), lam("z", var("y")), True)
62add("subst-capture-delayed", subst("x", var("z"), lam("z", var("x"))), lam("z", var("z")), False)
63add("subst-capture-correct", subst("x", var("z"), lam("z", var("x"))), lam("w", var("z")), True)
64add("subst-shadowed", subst("x", var("q"), lam("x", var("x"))), lam("x", var("x")), True)
65add("subst-repeated",
66 subst("x", var("a"), subst("y", var("b"), app(var("x"), var("y")))),
67 app(var("a"), var("b")), True)
68add("subst-under-binder-shift",
69 subst("x", app(var("w"), var("v")), lam("w", lam("v", var("x")))),
70 lam("a", lam("b", app(var("w"), var("v")))), True)
71add("subst-nested-subst",
72 subst("x", subst("y", var("k"), var("y")), lam("k", var("x"))),
73 lam("q", var("k")), True)
74add("subst-not-equiv", subst("x", var("y"), var("x")), var("z"), False)
75add("eta-ish-not-equiv", lam("x", app(var("f"), var("x"))), var("f"), False)
76add("app-order", app(var("a"), var("b")), app(var("b"), var("a")), False)
77add("normalises-equiv",
78 app(lam("x", var("x")), lam("y", var("y"))),
79 lam("z", var("z")), True)
80add("normalises-equiv2",
81 app(lam("x", lam("y", var("x"))), var("f")),
82 lam("y", var("f")), True)
83
84rng = random.Random(42)
85fv_pool = ["f","g","h","p","q"]
86for i in range(40):
87 t = gen(rng, [], fv_pool, rng.randrange(3, 7), 0.45, 0.4, 0.3)
88 add(f"rand-self-{i}", t, t, True)
89for i in range(30):
90 t = gen(rng, [], fv_pool, rng.randrange(3, 7), 0.45, 0.4, 0.3)
91 c=[0]
92 def alpha_rename(t, env):
93 if t["tag"]=="Var":
94 for old,new in reversed(env):
95 if old==t["name"]: return var(new)
96 return t
97 if t["tag"]=="App": return app(alpha_rename(t["fun"],env), alpha_rename(t["arg"],env))
98 if t["tag"]=="Subst":
99 c[0]+=1; n=f"r{c[0]}"
100 return subst(n, alpha_rename(t["repl"],env), alpha_rename(t["body"], env+[(t["var"],n)]))
101 c[0]+=1; n = f"r{c[0]}"
102 return lam(n, alpha_rename(t["body"], env+[(t["param"], n)]))
103 t2 = alpha_rename(t, [])
104 add(f"rand-renamed-{i}", t, t2, True)
105for i in range(20):
106 t1 = gen(rng, [], fv_pool, 5, 0.45, 0.4, 0.3)
107 t2 = gen(rng, [], fv_pool, 5, 0.45, 0.4, 0.3)
108 add(f"rand-any-{i}", t1, t2, None)
109
110with open(os.path.join(OUT, "corpus.json"), "w") as f:
111 json.dump(corpus, f, indent=1)
112
113rng = random.Random(7)
114def bench_chain(n):
115 t = var("x0")
116 for i in range(n): t = lam(f"b{i%5}", t)
117 return t
118def bench_apps(n):
119 t = var("f")
120 for i in range(n): t = app(t, var("x"))
121 return t
122def bench_shadow(n):
123 t = var("x")
124 for i in range(n): t = lam("x", t)
125 return t
126def bench_fv(n):
127 t = var("s")
128 for i in range(n): t = app(t, var(f"fv{i%50}"))
129 return t
130def bench_shift(n):
131 t = var("x")
132 for i in range(n):
133 t = subst("x", var(f"w{i%3}"), lam(f"w{i%3}", t))
134 return t
135def bench_bigsubst(n):
136 inner = var("x")
137 for i in range(n): inner = app(inner, var(f"g{i%20}"))
138 t = var("y")
139 for i in range(20): t = lam(f"p{i}", t)
140 return subst("y", inner, t)
141def bench_diff_at_leaves(n):
142 t = var("q")
143 for i in range(n): t = lam(f"a{i}", app(t, var(f"x{i}")))
144 t2 = var("DIFFERENT")
145 for i in range(n): t2 = lam(f"a{i}", app(t2, var(f"x{i}")))
146 return t, t2
147
148def deep_rename(t, c=[0]):
149 if t["tag"]=="Var": return t
150 if t["tag"]=="App": return app(deep_rename(t["fun"],c), deep_rename(t["arg"],c))
151 if t["tag"]=="Subst": return subst(t["var"], deep_rename(t["repl"],c), deep_rename(t["body"],c))
152 c[0]+=1
153 return lam(f"N{c[0]}", deep_rename(t["body"],c))
154
155benches = {}
156sizes = {"small":60, "medium":250, "large":1000}
157for label,n in sizes.items():
158 benches[f"chain-{label}"] = bench_chain(n)
159 benches[f"apps-{label}"] = bench_apps(n)
160 benches[f"shadow-{label}"] = bench_shadow(n)
161 benches[f"fv-{label}"] = bench_fv(n)
162 benches[f"shift-{label}"] = bench_shift(n // 5 if label!="large" else 120)
163 benches[f"bigsubst-{label}"] = bench_bigsubst(n)
164 a,b = bench_diff_at_leaves(n)
165 benches[f"leaves-{label}-a"] = a
166 benches[f"leaves-{label}-b"] = b
167 benches[f"allbinders-{label}-a"] = bench_chain(n)
168 benches[f"allbinders-{label}-b"] = deep_rename(bench_chain(n))
169
170with open(os.path.join(OUT, "bench.json"), "w") as f:
171 json.dump(benches, f)
172
173print(f"corpus: {len(corpus)} pairs, benches: {len(benches)} terms")