E-graf

Inom datavetenskap är en e-graf en datastruktur som lagrar en ekvivalensrelation över termer av något språk.

Definition och verksamhet

Låt $\Sigma$ vara en uppsättning funktionssymboler, låt $\Sigma _{n}$ vara delmängden av $\Sigma$ som består av symboler för arity $n$ . Låt $\mathbb {id}$ vara en räknebar uppsättning ogenomskinliga identifierare som kan jämföras för likhet, kallade e-klass-ID:n . Då är en e-nod en $n$ -är funktionssymbol tillsammans med $n$ e-klass-ID. En e-nod med $n$ -är funktionssymbol $f\in \Sigma _{n}$ och e-klass-ID: $i_{1},i_{2},\ldots ,i_{n}\in \mathbb {id}$ betecknas $f(i_{ 1},i_{2},\ldots ,i_{n})$ . En e-klass är en uppsättning e-noder. En e-graf innehåller en union-find- struktur $U$ över e-klass-ID:n med standardoperationer $\mathrm {add}$ , $\mathrm {find$ , och $\mathrm {sammanfoga}$ .

Ett e-klass-ID $e$ är kanoniskt om $\mathrm {find} (U,e)=e$ . En e-nod $f(i_{1},\ldots ,i_{n})$ (med $i_{ 1},\ldots ,i_{n}\in \mathbb {id}$ ) är kanonisk om varje $i_{j}$ är kanonisk ( $j$ i ${\ displaystyle 1,\ldots ,n}$ ).

En e-graf är kombinationen av:

union-find-strukturen $U$ ,
en hashcons $H$ (dvs en mappning) från kanoniska e-noder till e-klass-ID, och
en e-klasskarta $M$ som mappar e-klass-ID:n till e-klasser, så att $M$ mappar motsvarande ID:n till samma uppsättning e-noder: $\forall i,j\in \mathbb {id} ,M[i]= M[j]\Leftrightarrow \mathrm {hitta} (U,i)=\mathrm {hitta} (U,j)$

Invarianter

Förutom ovanstående struktur överensstämmer en giltig e-graf med flera datastrukturinvarianter . Två e-noder är likvärdiga om de är i samma e-klass. Kongruensinvarianten ${\displaystyle f(i_ {1},\ldots ,i_{n}),f(j_{1},\ldots,j_{n})} är$ graf måste säkerställa att ekvivalensen stängs under kongruens , där två e-noder , kongruenta när $\mathrm {find} (U,i_{k})=\mathrm {hit} (U,j_{k}),k\in \{1 ,\ldots ,n\}$ . Hashcons -invarianten anger att hashcons mappar kanoniska e-noder till deras e-klass-ID.

Operationer

E-grafer exponerar omslag runt a $\displaystyle \mathrm {add} }$ , $\mathrm {find}$ , och $mathrm {merge} }$ displaystyle från det fackliga fyndet som bevarar e-grafens invarianter. Den sista operationen, e-matchning, beskrivs nedan.

E-matchning

Låt $V$ vara en uppsättning variabler och låt $\mathrm {Term} (\Sigma ,V)$ vara den minsta uppsättningen som inkluderar 0-aritetsfunktionssymbolerna (även kallade konstanter ), inkluderar variablerna och stängs under tillämpning av funktionssymbolerna. Med andra ord, $\mathrm {Term} (\Sigma ,V)$ är den minsta mängden så att $V\ delmängd \mathrm {Term} (V,\Sigma )$ , $\Sigma _{0}\subset \mathrm {Term} (\Sigma ,V)$ och när $x_{1},\ldots ,x_{n}\in \mathrm {Term} (\Sigma ,V)$ och $f\in \Sigma _{n}$ , sedan $f(x_{1},\ldots , x_{n})\in \mathrm {Term} (\Sigma ,V)$ . En term som innehåller variabler kallas ett mönster , en term utan variabler kallas mark .

En e-graf $E$ representerar en grundterm $t\in \mathrm {Term} (\Sigma ,\emptyset )$ om en av dess e- klasser representerar $t$ . En e-klass $C$ representerar $t$ om någon e-nod $f(i_{1},\ldots ,i_{n })\in C$ gör det. En e-nod $f(i_{1},\ldots ,i_{n})\in C$ representerar en term $g(j_{1},\ldots ,j_{n})$ om $f=g$ och varje e-klass $M[i_{k} ]$ representerar termen $j_{k}$ ( $k$ i $1,\ldots ,n$ ).

e-matchning är en operation som tar ett mönster $p\in \mathrm {Term} (\Sigma ,V)$ och en e-graf $E$ , och ger alla par $(\sigma ,C)$ där $\sigma \subset V\times \mathbb {id}$ är en substitutionsmappning av variablerna i $p$ till e-klass-ID och $C\in \mathbb {id}$ är ett e-klass-ID så att varje term $\sigma (p)$ representeras av $C$ . Det finns flera kända algoritmer för e-matchning.

Jämställdhetsmättnad

Jämlikhetsmättnad är en teknik för att bygga optimera kompilatorer med hjälp av e-grafer. Den fungerar genom att tillämpa en uppsättning omskrivningar med e-matchning tills e-grafen är mättad, en timeout nås, en e-grafstorleksgräns har nåtts, ett fast antal iterationer överskrids eller något annat stopptillstånd uppnås. Efter omskrivning extraheras en optimal term från e-grafen enligt någon kostnadsfunktion, vanligtvis relaterad till AST- storlek eller prestandaöverväganden.

Ansökningar

E-grafer används vid automatiserad satsbevisning . De är en avgörande del av moderna SMT-lösare som Z3 och CVC4 . De används också i Simplify theorem prover av ESC/Java .

Jämlikhetsmättnad används i specialiserade optimeringskompilatorer , t.ex. för djupinlärning och linjär algebra . Jämlikhetsmättnad har också använts för översättningsvalidering tillämpad på LLVM -verktygskedjan.

E-grafer har tillämpats på flera problem i programanalys , inklusive fuzzing, abstrakt tolkning och biblioteksinlärning.

de Moura, Leonardo; Bjørner, Nikolaj (2007). Pfenning, Frank (red.). "Effektiv e-matchning för SMT-lösare" . Automatiskt avdrag – CADE-21 . Föreläsningsanteckningar i datavetenskap. Berlin, Heidelberg: Springer. 4603 : 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). "ägg: Snabb och utvidgbar jämställdhetsmättnad" . Proceedings of ACM on Programming Languages . 5 (POPL): 23:1–23:29. arXiv : 2004.03082 . doi : 10.1145/3434304 . S2CID 226282597 .
Tate, Ross; Stepp, Michael; Tatlock, Zachary; Lerner, Sorin (2009-01-21). "Jämställdhetsmättnad: ett nytt tillvägagångssätt för optimering" . Handlingar från det 36:e årliga ACM SIGPLAN-SIGACT-symposiet om principer för programmeringsspråk . POPL '09. Savannah, GA, USA: Association for Computing Machinery: 264–276. doi : 10.1145/1480881.1480915 . ISBN 978-1-60558-379-2 . S2CID 2138086 .

externa länkar