Los Refinement E-Graphs son una extensión teórica de los grafos de ecuaciones (e-graphs) que introduce una relación de refinamiento (<=) para modelar reescrituras unidireccionales en compiladores. A diferencia de las igualdades bidireccionales, esta relación permite transitar de especificaciones abstractas o 'flojas' a programas concretos y deterministas, aprovechando la ambigüedad inherente a los lenguajes de programación para maximizar las oportunidades de optimización.
El artículo detalla un prototipo implementado en WASM basado en el framework microegg, utilizando el concepto de 'Don't Care' en circuitos digitales como caso de estudio. En este ejemplo, el término 'dontcare' representa un conjunto de valores posibles (como {True, False}) que se refina a valores específicos (True o False) según el contexto, permitiendo al optimizador elegir la salida más eficiente sin forzar una igualdad estricta. Esta semántica se modela mediante la inclusión puntual de conjuntos, donde la desigualdad implica que el conjunto de un término es subconjunto del otro.
Técnicamente, la implementación requiere una estructura de 'inequality union find' que combine la búsqueda de uniones con la gestión de consistencia de hashes. A diferencia del cierre de congruencia tradicional, el cierre de refinamiento aplica teoremas de monotonicidad y contravariancia para mantener relaciones de orden entre nodos. Este enfoque permite a los compiladores manejar funciones con comportamientos complejos, como la diferencia de conjuntos, donde la monotonicidad varía según los argumentos, facilitando la extracción de términos y la optimización de código a nivel de bajo nivel.