// HACKER NEWS — CYBERSECURITY
Lambda MicroEgg
It’s an egraph that supports well-scoped alpha aware binders.
I made a tool that attaches my lifting e-graph ideas arxiv youtube to an s-expression based frontend.
It’s heavily based around Max’s microegg https://pavpanchekha.com/blog/microegg.html . But I added built in binders, higher order miller patterns, and capture avoiding substitution in right hand sides.
Here is using the binders for some $\sum$ rewrite rules. @ marks sum as a unary binding form. {?a x} is Miller pattern notation. More on that below.
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.
There is a tension between the typical first order notion of application FOApp(Symbol, Vec) and the higher order binary version HOApp(Id,Id). The latter can be encoded into the former using a ubiquitout “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.
If I switch out in an AC saturation example the first order () for the higher order [] there is a cost to it. But, perhaps with some optimizations (like precomputing ground ids in the pattern) this could be improved.
Superposition provers like e-prover and zipperposition have received special smarts for this lambda free higher order fragment https://inria.hal.science/hal-03485227/document. It’s a useful but simple thing. Or a simple but useful thing?
But in addition to this, it is really nice to support actual binders.