Lambda MicroEgg is a small, s-expression-based rewriting tool built around lifting e-graph ideas. An equality graph, or e-graph, stores many equivalent forms of an expression at once; rewrite rules add alternatives, and the engine can later extract a simpler or otherwise useful form. The hard case here is scope: in a lambda expression, a variable name belongs to the nearest binder, so a rewrite must not accidentally let it refer to the wrong variable.
Placed after the opening explanation of Lambda MicroEgg and equality graphs, where the project itself is introduced.
The project represents binders generically. Both `(@sum x BODY)` and `(@lam x BODY)` use the same internal `Binder(Symbol, Id)` shape; `lam` is just the conventional symbol for lambda calculus. Rewrite right-hand sides can also request explicit substitution through `#subst`, reducing the risk that moving a term across binders will capture a free variable.
Matching is deliberately restricted to Miller patterns, a tractable form of higher-order pattern. In a pattern such as `{?a x}`, the metavariable `?a` may stand for a body containing the distinct bound variable `x`, but it cannot capture an unrelated variable such as `y`. That restriction makes scoped matching easier to implement than full higher-order matching, which can encode undecidable problems. A supplied beta-reduction example rewrites `[((@lam x {?body x}) ?e)]` to `[{?body ?e}]` and extracts `42` from applying the identity function to `42`.
The implementation also uses thinning annotations to track how terms move between variable contexts. The author reports that alpha-equivalent terms—terms that differ only by consistent variable renaming—hash-cons to the same internal representation, while terms related by weakening can share some deeper memory. This is a design claim from the project, not an independent benchmark result.
The main trade-off is performance versus expressiveness. The author’s page reports that one higher-order saturation run was slower than a similar run using `egg`, and that switching from first-order to higher-order application added cost. Lambda MicroEgg supports ordered Miller patterns, so a nonlinear pattern that uses the same metavariable in a different argument order is rejected rather than silently handled. The repository describes command-line and WebAssembly demo entry points, but the packet does not establish broader adoption, correctness guarantees, or production performance.