電子グラフ

コンピュータサイエンスにおいて、eグラフとは、ある言語の項間の同値関係を格納するデータ構造のことである。

させて${\displaystyle \Sigma }$は解釈されていない関数の集合であり、$\displaystyle \Sigma _{n}}$は、${\displaystyle \Sigma }$アリティ関数から構成される${\displaystyle n}$。 させて${\displaystyle \mathbb {id} }$等価性を比較できる不透明な識別子の可算集合であり、eクラスIDと呼ばれる。${\displaystyle f\in \Sigma _{n}}$eクラスIDへ${\displaystyle i_{1},i_{2},\ldots ,i_{n}\in \mathbb {id} }$と表記される${\displaystyle f(i_{1},i_{2},\ldots ,i_{n})}$そしてeノードと呼ばれる。

e -graph は、次のデータ構造を使用して e-node の同値類を表します。^{[ 1 ]}

• ユニオンファインド構造${\displaystyle U}$eクラスIDの同値クラスを表し、通常の操作を行う${\displaystyle \mathrm {検索} }$、${\displaystyle \mathrm {追加} }$そして${\displaystyle \mathrm {マージ} }$eクラスID${\displaystyle e}$正典である場合${\displaystyle \mathrm {find} (U,e)=e}$電子ノード${\displaystyle f(i_{1},\ldots ,i_{n})}$ それぞれが正典である場合${\displaystyle i_{j}}$正典です（${\displaystyle j}$で${\displaystyle 1,\ldots ,n}$)
• e-クラスIDとe-ノードのセット（e-クラスと呼ばれる）との関連付け。これは以下から構成されます。
  • ハッシュコン${\displaystyle H}$（つまり、eノードからeクラスIDへのマッピング）
  • eクラスの地図${\displaystyle M}$eクラスIDをeクラスにマッピングし、${\displaystyle M}$同等のIDを同じeノードセットにマッピングします。${\displaystyle \forall i,j\in \mathbb {id} ,M[i]=M[j]\Leftrightarrow \mathrm {find} (U,i)=\mathrm {find} (U,j)}$

させて${\displaystyle V}$を変数の集合とし、${\displaystyle \mathrm {用語} (\Sigma ,V)}$は、0 項関数記号 (定数とも呼ばれる) を含み、変数を含み、関数記号の適用に関して閉じている最小の集合である。言い換えれば、${\displaystyle \mathrm {用語} (\Sigma ,V)}$は、${\displaystyle V\subset \mathrm {用語} (\Sigma ,V)}$、${\displaystyle \Sigma _{0}\subset \mathrm {Term} (\Sigma ,V)}$、そして${\displaystyle x_{1},\ldots ,x_{n}\in \mathrm {Term} (\Sigma ,V)}$そして${\displaystyle f\in \Sigma _{n}}$、 それから${\displaystyle f(x_{1},\ldots ,x_{n})\in \mathrm {Term} (\Sigma ,V)}$変数を含む項はパターンと呼ばれ、変数を含まない項はグラウンドと呼ばれます。

電子グラフ${\displaystyle E}$基底項を表す$\displaystyle t\in \mathrm {Term} (\Sigma ,\emptyset )}$そのeクラスの1つが${\displaystyle t}$eクラス${\displaystyle C}$表現する${\displaystyle t}$もしあるeノードが${\displaystyle f(i_{1},\ldots ,i_{n})\in C}$そうです。eノード${\displaystyle f(i_{1},\ldots ,i_{n})\in C}$用語を表す${\displaystyle g(j_{1},\ldots ,j_{n})}$もし${\displaystyle f=g}$そして各eクラス${\displaystyle M[i_{k}]}$用語を表す${\displaystyle j_{k}}$（${\displaystyle k}$で${\displaystyle 1,\ldots ,n}$)

e-マッチングは、パターンを受け取る操作です。${\displaystyle p\in \mathrm {Term} (\Sigma ,V)}$そして電子グラフ${\displaystyle E}$、そしてすべてのペアを生成します${\displaystyle (\sigma ,C)}$どこ${\displaystyle \sigma \subset V\times \mathbb {id} }$は、変数をマッピングする置換です。${\displaystyle p}$eクラスIDと${\displaystyle C\in \mathbb {id} }$は、用語が${\displaystyle \sigma (p)}$は${\displaystyle C}$e-マッチングにはいくつかの既知のアルゴリズムがあり、^{[ 4 ] [ 5 ]}関係e-マッチングアルゴリズムは最悪ケース最適結合に基づいており、最悪ケース最適である。^{[ 6 ]}

e-クラスと、各関数シンボルをマッピングするコスト関数が与えられた場合、${\displaystyle \Sigma }$自然数への抽出問題は、与えられたeクラスによって表現される総コストが最小となる基底項を見つけることです。この問題はNP困難です。^{[ 7 ]}また、この問題には定数係数近似アルゴリズム も存在せず、これは集合被覆問題からの還元によって示されます。ただし、木幅が制限されているグラフの場合、線形時間で固定パラメータの扱いやすいアルゴリズムが存在します。^{[ 8 ]}

• n 個の等式を持つ e-graph はO( n log n ) 時間で構築できます。^{[ 9 ]}

等価飽和は、eグラフを使用して最適化コンパイラを構築するための手法です。^{[ 10 ]}この手法は、eグラフが飽和するか、タイムアウトに達するか、eグラフのサイズ制限に達するか、固定回数の反復を超えるか、またはその他の停止条件に達するまで、eマッチングを使用して一連の書き換えを適用することによって動作します。書き換え後、通常はASTサイズまたはパフォーマンスの考慮事項に関連するコスト関数に従って、eグラフから最適な項が抽出されます。

Eグラフは自動定理証明で使用されます。Z3 ^{[ 11 ]}やCVC4などの最新のSMTソルバーの重要な部分であり、等式の集合の合同閉包を計算することで空理論を判定するために使用され、eマッチングは量化子をインスタンス化するために使用されます。^{[ 12 ]}衝突駆動型節学習（非時系列バックトラッキングとも呼ばれる）を使用するDPLL(T)ベースのソルバーでは、eグラフは証明証明書を生成するために拡張されます。^{[ 13 ]} EグラフはESC/JavaのSimplify定理証明器でも使用されます。^{[ 14 ]}

等価性飽和は、ディープラーニング^{[ 16 ]}、線形代数^{[ 17 ]} 、デジタル信号プロセッサの自動ベクトル化^{[ 18 ]}などの特殊な最適化コンパイラで使用されています^{[ 15 ]} 。等価性飽和は、 LLVMツールチェーンに適用される翻訳検証にも使用されています^{[ 19 ]}。

Eグラフは、ファジング^{[ 20 ]}、抽象解釈^{[ 21 ]}、ライブラリ学習^{[ 22 ]}など、プログラム解析におけるいくつかの問題に適用されてきた。

• de Moura, Leonardo; Bjørner, Nikolaj (2007). "SMTソルバーのための効率的なEマッチング" . Pfenning, Fr​​ank (編).自動推論 – CADE-21 . Lecture Notes in Computer Science. Vol.  4603. Berlin, 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: 高速で拡張可能な等価性飽和" . Proceedings of the 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年1月21日) 「等価性飽和」 .第36回ACM SIGPLAN-SIGACTプログラミング言語原理シンポジウム議事録. POPL '09. 米国ジョージア州サバンナ: Association for Computing Machinery. pp. 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 (2022年10月) 「合同閉包からの小さな証明」 A. Griggio; N. Rungta (編)『第22回コンピュータ支援設計における形式手法に関する会議 – FMCAD 2022 議事録』 TU Wien Academic Press、pp. 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). "疎な等価グラフの高速かつ最適な抽出" . ACM プログラミング言語に関する論文集. 8 (OOPSLA2): 361:2551–361:2577. doi : 10.1145/3689801 .

• エッグプロジェクト
• eグラフを説明するColabノートブック