Lambda MicroEgg: un egraph que maneja binders lambda con contextos y patrones de Miller
Philip Zucker presenta Lambda MicroEgg, un egraph basado en s-expressions que añade binders integrados, patrones de Miller de orden superior y sustitución que evita captura. Construido sobre microegg de Max Willsey, usa un byte robado del Id u32 para almacenar liftings de contexto, logrando que términos alfa-equivalentes se hash-consoliden igual y compartiendo memoria entre términos relacionados por thinning. Incluye demo wasm y repositorio en GitHub.
Es un egraph que soporta binders bien scopados y conscientes de alfa. Todo lo viejo es nuevo otra vez.