Los e-graphs son excelentes para el razonamiento ecuacional, pero tradicionalmente operan sobre términos de primer orden, lo que dificulta la reescritura consciente de ligaduras. Lambda MicroEgg de Philip Zucker extiende microegg de Max Willsey con ligaduras nativas, patrones de Miller y sustitución que evita capturas.
La idea clave de ingeniería es almacenar anotaciones de elevación (profundidad de alcance) en un único byte tomado del ID de e-class u32. Esto permite que los términos lambda alfa-equivalentes se hash-consoliden en e-classes idénticas — (@lam x (@lam y (+ x y))) y (@lam a (@lam b (+ a b))) se convierten en el mismo e-nodo — mientras que los términos no alfa-equivalentes pero relacionados por adelgazamiento comparten una subestructura más profunda.
Los patrones de Miller {?a x y} restringen las metavariables para que se apliquen solo a variables ligadas distintas dentro del alcance, lo que proporciona un fragmento decidible de emparejamiento de orden superior. El sistema también admite aplicación de orden superior sin lambda mediante la notación [] que aplica currificación automática a HOApp(Id,Id), evitando la codificación verbosa (app (app f x) y). La sustitución beta se convierte en una simple regla de reescritura.
El rendimiento está dentro de 2-3x de la biblioteca egg base en los benchmarks de saturación AC (262k uniones en ~1.5s frente a ~0.6s de egg), y el byte de elevación añade una sobrecarga insignificante cuando no se usa.
Tomar un byte de los ID de e-class u32 para almacenar anotaciones de elevación, lo que permite hash-consolidación alfa-equivalente y sustitución que evita capturas sin sobrecarga de memoria adicional
Los e-graphs de primer orden requieren codificaciones verbosas de De Bruijn o maquinaria de sustitución explícita para las ligaduras
Los patrones de Miller proporcionan un fragmento decidible y bien comportado del emparejamiento de orden superior
Tomar un byte de los ID existentes evita la sobrecarga de asignación para las anotaciones de elevación
La hash-consolidación alfa-equivalente surge naturalmente de la representación de elevación
Un único byte tomado de los ID existentes puede codificar la disciplina de alcance, convirtiendo un e-graph de primer orden en uno de orden superior con una sobrecarga mínima.
La implementación es de código abierto en github.com/philzook58/lambda-microegg con una demostración WASM. El autor planea añadir registro de pruebas, e-nodos efímeros para más variables e integración con la completación de Buchberger/multiconjunto/cadena/semianillo.
CONSULTA LAS PRUEBAS
Las fuentes
- Lambda MicroEgg Philip Zucker's Blog · philipzucker.com