注目★★★★★Lobsters
Lambda MicroEgg、binders対応e-graphを実装
30秒で把握
- 1Lambda MicroEgg がスコープ付きalpha同値binder対応e-graphを公開
- 2Miller pattern・高階適用・capture-avoiding substitutionを実装
- 3AC-10で約58,000 e-node生成、変数は現状7個まで対応
要約
著者は、スコープ付きalpha同値binderを扱えるe-graph実装「Lambda MicroEgg」を公開した。Maxのmicroeggを基盤に、Miller pattern、capture-avoiding substitution、higher-order applicationを組み込んだ。λ計算のβ置換や総和の書き換え規則を実行でき、alpha同値な項は同じメモリにハッシュ統合する。AC-10の例では約57,000〜58,000個のe-nodeを生成し、first-order版よりhigher-order版の処理時間が増えた。現実装はthinning用にu32 IDの1バイトを使い、コンテキスト内の変数は最大7個に制限される。
あなたへの影響
定理証明器や言語処理系を開発する日本のエンジニアは、Miller patternとcapture-avoiding substitutionの設計を検証する題材として評価できる。
推奨：現実装には変数数とordered Miller patternの制限があるため、導入前に対象言語のbinder表現でテストすべき。