Lambda MicroEgg：带 Miller 模式和避免捕获替换的高阶 e-graph

E-graph 擅长等式推理，但传统上只处理一阶项，因此涉及绑定器的重写很别扭。Philip Zucker 的 Lambda MicroEgg 在 Max Willsey 的 microegg 基础上扩展，加入原生绑定器、Miller 模式和避免捕获的替换。

关键的工程洞见是：把提升标注（作用域深度）存进从 u32 e-class ID 中挪出的一个字节里。这样，alpha 等价的 lambda 项会哈希合并到相同的 e-class —— (@lam x (@lam y (+ x y))) 和 (@lam a (@lam b (+ a b))) 成为同一个 e-node —— 而非 alpha 等价但存在细化关系的项则共享更深层的子结构。

Miller 模式 {?a x y} 限制元变量只能应用于作用域内互不相同的绑定变量，从而给出高阶匹配的一个可判定片段。系统还通过 [] 记法支持免 lambda 的高阶应用，它会自动柯里化为 HOApp(Id,Id)，避免冗长的 (app (app f x) y) 编码。Beta 替换则变成一条简单的重写规则。

在 AC 饱和基准测试中，性能与基础 egg 库相差在 2-3 倍以内（约 1.5 秒完成 262k 次合并，而 egg 约 0.6 秒），未使用时提升字节带来的开销可忽略不计。

从 u32 e-class ID 中挪出一个字节来存储提升标注，在不增加额外内存开销的情况下实现 alpha 等价哈希合并和避免捕获的替换

一阶 e-graph 处理绑定器需要冗长的 De Bruijn 编码或显式的替换机制

Miller 模式给出高阶匹配的一个可判定、行为良好的片段

从现有 ID 中挪出一个字节，避免了提升标注的分配开销

alpha 等价哈希合并从提升表示中自然涌现

从现有 ID 中挪出的一个字节就能编码作用域规则，以极小开销把一阶 e-graph 变成高阶 e-graph。

该实现在 github.com/philzook58/lambda-microegg 开源，并附有 WASM 演示。作者计划加入证明日志、用于更多变量的临时 enode，以及与 Buchberger/多重集/字符串/半环补全的集成。