Gráfico electrónico

En informática , un e-grafo es una estructura de datos que almacena una relación de equivalencia entre términos de algún lenguaje.

Dejar${\displaystyle \Sigma }$sea ​​un conjunto de funciones no interpretadas , donde${\displaystyle \Sigma _{n}}$es el subconjunto de${\displaystyle \Sigma }$que consta de funciones de aridad${\displaystyle n}$. Dejar${\displaystyle \mathbb {id} }$ser un conjunto contable de identificadores opacos que se pueden comparar para comprobar su igualdad, llamados identificadores de clase e . La aplicación de${\displaystyle f\in \Sigma _{n}}$a identificadores de clase electrónica${\displaystyle i_{1},i_{2},\ldots ,i_{n}\in \mathbb {id} }$se denota${\displaystyle f(i_{1},i_{2},\ldots ,i_{n})}$y se denomina e-nodo .

El grafo electrónico representa entonces clases de equivalencia de nodos electrónicos, utilizando las siguientes estructuras de datos: ^{[ 1 ]}

• Una estructura de unión-hallazgo${\displaystyle U}$representando clases de equivalencia de identificadores de clase e, con las operaciones habituales${\displaystyle \mathrm {buscar} }$,${\displaystyle \mathrm {agregar} }$y${\displaystyle \mathrm {fusionar} }$Un ID de clase electrónica${\displaystyle e}$es canónico si${\displaystyle \mathrm {buscar} (U,e)=e}$; un nodo electrónico${\displaystyle f(i_{1},\ldots ,i_{n})}$ es canónico si cada${\displaystyle i_{j}}$es canónico (${\displaystyle j}$en${\displaystyle 1,\ldots ,n}$).
• Una asociación de identificadores de clases electrónicas con conjuntos de nodos electrónicos, denominados clases electrónicas . Esto consiste en:
  • un hashcons${\displaystyle H}$(es decir, una asignación) de e-nodos a identificadores de e-clase, y
  • un mapa de clase electrónica${\displaystyle M}$que asigna identificadores de clases electrónicas a clases electrónicas, de tal manera que${\displaystyle M}$asigna identificadores equivalentes al mismo conjunto de nodos electrónicos:${\displaystyle \forall i,j\in \mathbb {id} ,M[i]=M[j]\Leftrightarrow \mathrm {buscar} (U,i)=\mathrm {buscar} (U,j)}$

Dejar${\displaystyle V}$sea ​​un conjunto de variables y dejemos que${\displaystyle \mathrm {Término} (\Sigma,V)}$sea ​​el conjunto más pequeño que incluye los símbolos de función de aridad 0 (también llamados constantes ), incluye las variables y es cerrado bajo la aplicación de los símbolos de función. En otras palabras,${\displaystyle \mathrm {Término} (\Sigma,V)}$es el conjunto más pequeño tal que${\displaystyle V\subset \mathrm {Término} (\Sigma,V)}$,${\displaystyle \Sigma _{0}\subset \mathrm {Término} (\Sigma ,V)}$y cuando${\displaystyle x_{1},\ldots ,x_{n}\in \mathrm {Término} (\Sigma ,V)}$y${\displaystyle f\in \Sigma _{n}}$, entonces${\displaystyle f(x_{1},\ldots ,x_{n})\in \mathrm {Término} (\Sigma ,V)}$. Un término que contiene variables se llama patrón , un término sin variables se llama base .

Un gráfico electrónico${\displaystyle E}$representa un término fundamental${\displaystyle t\in \mathrm {Término} (\Sigma ,\emptyset )}$si una de sus clases electrónicas representa${\displaystyle t}$Una clase electrónica${\displaystyle C}$representa${\displaystyle t}$si algún enodo${\displaystyle f(i_{1},\ldots ,i_{n})\in C}$Sí. Un e-nodo${\displaystyle f(i_{1},\ldots ,i_{n})\in C}$representa un término${\displaystyle g(j_{1},\ldots ,j_{n})}$si${\displaystyle f=g}$y cada clase electrónica${\displaystyle M[i_{k}]}$representa el término${\displaystyle j_{k}}$(${\displaystyle k}$en${\displaystyle 1,\ldots ,n}$).

El emparejamiento electrónico es una operación que toma un patrón.${\displaystyle p\in \mathrm {Term} (\Sigma ,V)}$y un gráfico electrónico${\displaystyle E}$y produce todos los pares${\displaystyle (\sigma ,C)}$dónde${\displaystyle \sigma \subset V\times \mathbb {id} }$es una sustitución que mapea las variables en${\displaystyle p}$a los identificadores de clase electrónica y${\displaystyle C\in \mathbb {id} }$es un ID de clase electrónica tal que el término${\displaystyle \sigma (p)}$está representado por${\displaystyle C}$. Existen varios algoritmos conocidos para el emparejamiento electrónico, ^{[ 4 ] [ 5 ]} el algoritmo de emparejamiento electrónico relacional se basa en uniones óptimas en el peor de los casos y es óptimo en el peor de los casos. ^{[ 6 ]}

Dado una clase e y una función de costo que asigna cada símbolo de función en${\displaystyle \Sigma }$Para un número natural, el problema de extracción consiste en encontrar un término base con un costo total mínimo que esté representado por la clase e dada. Este problema es NP-difícil . ^{[ 7 ]} Tampoco existe un algoritmo de aproximación de factor constante para este problema, lo cual se puede demostrar mediante una reducción del problema de cobertura de conjuntos . Sin embargo, para grafos con ancho de árbol acotado , existe un algoritmo tratable de tiempo lineal y parámetro fijo . ^{[ 8 ]}

• Se puede construir un e-grafo con n igualdades en tiempo O( n log n ). ^{[ 9 ]}

La saturación de igualdad es una técnica para construir compiladores optimizadores que utilizan grafos e. ^{[ 10 ]} Funciona aplicando un conjunto de reescrituras mediante la coincidencia de e hasta que el grafo e se satura, se alcanza un tiempo límite, se alcanza un límite de tamaño del grafo e, se supera un número fijo de iteraciones o se alcanza alguna otra condición de parada. Después de la reescritura, se extrae un término óptimo del grafo e según alguna función de coste, generalmente relacionada con el tamaño del AST o consideraciones de rendimiento.

Los grafos E se utilizan en la demostración automática de teoremas . Son una parte crucial de los solucionadores SMT modernos como Z3 ^{[ 11 ]} y CVC4 , donde se utilizan para decidir la teoría vacía calculando el cierre de congruencia de un conjunto de igualdades, y el emparejamiento E se utiliza para instanciar cuantificadores. ^{[ 12 ]} En los solucionadores basados ​​en DPLL(T) que utilizan aprendizaje de cláusulas impulsado por conflictos (también conocido como retroceso no cronológico), los grafos E se extienden para producir certificados de prueba. ^{[ 13 ]} Los grafos E también se utilizan en el demostrador de teoremas Simplify de ESC/Java . ^{[ 14 ]}

La saturación de igualdad se utiliza en compiladores optimizadores especializados , ^{[ 15 ]} por ejemplo, para aprendizaje profundo ^{[ 16 ]} , álgebra lineal ^{[ 17 ]} y autovectorización para procesadores de señales digitales ^{[ 18 ]} . La saturación de igualdad también se ha utilizado para la validación de traducción aplicada a la cadena de herramientas LLVM . ^{[ 19 ]}

Los grafos E se han aplicado a varios problemas en el análisis de programas , incluyendo fuzzing, ^{[ 20 ]} interpretación abstracta, ^{[ 21 ]} y aprendizaje de bibliotecas. ^{[ 22 ]}

• de Moura, Leonardo; Bjørner, Nikolaj (2007). "Efficient E-Matching for SMT Solvers" . En Pfenning, Frank (ed.). Automated Deduction – CADE-21 . Lecture Notes in Computer Science. Vol.  4603. Berlín, Heidelberg: Springer. pp. 183–198 . doi : 10.1007/978-3-540-73595-3_13 . ISBN  978-3-540-73595-3.
• Willsey, Max; Nandi, Chandrakana; Wang, Yisu Remy; Flatt, Oliver; Tatlock, Zachary; Panchekha, Pavel (2021-01-04). "egg: Saturación de igualdad rápida y extensible" . Actas de la ACM sobre lenguajes de programación . 5 (POPL): 23:1–23:29. arXiv : 2004.03082 . doi : 10.1145/3434304 . S2CID 226282597 . 
• Tate, Ross; Stepp, Michael; Tatlock, Zachary; Lerner, Sorin (21 de enero de 2009). «Saturación de igualdad» . Actas del 36.º simposio anual ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . POPL '09. Savannah, GA, EE. UU.: Association for Computing Machinery. págs. 264-276 . doi : 10.1145/1480881.1480915 . ISBN  978-1-60558-379-2. S2CID 2138086 . 
• Flatt, Oliver; Coward, Samuel; Willsey, Max; Tatlock, Zachary; Panchekha, Pavel (octubre de 2022). «Pequeñas pruebas a partir del cierre de congruencia» . En A. Griggio; N. Rungta (eds.). Actas de la 22.ª Conferencia sobre Métodos Formales en Diseño Asistido por Computadora – FMCAD 2022. TU Wien Academic Press. págs. 75–83 . doi : 10.34727/2022/isbn.978-3-85448-053-2_13 . ISBN  978-3-85448-053-2. S2CID 252118847 . 
• Goharshady, Amir Kafshdar; Lam, Chun Kit; Parreaux, Lionel (2024-10-08). "Extracción rápida y óptima para grafos de igualdad dispersos" . Actas de la ACM sobre lenguajes de programación . 8 (OOPSLA2): 361:2551–361:2577. doi : 10.1145/3689801 .

• El proyecto del huevo
• Un cuaderno de Colab que explica los gráficos electrónicos.