E-graf

V informatice je e-graf datová struktura, která ukládá relaci ekvivalence nad termy nějakého jazyka.

Nechť jsou ${\displaystyle f,g,\ldots }$ symboly funkcí v nějakém jazyce, a nechť jsou ${\displaystyle t_{1},\ldots }$ termy v tomtéž jazyce. Nechť je ${\displaystyle \mathbb {id} }$ spočetná množina neprůhledných identifikátorů, u nichž lze ověřovat rovnost. Tuto množinu nazýváme identifikátory e-tříd. Potom e-uzel je symbol n-ární funkce společně s ${\displaystyle n}$ identifikátory e-tříd. E-třída je množina e-uzlů. E-graf obsahuje datovou strukturu disjunktních množin ${\displaystyle U}$ nad identifikátory e-tříd se standardními operacemi ${\displaystyle \mathrm {add} }$, ${\displaystyle \mathrm {find} }$, a ${\displaystyle \mathrm {merge} }$.

Identifikátor e-tříd ${\displaystyle e}$ je kanonický, pokud ${\displaystyle \mathrm {find} (U,e)=e}$. E-uzel ${\displaystyle f(i_{1},\ldots ,i_{n})}$ (kde ${\displaystyle i_{1},\ldots ,i_{n}\in \mathbb {id} }$) je kanonický, pokud je každý ${\displaystyle i_{j}}$ kanonický (kde ${\displaystyle j}$ je v ${\displaystyle 1,\ldots ,n}$ ).

E-graf je kombinací: ^[1]

• struktury disjunktních množin ${\displaystyle U}$
• hashcons ${\displaystyle H}$ (tj. zobrazení) z kanonických e-uzlů na identifikátory e-tříd
• zobrazení e-tříd ${\displaystyle M}$ které zobrazuje identifikátory e-tříd na e-třídy tak, že ${\displaystyle M}$ přiřadí ekvivalentním identifikátorům stejnou množinu e-uzlů: ${\displaystyle \forall i,j\in \mathbb {id} ,M[i]=M[j]\Leftrightarrow \mathrm {find} (U,i)=\mathrm {find} (U,j)}$

Kromě výše uvedené struktury vyhovuje platný e-graf několika datovým invariantám. ^[1] Dva e-uzly jsou ekvivalentní, pokud jsou ve stejné e-třídě. Invarianta kongruence uvádí, že e-graf musí zajistit, aby byla ekvivalence uzavřena v rámci kongruence, kde dva e-uzly ${\displaystyle f(i_{1},\ldots ,i_{n}),f(j_{1},\ldots ,j_{n})}$ jsou kongruentní, když ${\displaystyle \mathrm {find} (U,i_{k})=\mathrm {find} (U,j_{k}),k\in \{1,\ldots ,n\}}$. Invarianta hashcons postuluje, že hashcons mapuje kanonické e-uzly na identifikátor jejich e-třídy.

E-grafy poskytují abstrakci kolem operací ${\displaystyle \mathrm {add} }$, ${\displaystyle \mathrm {find} }$, a ${\displaystyle \mathrm {merge} }$ ze struktury disjunktních množin, které zachovávají e-grafové invarianty. Další operací je e-párování. Ten mapuje „vzory“ (termy s proměnnými) na n-tice substitucí (od vzorů k identifikátorům e-tříd) a na identifikátory e-tříd tak, že vrácené e-třídy obsahují uzly, které odpovídají vstupnímu vzoru po aplikování substituce.

Saturace rovností je technika vytváření optimalizujících překladačů pomocí e-grafů. ^[2] Funguje tak, že aplikuje sadu přepisovacích pravidel pomocí e-párování, dokud není e-graf nasycený, nevyprší časový limit, není dosaženo limitu velikosti e-grafu, není překročen určitý počet iterací nebo není dosaženo jiné zastavovací podmínky. Po přepisování se z e-grafu extrahuje optimální term podle nějaké nákladové funkce, obvykle související s velikostí AST nebo výkonem.

E-grafy se používají v automatických důkazových systémech. Tvoří klíčovou součást moderních SMT solverů, jako jsou Z3 ^[3] a CVC4.

Saturace rovností se používá ve specializovaných optimalizujících kompilátorech, ^[4] např. pro hluboké učení ^[5] a lineární algebru. ^[6] Saturace rovností byla také použita při validaci překladu aplikovanou na sadu nástrojů LLVM. ^[7]

V tomto článku byl použit překlad textu z článku E-graph na anglické Wikipedii.

• DE MOURA, Leonardo; BJØRNER, Nikolaj. Efficient E-Matching for SMT Solvers. S. 183–198. Redakce Frank Pfenning. Automated Deduction – CADE-21 [online]. Springer [cit. 2007]. Roč. 4603, s. 183–198. Dostupné online. DOI 10.1007/978-3-540-73595-3_13. (anglicky) 
• WILLSEY, Max; NANDI, Chandrakana; WANG, Yisu Remy, Oliver Flatt, Zachary Tatlock, Pavel Panchekha. egg: Fast and extensible equality saturation. S. 23:1–23:29. Proceedings of the ACM on Programming Languages [online]. [cit. 2021-01-04]. Roč. 5, s. 23:1–23:29. Dostupné online. arXiv 2004.03082. DOI 10.1145/3434304. s2cid 226282597. 
• TATE, Ross; STEPP, Michael; TATLOCK, Zachary, Lerner Sorin. Equality saturation: a new approach to optimization. S. 263–276, Savannah, GA, USA. Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages [online]. Association for Computing Machinery [cit. 2009-01-21]. S. 263–276. Dostupné online. DOI 10.1145/1480881.1480915. s2cid 2138086, ISBN 978-1-60558-379-2. 

• The Egg Project^{[nedostupný zdroj]}
• Google Colab notebook vysvětlující e-grafy