Lambda MicroEgg

It’s an egraph that supports well-scoped alpha aware binders. Everything old is new again. I made a tool that attaches my lifting e-graph ideas to an s-expression based frontend. Repo: github.com/philzook58/lambda-microegg, WASM demo: philipzucker.com/lambda-microegg/. The oooooold playbook. It’s heavily based around Max’s microegg. But I added built-in binders, higher-order Miller patterns, and capture-avoiding substitution in right-hand sides.

这是一个支持良作用域（well-scoped）且具备 alpha 等价感知绑定器的 egraph。一切旧事物又焕发了新生。我制作了一个工具，将我的 lifting e-graph 思想与基于 s-expression 的前端结合起来。仓库地址：github.com/philzook58/lambda-microegg，WASM 演示：philipzucker.com/lambda-microegg/。这是非常经典的老套路。它主要基于 Max 的 microegg，但我添加了内置绑定器、高阶 Miller 模式以及右侧的避免捕获替换（capture-avoiding substitution）。

Here is using the binders for some $\sum$ rewrite rules. @ marks sum as a unary binding form. {?a x} is Miller pattern notation.

以下是使用绑定器进行一些 $\sum$ 重写规则的示例。@ 将 sum 标记为一元绑定形式。{?a x} 是 Miller 模式的表示法。

%%file /tmp/sum.sexp
(insert (@sum x (@sum y (* 2 y))))
(rewrite (@sum x (* ?a {?b x})) (* ?a (@sum x {?b x}))) ; constant factoring
(rewrite (@sum x ?a) (* ?a N)) ; constant sum
(rewrite (* ?a ?b) (* ?b ?a)) ; mul commutativity
(run 10)
(guard (@sum x (@sum y (* 2 y))) (* 2 (* N (@sum x x))))

Overwriting /tmp/sum.sexp ! lambda-microegg /tmp/sum.sexp ; inserted e4 ; rewrite 1 added ; rewrite 2 added ; rewrite 3 added ; ran 5 rounds, 17 unions: 9 classes, 22 e-nodes ; match 21.72µs, apply 14.991µs, rebuild 19.347µs ; guard passed

覆盖 /tmp/sum.sexp ! lambda-microegg /tmp/sum.sexp ; 插入 e4 ; 添加重写 1 ; 添加重写 2 ; 添加重写 3 ; 运行 5 轮，17 次合并：9 个类，22 个 e-nodes ; 匹配 21.72µs，应用 14.991µs，重建 19.347µs ; 守卫通过

Here is an AC-10 saturation run. This is a reasonable no-thinking way to kind of know perf you’re in the ball park of. On my computer, egg is ~0.6s for a similar thing, so we’re slower but not extremely so. Since liftings are stored as a byte stolen from the u32 Id, there hopefully isn’t really much overhead associated with them, especially if not used.

这是一个 AC-10 饱和运行示例。这是一种无需多想就能大致了解性能是否在合理范围内的好方法。在我的电脑上，egg 处理类似任务大约需要 0.6 秒，所以我们慢一些，但并没有慢得离谱。由于 lifting 是作为从 u32 Id 中借用的一字节存储的，希望它们不会带来太多开销，尤其是在不使用它们的情况下。

Lambda Free Higher Order Application

无 Lambda 的高阶应用

There is a tension between the typical first-order notion of application FOApp(Symbol, Vec<Id>) and the higher-order binary version HOApp(Id,Id). The latter can be encoded into the former using a ubiquitous “app” symbol (app (app f x) y). This is burdensome to write though, so I added a different constructor and notation [] which automatically curries and uses HOApp.

典型的第一阶应用概念 FOApp(Symbol, Vec<Id>) 与高阶二元版本 HOApp(Id,Id) 之间存在张力。后者可以使用通用的 “app” 符号 (app (app f x) y) 编码为前者。但这写起来很麻烦，所以我添加了一个不同的构造函数和符号 []，它会自动进行柯里化并使用 HOApp。

Miller Patterns

Miller 模式

But in addition to this, it is really nice to support actual binders. The variation of higher-order patterns supported is Miller patterns. A Miller pattern {?a x y} is basically a bound variable allowance pattern. Another way of saying it is Miller patterns are higher-order patterns where the metavariable must be applied to distinct bound variables, not arbitrary terms.

除此之外，支持真正的绑定器也非常棒。所支持的高阶模式变体是 Miller 模式。Miller 模式 {?a x y} 本质上是一种绑定变量允许模式。换句话说，Miller 模式是指元变量必须应用于不同的绑定变量，而不是任意项的高阶模式。

What I think the thing I’ve actually added is the ability of pattern variables to have more context lying around than the base context. This first example returns a substitution in a context of size 1. ?b is the free variable in that context.

我认为我真正添加的功能是让模式变量能够拥有比基础上下文更多的上下文。第一个示例返回了一个大小为 1 的上下文中的替换。?b 是该上下文中的自由变量。