Lambda MicroEggは、e-graphの考え方を拡張することを軸に設計された、小規模なS式ベースの書き換えツールです。等値グラフ、つまりe-graphは、式の多数の等価な形を同時に保持します。書き換え規則が代替形を追加し、エンジンが後から、より単純な形や別の目的に有用な形を取り出せます。ここで難しいのがスコープです。lambda式では、ある変数名が属するのは最も内側のバインダであるため、書き換えによって誤って別の正しい変数を参照させることのないようにする必要があります。
Lambda MicroEggとe-graphの冒頭の説明の後に配置され、プロジェクト自体を紹介する部分にあります。
このプロジェクトでは、バインダを一般的に表現します。`(@sum x BODY)`も`(@lam x BODY)`も、同じ内部構造である`Binder(Symbol, Id)`を使います。`lam`はlambda計算で慣用的に使われる記号にすぎません。書き換え規則の右辺では、`#subst`を通じて明示的な代入を要求することもでき、項をバインダをまたいで移動した際に自由変数が捕获される危険を減らせます。
マッチングは、計算量的に扱いやすい高階パターンであるMillerパターンに意図的に限定されています。`{?a x}`のようなパターンでは、メタ変数`?a`は束縛変数`x`を含む式本体を表せますが、`y`のような無関係な別の変数を捕获することはできません。この制約により、スコープを持つマッチングは、決定不能な問題を符号化し得る完全な高階マッチングよりも実装しやすくなります。提示されたベータ簡約の例では、`[((@lam x {?body x}) ?e)]`を`[{?body ?e}]`に書き換え、恒等関数に`42`を適用した結果から`42`を取り出します。
この実装では、項が変数コンテキスト間をどのように移動するかを追跡するため、thinning注釈も使っています。著者によると、alpha同値な項、つまり一貫した変数名の変更だけが異なる項は、同じ内部表現にhash-consされます。また、weakeningによって関係づけられる項は、より深い部分のメモリを一部共有できます。これは独立したベンチマーク結果ではなく、このプロジェクトによる設計上の主張です。
主なトレードオフは、性能と表現力のバランスです。著者のページでは、高階のsaturation実行が`egg`を使った同様の実行より遅かったこと、および一階のapplicationから高階のapplicationへ切り替えるとコストが増えたことが報告されています。Lambda MicroEggは順序付きMillerパターンに対応しているため、異なる引数の順序で同じメタ変数を使う非線形パターンは、暗黙に処理されるのではなく拒否されます。リポジトリにはコマンドラインとWebAssemblyのデモ用エントリーポイントが記載されていますが、このパッケージから、より広い採用実績、正しさの保証、または実運用環境での性能が確認できるわけではありません。