Lambda MicroEgg: HO e-graph with Miller patterns and capture-avoiding substitution

E-graphs excel at equational reasoning but traditionally operate on first-order terms, making binder-aware rewriting awkward. Philip Zucker's Lambda MicroEgg extends Max Willsey's microegg with native binders, Miller patterns, and capture-avoiding substitution.

The key engineering insight is storing lifting annotations (scope depth) in a single byte stolen from the u32 e-class ID. This lets alpha-equivalent lambda terms hash-cons to identical e-classes — (@lam x (@lam y (+ x y))) and (@lam a (@lam b (+ a b))) become the same e-node — while non-alpha-equivalent but thinning-related terms share deeper substructure.

Miller patterns {?a x y} restrict metavariables to apply only to distinct bound variables in scope, providing a decidable fragment of higher-order matching. The system also supports lambda-free higher-order application via [] notation that auto-curries to HOApp(Id,Id), avoiding the verbose (app (app f x) y) encoding. Beta substitution becomes a simple rewrite rule.

Performance is within 2-3x of the base egg library on AC saturation benchmarks (262k unions in ~1.5s vs egg's ~0.6s), with the lifting byte adding negligible overhead when unused.

Steal one byte from u32 e-class IDs to store lifting annotations, enabling alpha-equivalent hash-consing and capture-avoiding substitution without extra memory overhead

First-order e-graphs require verbose De Bruijn encodings or explicit substitution machinery for binders

Miller patterns give a decidable, well-behaved fragment of higher-order matching

Stealing a byte from existing IDs avoids allocation overhead for lifting annotations

Alpha-equivalent hash-consing emerges naturally from the lifting representation

A single byte stolen from existing IDs can encode scoping discipline, turning a first-order e-graph into a higher-order one with minimal overhead.

The implementation is open-source at github.com/philzook58/lambda-microegg with a WASM demo. The author plans to add proof logging, ephemeral enodes for more variables, and integration with Buchberger/multiset/string/semiring completion.