Lambda MicroEgg

Lambda MicroEgg is an e-graph implementation that adds well-scoped, alpha-aware binders and higher-order Miller-pattern matching to an s-expression frontend, building on Max’s microegg ideas. It supplies built-in binders, a higher-order application form (HOApp) that automatically curries, and capture-avoiding substitution on right-hand sides. Examples show sum rewrites, a beta-reduction rule using Miller patterns, and AC saturation benchmarks; timings for match, apply, and rebuild are reported and the author notes reasonable but slower performance compared to egg. Alpha-equivalent terms are hash-consed; lifting annotations occupy a byte stolen from a 32-bit id. A repository and a wasm demo are available.

Miller patterns restrict metavariables to be applied to distinct bound variables while allowing free variables from the outer context; the implementation extends this by carrying richer context information for pattern-variable substitutions so substitutions are produced relative to a top context. An extra restriction requires pattern-variable arguments to appear in the same order as their binding, which simplifies matching and reduces complexity at the cost of some expressivity (notably certain nonlinear patterns). The write-up documents concrete trade-offs, internal representation choices, and possible extensions such as term-creation in patterns, explicit thinning, and variable-allowance annotations.