E-graf

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

Definice a operace

Nechť jsou $f,g,\dots$ symboly funkcí v nějakém jazyce, a nechť jsou $t_1,\dots$ termy v tomtéž jazyce. Nechť je $𝕚𝕕$ 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 $n$ identifikátory e-tříd. E-třída je množina e-uzlů. E-graf obsahuje datovou strukturu disjunktních množin $U$ nad identifikátory e-tříd se standardními operacemi $\mathrm{a}\mathrm{d}\mathrm{d}$, $\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{d}$, a $\mathrm{m}\mathrm{e}\mathrm{r}\mathrm{g}\mathrm{e}$.

Identifikátor e-tříd $e$ je kanonický, pokud $\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{d}(U,e)=e$. E-uzel $f(i_1,\dots ,i_n)$ (kde $i_1,\dots ,i_n\in 𝕚𝕕$) je kanonický, pokud je každý $i_j$ kanonický (kde $j$ je v $1,\dots ,n$ ).

E-graf je kombinací:

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

Invarianty

Kromě výše uvedené struktury vyhovuje platný e-graf několika datovým invariantám. 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 $f(i_1,\dots ,i_n),f(j_1,\dots ,j_n)$ jsou kongruentní, když $\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{d}(U,i_k)=\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{d}(U,j_k),k\in \{1,\dots ,n\}$. Invarianta hashcons postuluje, že hashcons mapuje kanonické e-uzly na identifikátor jejich e-třídy.

Operace

E-grafy poskytují abstrakci kolem operací $\mathrm{a}\mathrm{d}\mathrm{d}$, $\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{d}$, a $\mathrm{m}\mathrm{e}\mathrm{r}\mathrm{g}\mathrm{e}$ 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í

Saturace rovností je technika vytváření optimalizujících překladačů pomocí e-grafů. 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.

Použití

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 a CVC4.

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

Reference

• Šablona:Citace elektronického periodika
• Šablona:Citace elektronického periodika
• Šablona:Citace elektronického periodika

Externí odkazy

• The Egg ProjectŠablona:Nedostupný zdroj
• Google Colab notebook vysvětlující e-grafy