El problema fundamental que abordan los Lifting E-Graphs es la gestión del contexto y la aridad de las funciones en sistemas de reescritura de términos, como los e-graphs. La notación matemática tradicional a menudo oculta el contexto (ej. sin(x) puede referirse a x |-> sin(x) : R -> R o x,y |-> sin(x) : R^2 -> R), lo que lleva a tres problemas en sistemas automatizados: generación redundante de nombres, compartición ineficiente de subestructuras (demasiado poca o demasiada) y, sorprendentemente, la posible "conflación" de objetos semánticamente distintos.

La tesis central es que "el contexto no es dónde está un término, es parte de lo que es un término". Esto implica que la aridad y las variables de un término deben ser explícitas y parte integral de su identidad. Los Lifting E-Graphs resuelven esto al integrar operaciones de 'lifting' (que transforman funciones de menor aridad en funciones de mayor aridad ignorando argumentos adicionales) directamente en la estructura de los e-graphs, permitiendo una representación más compacta y semánticamente precisa de términos con contextos variables. Esto es crucial para la optimización de programas donde la misma lógica puede aplicarse en diferentes contextos de variables, y donde la gestión eficiente de la equivalencia y la compartición es clave.

Arquitectura del Sistema

La arquitectura de los Lifting E-Graphs se basa en una extensión de los e-graphs tradicionales, que utilizan una estructura de datos de Union-Find para representar clases de equivalencia de términos. En lugar de nombres explícitos para las variables, se utilizan pares (dimensión, índice) (ej. x_10 para la variable cero en un contexto de una dimensión). Las funciones también se "disambiguan" por su aridad (ej. sin_1 para R -> R, sin_2 para R^2 -> R).

El componente clave es la operación de 'lifting', que se representa explícitamente como un combinador lift_i(X), donde i es un bitvector que indica qué argumentos se mantienen y cuáles se descartan. Por ejemplo, lift_10(f(x_10)) transforma f: R -> R en f: R^2 -> R ignorando el segundo argumento. Este combinador permite que términos semánticamente relacionados, pero con diferentes aridades, compartan subestructuras. Las propiedades del lifting se codifican como reglas de reescritura (ej. sin(lift_i(X)) = lift_i(sin(X)) y lift_i(lift_j(X)) = lift_k(X) donde k = i . j).

La implementación se apoya en un "smart constructor" que, al construir un nuevo nodo, examina los liftings comunes de sus argumentos, los "despega", intercala el enodo base y luego vuelve a aplicar el lifting común. Esto asegura la canonización y la máxima compartición. El Union-Find se adapta para manejar "fat eids" que incluyen la anotación de lifting. Cuando se unen lift_i(a) = lift_i(b), se puede inferir a = b. Casos más complejos, como x * 0 = 0, se manejan orientando la unión para que el lado "solvable" (ej. e47 -> lift_0(e6)) sea el padre, similar a un Union-Find con anotaciones de offset. El e-matching se extiende para considerar los liftings en los patrones, permitiendo diferentes estrategias de búsqueda.

Proceso de Smart Constructor con Lifting

  1. 1 Construir Enodo Se intenta construir un nuevo enodo con argumentos que son 'fat eids' (eid + ...
  2. 2 Examinar Liftings El smart constructor analiza los liftings de todos los argumentos.
  3. 3 Extraer Lifting Común Se identifica y 'despega' el lifting común a todos los argumentos.
  4. 4 Internar Enodo Base El enodo sin el lifting común se intercala en el memo table para obtener un e...
  5. 5 Aplicar Lifting Común El lifting común se vuelve a aplicar al eid base.
  6. 6 Retornar Fat EID Se devuelve el 'fat eid' resultante (eid base + lifting común) al usuario.

Trade-offs

Ganancias
  • ▲ Compartición de subestructuras
  • ▲ Coherencia semántica
  • ▲ Reducción de redundancia de nombres
Costes
  • △ Complejidad de implementación de e-matching
  • △ Posible aumento de la complejidad de reglas de reescritura 
type Thin = list[bool]
type Id = tuple[Thin, int]
Define un tipo 'Thin' para representar el bitvector de lifting y 'Id' como un par (Thin, int) para un 'fat eid'.
@dataclass
class Node:
    f : str
    args : tuple[Id, ...]
Define la estructura de un nodo en el e-graph, incluyendo el símbolo de la función y sus argumentos (fat eids).

Fundamentos Teóricos

La problemática de la gestión de variables y contextos en sistemas de reescritura de términos tiene profundas raíces en la teoría de tipos y la lógica. La distinción entre x |-> sin(x) y x,y |-> sin(x) es un ejemplo clásico de la importancia de la aridad y el tipo en sistemas formalmente rigurosos. El uso de índices de De Bruijn para representar variables ligadas en cálculo lambda es un precursor de la idea de referirse a variables por su posición en lugar de nombres explícitos, eliminando problemas de captura de variables y renombrado alfa. El concepto de 'thinning' o 'weakening' es fundamental en la teoría de categorías y en los cálculos de tipos con dependencias, donde se formaliza cómo un contexto puede ser extendido sin afectar el significado de un término.

La idea de un Union-Find con anotaciones (como los offsets enteros en un Group Union-Find) se extiende aquí para manejar las anotaciones de lifting, lo que recuerda a las técnicas de Abstract Congruence Closure de Bachmair y Tiwari (2000), que buscan generalizar la congruencia a contextos más abstractos. La conexión con el estilo co-De Bruijn de normalizar términos lambda, como se describe en el trabajo de Conor McBride (2018), sugiere que la integración del contexto en la identidad del término es una dirección prometedora para la representación de lenguajes con ligadores.