Sketch-Guided Equality Saturation

paper

2022-11-14

@article{koehler2021sketch,
  title={Sketch-Guided Equality Saturation: Scaling Equality Saturation to Complex Optimizations in Languages with Bindings},
  author={Koehler, Thomas and Trinder, Phil and Steuwer, Michel},
  journal={arXiv preprint arXiv:2111.13040},
  year={2021},
  url={https://arxiv.org/pdf/2111.13040.pdf}
}

repo: GitHub - Bastacyclop/egg-rise: Exprimenting with egg (https://github.com/egraphs-good/egg) for Rise (https://github.com/rise-lang)

• Simply Typed Lambda Calculus を Equality Saturation で扱いたい
• 巨大な書き換え列で E-Graphはすぐに巨大になる

Introduction

• LIFT
• 最適化パスは大量にあると困難
  • Phase ordering problem
  • Equality Saturation が解決
• しかし, 複雑な最適化には対応してない
  • 可換性や結合性などの規則で急速に巨大化する
• Lambda Calculus Encoding
  • 変数, 束縛を効率的に行う方法について議論する
    • t タイムリー, ちょうど困っていた
    • ナイーブなλ計算のencodingは非効率的 Equality Saturation for Tensor Graph Superoptimization
• 束縛は De Bruijn index で $\alpha$-equivalentな項にすることでE-Graphの巨大化を回避
• 置換の近似として中間置換ステップを実装することで回避

Motivation and Background

• term ameliorate: 改善する
• E-graph の説明

3. Sketch-guided Equality Saturation

• term suffice 十分
• 例えば, 行列積のブロック化は膨大な規則を用いなければいけないが, sketchなら2つで十分

• SKETCH BASIC
  • S ::=
    • ? | 最小の
    • F(S, ...) | contains(S) | S || S
• Sketch $s$ は項の集合 $R(s)$ を表す