La reescritura de términos es una técnica fundamental en la optimización de compiladores, demostración de teoremas y sistemas de razonamiento automatizado. Sin embargo, su aplicación en lenguajes con ligadura de variables (como cálculo lambda o lenguajes funcionales) presenta desafíos significativos debido a la necesidad de manejar correctamente la equivalencia alfa, la sustitución con evitación de captura y los contextos de variables. Los e-graphs (equality graphs) han demostrado ser una estructura de datos eficiente para representar y manipular conjuntos de términos equivalentes, pero tradicionalmente operan en un contexto de primer orden, donde las variables son libres o globales.
Lambda MicroEgg aborda este problema fundamental extendiendo los e-graphs para incorporar de forma nativa el concepto de binders y patrones de orden superior. Esto permite aplicar técnicas de reescritura a expresiones con alcance léxico de manera robusta y eficiente, resolviendo la tensión entre la representación de aplicación de primer orden y de orden superior. La clave reside en una representación de 'liftings' que codifica el contexto de las variables ligadas directamente en los identificadores de los nodos del e-graph, lo que facilita la gestión de la equivalencia alfa y la sustitución, haciendo que la reescritura sea semánticamente correcta en presencia de ligadura de variables.
Arquitectura del Sistema
Lambda MicroEgg se construye sobre la base de un motor de e-graphs, similar a 'egg', pero con modificaciones clave para manejar la ligadura de variables. La representación interna de los términos utiliza una estructura de e-nodes que, además de los símbolos y referencias a otros e-nodes (Ids), incorpora 'lifting annotations'. Estas anotaciones son bits robados de los Ids de 32 bits, que indican el contexto de las variables ligadas, permitiendo hasta 7 variables en contexto en la implementación actual. Esta técnica de 'thinnings' o 'liftings' permite que términos alfa-equivalentes (ej. (@lam x x) y (@lam y y)) se hash-cons a la misma representación interna, garantizando la compartición de memoria y la eficiencia.
El sistema soporta 'Miller patterns', un tipo de patrón de orden superior que permite que las metavariables sean aplicadas a variables ligadas distintas, pero no a términos arbitrarios. Esto simplifica el problema de unificación de orden superior, haciéndolo decidible. La reescritura se realiza mediante reglas que especifican un patrón de lado izquierdo (LHS) y un patrón de lado derecho (RHS). Cuando un LHS coincide con una subexpresión en el e-graph, el RHS se utiliza para generar una nueva expresión equivalente, que se inserta en el e-graph, fusionando las clases de equivalencia correspondientes. La sustitución en el RHS es 'capture-avoiding', un proceso que recursivamente copia el e-graph o extrae términos, sustituye y reinserta, asegurando la corrección semántica. La arquitectura también introduce una distinción entre aplicación de primer orden () y aplicación de orden superior [] que automáticamente curries y utiliza HOApp(Id, Id), facilitando la escritura de expresiones de orden superior.
Flujo de Reescritura de Términos con Binders
- 1 Insertar Término El término inicial se parsea y se inserta en el e-graph, creando e-nodes y e-...
- 2 Añadir Reglas de Reescritura Las reglas (LHS -> RHS) se añaden al motor. Los LHS pueden contener Miller pa...
- 3 Ejecutar Reescritura El motor itera, buscando coincidencias de LHS en el e-graph. Se utiliza un al...
- 4 Aplicar Reglas Para cada coincidencia, se evalúa el RHS. La sustitución es 'capture-avoiding...
- 5 Unificar Clases Los nuevos términos generados por el RHS se insertan en el e-graph. Si un tér...
- 6 Reconstruir E-graph El e-graph se reconstruye y normaliza después de las uniones, manteniendo la ...
- 7 Extraer Resultado Una vez que la reescritura converge o se alcanza un límite, se extrae el térm...
| Capa | Tecnología | Justificación |
|---|---|---|
| data-processing | E-graphs (Equality Graphs) | Estructura de datos central para representar y manipular conjuntos de términos equivalentes de forma compacta y eficiente, extendida para manejar variables ligadas. vs Abstract Syntax Trees (ASTs), Directed Acyclic Graphs (DAGs), Term Rewriting Systems basados en unificación de orden superior completa |
| data-processing | Miller Patterns | Mecanismo de patrones de orden superior que permite la unificación decidible de metavariables con términos que contienen variables ligadas, crucial para la reescritura semánticamente correcta. vs Higher-Order Unification (general), Unificación de primer orden |
| data-processing | Liftings / Thinnings | Técnica para codificar el contexto de las variables ligadas directamente en los identificadores de los nodos del e-graph, permitiendo la equivalencia alfa y la sustitución con evitación de captura. vs De Bruijn Indices, De Bruijn Levels, Slotted De Bruijn Indices 1 byte robado de u32 Id para hasta 7 variables en contexto. |
| compute | Rust | Lenguaje de implementación, elegido por su rendimiento, seguridad de memoria y control de bajo nivel, adecuado para la manipulación eficiente de estructuras de datos complejas como los e-graphs. vs C++, OCaml, Haskell |
Trade-offs
Ganancias
- ▲ Soporte nativo para binders y equivalencia alfa
- ▲ Sustitución con evitación de captura
- ▲ Compartición de memoria para términos alfa-equivalentes
- ▲ Manejo de patrones de orden superior (Miller patterns)
Costes
- △ Rendimiento en comparación con e-graphs de primer orden (ej. 'egg')
- △ Restricción a 'ordered Miller patterns' (variables aplicadas en el mismo orden en que fueron ligadas)
- △ Límite de 7 variables ligadas en contexto (debido a la codificación de 'thinnings')
(rewrite (@sum x (* ?a {?b x}))
(* ?a (@sum x {?b x}))) ; constant factoring(rewrite [(@lam x {?body x}) ?e] {?body ?e}) ; beta substitution.Fundamentos Teóricos
El concepto de e-graphs se remonta a trabajos como 'Equality Saturation in Practice' de Tate, et al. (2021), que popularizó su uso en optimización de compiladores. Sin embargo, la extensión a lenguajes con ligadura de variables conecta con la investigación en unificación de orden superior y sistemas de tipos dependientes. Los 'Miller patterns' son una contribución fundamental de Dale Miller y Gopalan Nadathur, descritos en trabajos como 'Higher-Order Logic Programming' (Miller & Nadathur, 1991), que establecieron las bases para unificación decidible en un fragmento de lógica de orden superior. La gestión de contextos y variables ligadas a través de 'liftings' o 'thinnings' se relaciona con la teoría de De Bruijn indices y niveles, así como con enfoques más recientes como 'slotted de Bruijn indices' que buscan optimizar la representación de términos con ligadura de variables para operaciones como la sustitución y la equivalencia alfa. La idea de que 'contextos son parte de lo que son los términos' resuena con la semántica de juicios [[ctx |- t]] en la teoría de tipos y la lógica.