Resumen Técnico: E-Graphs Categóricos para Cálculo Lambda

Planteamiento del Problema

La saturación de igualdad es una técnica poderosa para la optimización y el razonamiento de programas, utilizando clases de equivalencia de términos (e-graphs) para explorar un espacio de reglas de reescritura de forma no destructiva. Sin embargo, las e-graphs tradicionales carecen de soporte nativo para la vinculación de variables (variable binding), una característica fundamental de los lenguajes de programación funcional basados en el cálculo $\lambda$.

Los enfoques existentes para incorporar la vinculación enfrentan desafíos significativos:

1. Representaciones Textuales: En la sintaxis textual estándar, los términos $\alpha$-equivalentes son distintos y no pueden compartirse. Si bien los índices de De Bruijn identifican la $\alpha$-equivalencia sintácticamente, los índices dependen del alcance (scope) de la variable, lo que impide el intercambio de términos que difieren solo en la asignación de índices (por ejemplo, $\lambda f. f((\lambda x. fx)2)$).
2. Sustitución Explícita: Añadir nodos de sustitución explícita (por ejemplo, $t[x/u]$) para manejar la vinculación introduce "burocracia". Esto requiere nodos adicionales y reglas de reescritura para gestionar las permutaciones de sustituciones no interactuantes (equivalencia gráfica), lo que satura el espacio de estados con una sobrecarga administrativa en lugar de reescritura específica del dominio.
3. E-Graphs con Ranuras (Slotted E-Graphs): El trabajo reciente (Schneider et al.) introduce "e-graphs con ranuras" donde las variables son de primera clase. Aunque es efectivo, este enfoque depende de técnicas nominales aplicables a lenguajes arbitrarios (como el $\pi$-calculus), pero puede no aprovechar las propiedades estructurales específicas del cálculo $\lambda$ de manera tan eficiente como un modelo semántico dedicado.

El problema central es la falta de una estructura de datos categórica nativa para las e-graphs que soporte la vinculación de variables, permitiendo una saturación de igualdad eficiente en los cálculos $\lambda$ sin la sobrecarga de los nodos de sustitución explícita o las complejas reglas de renombramiento.

Metodología

Los autores proponen una solución fundamentada en la semántica categórica, extendiendo la interpretación de las e-graphs como diagramas de cuerdas.

1. Marco Categórico

El artículo se basa en el trabajo de Tiurin et al., quienes modelaron las e-graphs (sin vinculación) como morfismos en categorías de semilattice-enriquecidas monoidales simétricas (SLat-categories).

• Enriquecimiento SLat: Los conjuntos Hom son semilattices, donde la operación de unión ($+$) representa la equivalencia de subtérminos (clases de la e-graph).
• Estructura Monoidal Cerrada: Para manejar la vinculación de variables, los autores extienden la categoría para que sea monoidal cerrada. Esto introduce el objeto interno hom ($A \multimap B$) y la adjunción $- \otimes B \dashv B \multimap -$.
• Diagramas de Cuerdas: Los términos se representan como diagramas de cuerdas. La vinculación se modela mediante "cajas redondeadas" (que representan la abstracción $\lambda$), y las clases de equivalencia se modelan mediante "cajas discontinuas" (que representan la unión de la semilattice).

2. Representación Combinatoria: E-Hipergrafos Cerrados

Para proporcionar una estructura de datos concreta, los autores definen e-hipergrafos cerrados. Estos son hipergrafos jerárquicos que codifican:

• Hiperaristas: Representan operaciones (generadores).
• Aristas Jerárquicas: Dos tipos de estructuras anidadas:
  • Clases-e (Cajas discontinuas): Representan clases de equivalencia de subtérminos.
  • Cajas de Abstracción (Cajas redondeadas): Representan abstracciones $\lambda$.
• Interfaces: La estructura utiliza cospans extendidos para gestionar entradas y salidas, distinguiendo entre interfaces externas (nivel superior) e interfaces estrictamente internas (anidadas dentro de las cajas).

3. Sistema de Reescritura

Los autores definen un sistema de reescritura Double-Pushout with Interfaces (DPOI) para e-hipergrafos cerrados.

• Reglas de Reescritura: Definidas como spans de cospans extendidos.
• Complementos de Frontera: Se introduce una definición especializada del "hueco" (hole) dejado tras eliminar un match para manejar la naturaleza jerárquica de los grafos. Esto asegura que cuando se elimina un subgrafo, las interfaces internas se ajusten correctamente (por ejemplo, eliminar un término anidado actualiza la interfaz estrictamente interna de su padre).
• Corrección y Completitud: El artículo establece que la reescritura DPO en estos e-hipergrafos cerrados es correcta (sound) y completa con respecto a la reescritura de términos $\Sigma^+$ cerrados módulo las ecuaciones de las categorías monoidales simétricas SLat y la ley de distributividad de la estructura cerrada.

Contribuciones Clave

1. Extensión Categórica: La construcción de una forma de e-graphs que soporta la vinculación mediante la extensión del dominio categórico de categorías monoidales simétricas SLat libres a categorías monoidales simétricas cerradas SLat libres.
2. E-Hipergrafos Cerrados: La definición de una representación combinatoria concreta (e-hipergrafos cerrados) que absorbe naturalmente las ecuaciones de la estructura monoidal simétrica y la estructura cerrada (vinculación).
3. Reescritura DPOI para la Vinculación: La formulación de un sistema de reescritura DPOI para estas estructuras, demostrando su corrección y completitud respecto a la reescritura de términos en la teoría categórica correspondiente.
4. Comparación con E-Graphs con Ranuras: Una comparación teórica que demuestra que, mientras las e-graphs con ranuras ofrecen una vinculación genérica mediante técnicas nominales, el enfoque categórico integra la vinculación en el lenguaje interno del modelo, ofreciendo potencialmente ventajas para las optimizaciones específicas del cálculo $\lambda$.

Resultados

• Equivalencia de Reescritura: El artículo demuestra que la reescritura de términos de términos $\Sigma^+$ cerrados es equivalente a la reescritura DPO de e-hipergrafos cerrados.
• Manejo de la Equivalencia Gráfica: El enfoque maneja naturalmente la "equivalencia gráfica" (permutaciones de sustituciones no interactuantes) sin requerir nodos de sustitución explícitos. En el modelo categórico, la sustitución explícita se modela como composición, y las leyes estructurales de la categoría absorben las equivalencias necesarias.
• Estudio de Caso ($\lambda_{lsub}$): Los autores aplican la teoría al cálculo de sustitución lineal ($\lambda_{lsub}$). Demuestran que los términos con sustituciones explícitas (por ejemplo, bindings de tipo let) pueden representarse directamente como diagramas de cuerdas.
  • A diferencia de las e-graphs convencionales que requieren nodos explícitos para la sustitución y reglas de reescritura para manejar su permutación, el modelo categórico trata esto como propiedades estructurales del diagrama.
  • El artículo muestra que los programas semánticamente equivalentes (por ejemplo, reordenar bindings de tipo let) mapean al mismo diagrama de cuerdas, permitiendo que la saturación de igualdad opere sobre una representación normalizada.

Significado y Reivindicaciones

El artículo afirma proporcionar una semántica categórica fundacional para las e-graphs con vinculación, un área previamente subdesarrollada.

• Justificación Teórica: Ofrece una justificación rigurosa para las congruencias mantenidas por las e-graphs con vinculación, fundamentándolas en las propiedades de las categorías monoidales simétricas cerradas SLat.
• Potencial de Eficiencia: Al absorber las ecuaciones estructurales (como asociatividad, conmutatividad y permutaciones de sustitución) en la sintaxis gráfica y en la categoría subyacente, el enfoque busca reducir la "burocracia" en el espacio de estados de la saturación de igualdad. Esto contrasta con los enfoques que tratan estas como reglas de reescritura explícitas.
• Alcance: Los autores declaran explícitamente que su enfoque está especializado para el cálculo $\lambda$ y sus variaciones, aprovechando el lenguaje interno metateórico del modelo categórico. Reconocen que las e-graphs con ranuras pueden ser más flexibles para lenguajes con vínculos arbitrarios (como el $\pi$-calculus), pero argumentan que su método es superior para las optimizaciones específicas del cálculo $\lambda$.

El trabajo no presenta una implementación de software completa ni benchmarks empíricos en este artículo, sino que posiciona la representación de e-hipergrafos cerrados como una base viable para construir "e-graphs para la reescritura de diagramas de cuerdas" en trabajos futuros.