E-Graph

In computer science, an e-graph is a data structure that stores an equivalence relation over terms of some language.

• 非決定的な項書換えを行うための, 等式関係を表すデータ構造
• 古典的な書き換えは破壊的で, 書き換え前を忘れてしまうので局所解やループが発生してしまう.
• また同値の表現でも完全に一致していないとマッチ出来ない (ex. (a + b) + c = a + (b + c))
• E-GraphはDAGに似ていて, 部分木は可能な限り共有され, 順序や合流を木にすること無く書き換え規則を使うことが出来るので非決定的な項書換えが行える.
• Term Rewriting
• Equality Saturation

提案

2023-02-03

• Proof-Producing Congruence Closure

applications

• 2022-06-05
  • GitHub - JuliaCompilerPlugins/Yolk.jl: A configurable algebraic optimizer using Metatheory.jl.
    • MixTape.jl というJulia Compiler plugin用に E-Graph で最適化するパッケージらしい

参考文献

• E-graph - Wikipedia
• Intro to EGraphs | Google Colab
• Equality saturation a new approach to optimization (2009)
  • 提案論文, 80pp, 🤮
• egg: Rust実装
  • Fast and Extensible Equality Saturation with egg | SIGPLAN Blog
    • https://dl.acm.org/doi/pdf/10.1145/3434304
• Rewrite Rule Inference Using Equality Saturation
• TENSAT
  • egg で TASO 再実装
• Metatheory.jl: Julia実装