Lambda MicroEgg：Millerパターンと捕捉回避置換を備えた高階e-graph

e-graphは等式推論に優れるが、伝統的に一階項を扱うため、バインダを考慮した書き換えは扱いにくい。Philip ZuckerのLambda MicroEggは、Max Willseyのmicroeggをネイティブなバインダ、Millerパターン、および捕捉回避置換で拡張する。

重要なエンジニアリング上の洞察は、リフティング注釈（スコープ深度）をu32のe-class IDから1バイト借用して格納することである。これにより、アルファ等価なラムダ項が同一のe-classにハッシュコンシングされる — (@lam x (@lam y (+ x y))) と (@lam a (@lam b (+ a b))) は同じe-nodeになる — 一方、アルファ等価ではないがシンニング関連の項はより深い部分構造を共有する。

Millerパターン {?a x y} は、メタ変数の適用をスコープ内の異なる束縛変数に限定し、高階マッチングの決定可能な断片を提供する。このシステムはまた、[]記法によるラムダフリーの高階適用をサポートし、HOApp(Id,Id)へ自動カリー化することで、冗長な (app (app f x) y) エンコーディングを避ける。ベータ置換は単純な書き換え規則になる。

性能はAC飽和ベンチマークにおいてベースのeggライブラリの2〜3倍以内である（262kのunionを約1.5秒で処理、eggは約0.6秒）。リフティング用のバイトは未使用時には無視できる程度のオーバーヘッドしか追加しない。

u32のe-class IDから1バイトを借用してリフティング注釈を格納し、追加のメモリオーバーヘッドなしでアルファ等価なハッシュコンシングと捕捉回避置換を可能にした

一階e-graphではバインダのために冗長なDe Bruijnエンコーディングや明示的な置換機構が必要になる

Millerパターンは高階マッチングの決定可能で振る舞いの良い断片を与える

既存のIDから1バイトを借用することでリフティング注釈のための割り当てオーバーヘッドを避けられる

アルファ等価なハッシュコンシングがリフティング表現から自然に生じる

既存のIDから借用した1バイトでスコープ規律をエンコードでき、一階e-graphを最小限のオーバーヘッドで高階のものに変えられる。

実装はgithub.com/philzook58/lambda-microeggでオープンソース化されており、WASMデモもある。著者は証明ログ、より多くの変数のための一時的enode、およびBuchberger/マルチセット/文字列/半環完備化との統合を追加する予定である。