egg Fast and extensible equality saturation

2. Background

2.1 E-graphs

項間の合同関係を保持
- Automated Theorem Provers(ATP) 定理証明系で使われている

def. E-graph

E-graph $(U, M, H)$

union-find構造 $U$ は e-class idとして等しい関係( $\equiv_{id}$ ) を保持
e-classのマップ $M$ は e-class から e-classesへの写像
- $a \equiv_{i d} b$ iff $M [a] = M [b]$
e-classはidを持つが, e-nodeはそうではない.

def. canonicalization

find(U, a) = find(U, b) iff $a \equiv_{i d} b$ となるための findを $U$ は提供する
e-class $a$ が canonical iff find(a) = a
e-node $n$ が canonical iff n = canonicalize(n)
- canonicalize(f(a_1, a_2, \cdots)) = f(find(a_1), find(a_2), \cdots)

def. representation of terms

e-graph は e-class の項を表す
e-class $c$ は e-node $n \in c$ の項を表す
e-node $f (a_{1}, a_{2}, \dots)$ は同一の関数のシンボル $f$ の項 $f (t_{1}, t_{2} \dots)$ を表し, e-class $M [a_{i}]$ は $t_{i}$ を表す

def. Equivalence

e-graphは3つの合同関係を表す

e-class idの同一性 $a \equiv_{id} b$ iff find(a) = find(b)
e-node の同一性 $n_{1} \equiv_{node} n_{2}$ iff $n_{1}, n_{2}$ が同一の e-class を持っている
項の同一性 $t_{1} \equiv_{term} t_{2}$ iff $t_{1}, t_{2}$ が同一のe-classで表される場合

def. congruence

$≅$ はe-nodeの合同関係を表す. s.t $f (a_{1}, a_{2}, \dots) ≅ f (b_{1}, b_{2}, c \dots)$ iff $a_{i} \equiv_{id} b_{i}$

2.1.3 Interface and Rewriting

E-graphは2つの操作を提供

add(n: e-node)
- if lookup(n) = a
  - return a
- else
  - M[a] = {n}, return id of a

2.2 Equality Saturation

todo

3. Rebuilding

4. E-class analyses

4.1 E-class Analyses

domain $D$ , 各 e-class $c$ に紐付く値 $d_{c} \in D$

$make (n) \to d_{c}$
- 新しい e-node $n$ が $G$ に追加され, e-classに $c$ が作成され, $c$ に紐付くデータ $d_{c} \in D$ を作成
$join (d_{c_{1}}, d_{c_{2}}) \to d_{c}$
- e-class $c_{1}, c_{2}$ が $c$ にmergeされるとき, $d_{c_{1}}, d_{c_{2}}$ から $d_{c}$ を作成する
$modify (c) \to c^{'}$
- e-class $c$ に e-node が追加されたときなど $c$ が変更された時の処理, 冪等性 modify(modify(c)) = modify(c) を持つべき
join semilattice になる

^{\forall} c \in G, d_{c} = n \in c ⋀ make (n) and modify (c) = c

6. Case Studies

6.1 Herbie: Improving Floating Point Accuracy

6.2 Spores

SPORES

6.3 Szalinski

Synthesizing structured CAD models with equality saturation and inverse transformations

Quartz 5

Explorer