E-Matching eficiente: Una nueva herramienta para compiladores optimizadores

Los probadores de teoremas modernos y los compiladores optimizadores se basan en una técnica inteligente: E-matching. No solo coincide con la sintaxis, sino que, lo que es más importante, coincide con la semántica, logrando el razonamiento de equivalencia a través de E-graphs y el cierre de congruencia. Este artículo profundiza en los principios del E-matching, en particular, cómo encontrar patrones coincidentes en E-graphs de manera eficiente utilizando árboles de discriminación y cierre de congruencia, evitando la ineficiencia del recorrido recursivo tradicional. El autor también presenta su aplicación en el compilador Zob, compilando patrones en instrucciones de máquina virtual para E-matching eficiente, mejorando significativamente la eficiencia de la optimización.