Rewrite Rule Inference Using Equality Saturation

CCS Concepts: Theory of computation -> Equational logic and rewriting, Software and its enginenering -> Interpreters

Abstract

• 普通はコンパイラ, プログラム合成, 定理証明は Term Rewriting に依存しているが, 有益な書き換えルールの開発は難しい.
• そこで E-Graph を用いて, Equality Saturation がどのように適用されるかを検討.
• Ruler というツールを開発した
  • 文法, インタプリタから同類項の列挙をしてルールを生成, 選択
  • 5x 小さいルールセットで25x 高速に合成.
  • 生成された書き換え規則はドメインエキスパートと同等

1. Introduction

• 書き換えシステムは各rule $\ell ⇝r$ に対して書き換えを行う

• 多くのコンパイラ, プログラム合成, 定理証明系は書き換え系に依存している

  • 頼らないと遅くて大きなコード出すので

• いくつかのドメイン特化な書き換えが開発されているが最初にルールを作る時に専門家が試行錯誤しなければならない

  • そこでドメインに依らない Equality Saturation というアプローチを提案した

• いままでのツールは

  • ドメインから項集合 $T$ を列挙
  • 候補 $T\times T$ から $C$ を選択
  • そのなかから有用な規則 $R$ をフィルタリング

2. Background

2.1 Implementing Rewrite Systems

• 書き換え規則の開発
  • ドメイン $D$ から書き換え規則 $\ell \leftrightsquigarrow r$ を構成
    • $\ell ,r$ は同一のsemanticsでなければいけない
  • そこから循環的な(ex. $(x+y)⇝(y+x)$) 規則とか拡張的なルール (ex. $x⇝(x+0)$) を
• 書き換えエンジンによる規則の適用

2.2 E-graphs

• E-Graph は定理証明系で用いられているデータ構造
  • congluenceな関係を保持するための
  • 重複を生まないように Hash consing を使用している　
  • サイクルを持てるので無限集合も表せる

2.3 Equality Saturation

• Equality Saturation は E-Graph を効率的に書き換えるためのアルゴリズム
  • Equality saturation a new approach to optimization
  • 最適化や合成のために, 与えられたコスト関数を使って最善の項 $t_b$ を決める
  • 非破壊的な書き換えが出来るのがアド
  • E-matching を使って規則の $\ell$ を見つける
    • $(\sigma ,c_{\ell })$: Subst と EClass を返す
    • 規則を適用するのは情報を付加することなので破壊されない
• どのルールでも情報がふかされなくなった時, “saturated” という
• 評価関数を使って取り出し
  • ASISize とか単純なものから遺伝的アルゴリズムを使ったもの (egg Fast and extensible equality saturation) まで

擬似コード, Pythonに寄せている, highlightingされていて好感持てる.
Parallelizing fully homomorphic encryption for a cloud environment の擬似コードと大違い

3. Ruler

4. Evaluation

• performance: 類似手法と比べた, 規則の書き換えの速さ
• compactness: どれくらい少ない規則を生成するか
• derivability: 類似手法と比べてどれくらい同じ規則を生成するか
• end-to-end: 専門家が構築したルールと比べてどれくらいいいか
• sensitivity analysis: コアアルゴリズムを変えたときにどうなるか
• validation analysis: validation strategiesを変えた時にどうなるか