等式飽和とe-graph

等式飽和 (Equality Saturation) は、項に書き換え規則を非破壊的に適用し続け、到達可能な等価項をすべて保持してから最適なものを抽出する最適化・探索手法。2009年の “Equality saturation: a new approach to optimization” で提案された。古典的なequality-saturation（破壊的書き換え）が抱えるフェーズ順序問題（どの規則をどの順で適用するか）を、すべての書き換えを同時に保持することで回避する。

e-graph

中核となるデータ構造が e-graph (equivalence graph)。項の集合とその上の合同関係 (congruence) をコンパクトに表す。

• e-class: 等価な項の集合。union-find ($U$) で id を管理。
• e-node: 演算子 $f$ と引数（引数は e-class への参照）。canonicalize(f(a_1,...)) = f(find(a_1),...)。
• 部分木は可能な限り共有され（hash consing 的）、指数的な数の等価項を高い共有で保持できる。DAG に似る。
• e-graph $(U,M,H)$ は3つの合同関係を表す: e-class id の同一性 ${\equiv }_{id}$、e-node の同一性 ${\equiv }_{node}$、項の同一性 ${\equiv }_{term}$。

アルゴリズム: 初期項を挿入 → 規則集合を繰り返しマッチ・追加（マージのみ、消去しない）→ 飽和（新たな等価性が出ない）かタイムアウトまで継続 → コスト関数で最良項を extract する。

主要実装と拡張

• egg: Max Willsey らによる Rust 実装。rebuilding（合同の遅延回復）と e-class analysis（join semilattice 上の解析）で高速・拡張可能。
• Metatheory.jl: Julia 実装。EGraph → saturate! → extract!。
• e-graph intersection: 2つの e-graph の共通部分を飽和に似た手続きで計算（合成・検証に応用）。
• proof-producing congruence closure: 等価性に証明（説明）を付与し、Lean 等の証明項を再構築。

応用

• コンパイラ最適化（浮動小数点精度改善 Herbie、線形代数 SPORES、ベクトル化 diospyros）。
• テンソルグラフのスーパー最適化 (TENSAT、TASO の再実装)。
• CAD モデル合成 (Szalinski)、書き換え規則の自動発見、sketch-guided な大規模式の誘導。
• 定理証明: egg を Lean 4 のタクティクとして統合（Marcus Rossel）。束縛変数を第一級に扱う slotted e-graph (PLDI 2025) を生み、Terence Tao 主導の Equational Theories Project で4694法則・約2200万含意の検証を支えた。

関連

• 基盤はequality-saturation、束縛変数の扱いはlambda-calculus。
• 抽出はコンパイラ最適化 compiler-optimization と直結。
• _moc-lang-compilers

項書換えと抽象書き換え

項書換えシステム (Term Rewriting System, TRS) は、書き換え規則 $\ell ⇝r$ の集合により項を変換していく計算モデル。計算そのものを書き換えとして表し、書き換えは一般に非決定的。抽象書き換え (Abstract Rewriting) はこれを抽象化した分野で、言語クラス・論理学・圏論とも関連する。

正規形と効率

• TRS の応用では正規形 (normal form) の計算が基本手続き。言語の意味論は項の正規形であり、単語問題や方程式論の項の統一にも正規形が使われる。
• 木として素朴に書き換えると非効率なので、DAG 表現で部分項を共有すると効率化できる。非左線形システムでも効率的な戦略が得られる。
• 論理回路合成では AIG (And-Inverter Graph) の DAG-aware rewriting、FHE 回路の乗算深さ最小化では cone rewriting（DVD 問題＝Dag vertex deletion problem としての組合せ最適化）など、ドメイン特化の書き換えがある。

グラフ簡約と発展

• グラフ簡約 (graph reduction): 項を木でなくグラフで表し共有を保ちながら簡約する手法。関数型言語処理系の実行モデルの基礎で、lambda-calculusへ繋がる。
• 破壊的な書き換えは局所解やループに陥るため、非破壊的に等価項を保持するequality-saturation（e-graph）へ発展した。

関連

• 非破壊版はequality-saturation、簡約戦略の最適化はlambda-calculus。
• λ項の簡約規則はlambda-calculus。
• _moc-lang-compilers