Lambda MicroEgg：具 Miller 模式與避免捕獲代入的 HO e-graph

E-graph 擅長等式推理，但傳統上只處理一階項，使得能感知綁定子的改寫相當彆扭。Philip Zucker 的 Lambda MicroEgg 擴展了 Max Willsey 的 microegg，加入原生綁定子、Miller 模式與避免捕獲的代入。

關鍵的工程洞見，是把提升標註（作用域深度）存放在從 u32 e-class ID 偷來的一個位元組裡。這讓 alpha 等價的 lambda 項能 hash-cons 到相同的 e-class——(@lam x (@lam y (+ x y))) 與 (@lam a (@lam b (+ a b))) 會變成同一個 e-node——而彼此非 alpha 等價、但具 thinning 關係的項則共享更深的子結構。

Miller 模式 {?a x y} 限制元變數只能套用到作用域內相異的綁定變數，提供了一個可判定的高階匹配片段。該系統也透過 [] 記法支援無 lambda 的高階應用，會自動柯里化為 HOApp(Id,Id)，避免冗長的 (app (app f x) y) 編碼。Beta 代入則變成單純的改寫規則。

在 AC 飽和基準測試上，效能落在基礎 egg 函式庫的 2 至 3 倍以內（約 1.5 秒內完成 262k 次聯集，對比 egg 約 0.6 秒），而未使用時，提升位元組帶來的額外開銷可忽略不計。

從 u32 e-class ID 偷取一個位元組來存放提升標註，實現 alpha 等價的 hash-consing 與避免捕獲的代入，且不增加額外記憶體開銷

一階 e-graph 處理綁定子時，需要冗長的 De Bruijn 編碼或明確的代入機制

Miller 模式提供了可判定、行為良好的高階匹配片段

從既有 ID 偷取一個位元組，避免了提升標註的配置開銷

alpha 等價的 hash-consing 自然從提升表示法中浮現

從既有 ID 偷來的一個位元組，就能編碼作用域紀律，以極小開銷把一階 e-graph 變成高階 e-graph。

實作以開源形式發布於 github.com/philzook58/lambda-microegg，並附有 WASM 示範。作者計畫加入證明記錄、供更多變數使用的臨時 enode，以及與 Buchberger／多重集／字串／半環 completion 的整合。