AI・機械学習

Lambda MicroEgg

52 pointsby philzook2026年9月21日5 コメント

要約

Lambda MicroEggは、スコープ付きのアルファ対応バインダーをサポートするegraph実装です。Max's microeggをベースに、組み込みバインダー、高階ミラーパターン、キャプチャ回避置換などの機能が追加されています。これにより、ラムダ計算や代数的書き換えルールの表現と実行が容易になります。

全文翻訳

Lambda MicroEgg

これは、スコープを意識したアルファ（変数名）を考慮するバインダーをサポートするegraphです。

古いものはすべて新しくなります。

私のリフティングe-graphのアイデアarxiv youtubeをs式ベースのフロントエンドにアタッチするツールを作成しました。

リポジトリ https://github.com/philzook58/lambda-microegg
wasmデモ https://www.philipzucker.com/lambda-microegg/ 。非常に古いやり方です。

これはMaxのmicroegg https://pavpanchekha.com/blog/microegg.html を強くベースにしていますが、組み込みのバインダー、高階ミラーパターン、および右辺でのキャプチャ回避置換を追加しました。

以下は、バインダーを使用していくつかの$\sum$（シグマ）書き換えルールを使用する例です。@はsumを単項バインディングフォームとしてマークします。{?a x}はミラーパターン表記です。詳細は後述します。

%%file /tmp/sum.sexp

(insert (@sum x (@sum y (* 2 y))))
(rewrite (@sum x (* ?a {?b x})) 
         (* ?a (@sum x {?b x})))  ; 定数因数分解
(rewrite (@sum x ?a) (* ?a N))    ; 定数和
(rewrite (* ?a ?b) (* ?b ?a))     ; 乗法の可換性
(run 10)
(guard (@sum x (@sum y (* 2 y)))  (* 2 (* N (@sum x x))))

Overwriting /tmp/sum.sexp

! lambda-microegg /tmp/sum.sexp

; inserted e4
; rewrite 1 added
; rewrite 2 added
; rewrite 3 added
; ran 5 rounds, 17 unions: 9 classes, 22 e-nodes
; match 21.72µs, apply 14.991µs, rebuild 19.347µs
; guard passed

これはAC-10飽和実行の例です。これは、パフォーマンスがどの程度かを知るための、あまり考えずに実行できる合理的な方法です。私のコンピュータでは、eggで同様の処理を行うのに約0.6秒かかるため、それより遅いですが、極端に遅いわけではありません。

リフティングはu32 IDから1バイトを盗んでバイトとして格納されるため、特に使用されない場合は、それに伴うオーバーヘッドはほとんどないはずです。

%%file /tmp/basic.sexp

(insert (+ 1 (+ 2 (+ 3 (+ 4 (+ 5 (+ 6 (+ 7 (+ 8 (+ 9 10))))))))))
(rewrite (+ ?a ?b) (+ ?b ?a))
(rewrite (+ ?a (+ ?b ?c)) (+ (+ ?a ?b) ?c))
;(rewrite (+ (+ ?a ?b) ?c) (+ ?a (+ ?b ?c)))
(run 100)

Overwriting /tmp/basic.sexp

! lambda-microegg /tmp/basic.sexp

; inserted e18
; rewrite 1 added
; rewrite 2 added
; ran 9 rounds, 262291 unions: 1023 classes, 57012 e-nodes
; match 350.089112ms, apply 999.980826ms, rebuild 152.433662ms

Lambda Free Higher Order Application

典型的な一階の適用 FOApp(Symbol, Vec<Id>) と高階の二項版 HOApp(Id,Id) の間には緊張関係があります。後者は、遍在する「app」シンボル (app (app f x) y) を使用して前者にエンコードできます。しかし、これは書くのが面倒なので、別のコンストラクタと表記 [] を追加しました。これは自動的にカリー化され、HOApp を使用します。

%%file /tmp/comp.sexp

(insert [map [comp f g] [cons 3 nil]])

(rewrite [[comp ?f ?g] ?x] [?f [?g ?x]])                      ; compの定義
; (rewrite [map ?f [map ?g ?x]] [map [comp ?f ?g] ?x])          ; mapの融合
(rewrite [map ?f [cons ?x ?xs]] [cons [?f ?x] [map ?f ?xs]])  ; map cons
(rewrite [map ?f nil] nil)                                      ; map nil
(run 3)
(guard [[comp f g] 3] [f [g 3]])

Overwriting /tmp/comp.sexp

! lambda-microegg /tmp/comp.sexp

; inserted e12
; rewrite 1 added
; rewrite 2 added
; rewrite 3 added
; ran 2 rounds, 4 unions: 16 classes, 19 e-nodes
; match 28.954µs, apply 8.015µs, rebuild 19.358µs
; guard passed

AC飽和例で一階の () を高階の [] に切り替えると、コストがかかります。しかし、おそらくいくつかの最適化（パターンでのグラウンドIDの事前計算など）により、これは改善される可能性があります。

%%file /tmp/ho_ac.sexp

(insert [+ 1 [+ 2 [+ 3 [+ 4 [+ 5 [+ 6 [+ 7 [+ 8 [+ 9 10]]]]]]]]]) 
(rewrite [+ ?a ?b] [+ ?b ?a])
(rewrite [+ ?a [+ ?b ?c]] [+ [+ ?a ?b] ?c])
;(rewrite [+ [+ ?a ?b] ?c] [+ ?a [+ ?b ?c]]) 
(run 100)

Overwriting /tmp/ho_ac.sexp

! lambda-microegg /tmp/ho_ac.sexp

; inserted e28
; rewrite 1 added
; rewrite 2 added
; ran 9 rounds, 262143 unions: 2046 classes, 58035 e-nodes
; match 685.163722ms, apply 1.287551403s, rebuild 150.952363ms

e-proverやzipperpositionのような超位証明器は、このラムダフリー高階フラグメントに対して特別なスマートさを備えていますhttps://inria.hal.science/hal-03485227/document。有用ですが単純なものです。あるいは、単純ですが有用なものですか？

Miller Patterns

しかし、これに加えて、実際のバインダーをサポートすることは非常に便利です。

サポートされている高階パターンのバリエーションはミラーパターンです。

A Miller pattern {?a x y} は基本的に、バウンド変数の許可パターンです。

別の言い方をすれば、ミラーパターンは、メタ変数が任意の項ではなく、区別されたバウンド変数に適用されなければならない高階パターンです。

パターン ?a は、バウンド変数 x と y を含めることができますが、z（パターンにバウンドされた z が存在する場合）は含めることができません。

これは、パターンの先頭でスコープ内にある任意の自由変数を（興味深いことに）含めることができます。

ミラーパターンは、スコープ付き構文でのパターンを意味のあるものにするための最小限の方法です。追加でできることもありますが、概して高階マッチング/単一化問題における決定可能なオアシスです。

概念のさらなる説明:

https://www.philipzucker.com/ho_unify/
https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/proghol/extract.html 第4章
https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification
https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jlc91.pdf これはミラーパターンの元の参照ですか？

オブジェクト @lam 項のベータ置換をモデル化したい場合、実際には次のルールになります。

%%file /tmp/beta.sexp

(insert [(@lam x x) 42])
(rewrite  [(@lam x {?body x}) ?e] {?body ?e}) ; ベータ置換。app(lam,e)にマッチします。
(run 10)
(extract [(@lam x x) 42])

Overwriting /tmp/beta.sexp

! lambda-microegg /tmp/beta.sexp

; inserted e3
; rewrite 1 added
; ran 1 rounds, 1 unions: 3 classes, 4 e-nodes
; match 6.092µs, apply 4.989µs, rebuild 5.892µs
42

私が実際に追加したと思われるのは、パターン変数にベースコンテキストよりも多くのコンテキストを保持できる機能です。

この最初の例は、サイズ1のコンテキストでの置換を返します。?b はそのコンテキスト内の自由変数です。

%%file /tmp/ctx.sexp

(insert (@lam x (@lam y (+ 3 y))))
(match (+ ?a ?b))

Overwriting /tmp/ctx.sexp

! lambda-microegg /tmp/ctx.sexp

; inserted e4
; match 1: ctx1 |-> {?a = 3, ?b = $0}

しかし、この非常に似た例では、置換が存在するコンテキストはコンテキスト0（空のコンテキスト）です。?b は追加のバウンド変数を参照します。これはある種、ラムダですが、メタラムダです。

%%file /tmp/ctx2.sexp

(insert (@lam x (@lam y (+ 3 y))))
(match (@lam y (+ ?a {?b y})))

Overwriting /tmp/ctx2.sexp

! lambda-microegg /tmp/ctx2.sexp

; inserted e4
; match 1: {?a = 3, ?b = ctx1 |-> $0}

ctx0 |-> アノテーションを抑制するかどうかを自問自答しました。ノイズが多いので抑制しましたが、ctx0 |-> が概念的に「コンテキストレス」な項よりも優先されること、あるいは「コンテキストレス」な項は単なる ctx0 の省略形であるということが、私にとって重要な概念的認識でした。定数は「単に」0項関数です。項 a が実際には a() の省略形であるという考えに慣れています。これは実際には同じ観察ですが、ここでは判断 [[t]] が実際には [[{} |- t]] であるという意味論に適用されます。

また、これを見てください。アルファ等価な項は同じものにハッシュコンされます。l_10 アノテーションはリフティングアノテーションで、u32 IDから盗まれたバイトに格納されています。<- の行はeクラス内のenodeをリストしています。Union-Find内のリフティングは、リフティングがenodeに現れる l_01(eclass) <- enode のように、やや直感に反します。概念的/意味論的に正しい場所であるためには、そこに出現する必要があります。

%%file /tmp/alpha.egg
(insert (@lam x (@lam y (+ x y))))
(insert (@lam a (@lam b (+ a b))))
(print-egraph)

Writing /tmp/alpha.egg

! lambda-microegg /tmp/alpha.egg

; inserted e3
; inserted e3
; egraph: 4 classes, 4 e-nodes
; e0 = ctx1 |-> $0
;   e0 <- var
; e1 = ctx2 |-> (+ $0 $1)
;   e1 <- (+ l_10(e0) l_01(e0))
; e2 = ctx1 |-> (@lam x0 (+ $0 x0))
;   e2 <- (@lam e1)
; e3 = ctx0 |-> (@lam x0 (@lam x1 (+ x0 x1)))
;   e3 <- (@lam e2)

より興味深い（その珍しさにおいて）のは、アルファ等価ではないが、非常に薄い（thinning）関連を持つ項の間でメモリ共有があることです。(@lam z (@lam w (@lam v x))) と (@lam z (@lam w (@lam v y))) のこれらの深い項のすべては、実際には同じ形式にハッシュコンされますが、ナイーブなド・ブラウンインデックスアプローチではそうはなりません（それらは (lam (lam (lam var4)))) と (lam (lam (lam var3)))) になるでしょう）。スコープ内の変数の数ではなく、実際に使用されている変数のハッシュコンメモリのみを支払うようなものです。

%%file /tmp/thin.sexp
(insert (@lam x (@lam y (@lam z (@lam w (@lam v x))))))
(insert (@lam x (@lam y (@lam z (@lam w (@lam v y))))))
(print-egraph)

Writing /tmp/thin.sexp

! lambda-microegg /tmp/thin.sexp

; inserted e5
; inserted e7
; egraph: 8 classes, 8 e-nodes
; e0 = ctx1 |-> $0
;   e0 <- var
; e1 = ctx1 |-> (@lam x0 $0)
;   e1 <- (@lam l_10(e0))
; e2 = ctx1 |-> (@lam x0 (@lam x1 $0))
;   e2 <- (@lam l_10(e1))
; e3 = ctx1 |-> (@lam x0 (@lam x1 (@lam x2 $0)))
;   e3 <- (@lam l_10(e2))
; e4 = ctx1 |-> (@lam x0 (@lam x1 (@lam x2 (@lam x3 $0))))
;   e4 <- (@lam l_10(e3))
; e5 = ctx0 |-> (@lam x0 (@lam x1 (@lam x2 (@lam x3 (@lam x4 x0)))))
;   e5 <- (@lam e4)
; e6 = ctx0 |-> (@lam x0 (@lam x1 (@lam x2 (@lam x3 x0))))
;   e6 <- (@lam e3)
; e7 = ctx0 |-> (@lam x0 (@lam x1 (@lam x2 (@lam x3 (@lam x4 x1)))))
;   e7 <- (@lam l_0(e6))

興味深いニュアンスは、私が「順序付きミラーパターン」しかサポートできないことです。これは、非線形パターン、つまり変数が2回使用される場合にのみ顕著になります。パターンでの項作成を許可するか、シンニングを交換もサポートするように拡張することでこれをサポートできます。これにより、スロットに非常に近づきますが、微妙に異なると思います。なぜなら、スコープが異なって処理され、変数が順序付けられるからです。これにより、グループ対称性破壊の作業を実装する必要がなくなると思いますか？「同じもの」と見なすものの主観的な選択によっては、スロットとリフティングは同じものです。スロットは名前とアルファ置換/名前変更を強調するように見えますが、シンニングはスコープ/弱化を強調します。おそらく、違いを見ることに利害関係があるのかもしれません。

%%file /tmp/nogood.sexp

(rewrite (@lam x (@lam y (pair {?a x y} {?a y x}))) wontwork)

Overwriting /tmp/nogood.sexp

! lambda-microegg /tmp/nogood.sexp

/tmp/nogood.sexp:2:41: error: Miller metavariable '?a' arguments are out of order; write {?a x y} on the match left-hand side, then permute its arguments on the rewrite right-hand side if needed

Bits and Bobbles

これがまとまるのを見て、とても興奮しています。https://www.philipzucker.com/egraph-ground-rewrite/ しばらくラムダをそこに入れることを模索していました。

項作成をパターンに「バンドエイドを剥がす」だけで、より高度なパターンをサポートできます。パターン変数がグラウンド化されると、それを使用して、より複雑なベータ置換を含む他の使用箇所をグラウンド化できます。

おそらく、異なる概念のために異なるブレースを使用するのは奇妙です。FOAppを削除する方が良いかもしれません。たとえパフォーマンスのヒットがあったとしてもです。

マップコンプ融合の例が爆発する可能性があることに少し驚きました。e-graphはダメなのかもしれません。

使用していないときはほとんどコストをかけずに、7つ以上の変数をサポートしたいと思っています。現在、「一時的なenode」のアイデアに傾いています。また、ブッフバーガー、多重集合、文字列、半環の完了をこのものに注入してみたいです。

次に証明を行いたいと思います。Leanの慣習に従って、証明項を出力するためにトラバースする証明ログバージョンを試したいと思います。

パターンをフラット化し、動的に上、下、または横に依存して移動しますか？

egglogがGAT向けに設計されていた場合、これはSOGATにも良いですか？

これらすべては何のためか？

関係計算統合ルールプログラムインタプリタ型チェッカー固定点推論全称量化子存在量化子推論計算モード。冗長なルールの証明。

はい、すべてのアルファ等価な項は同じメモリにハッシュコンされます。

まあまあ。自由変数は暗黙の順序を持っています。アルファ等価な閉じた項と、同じ順序で自由変数を使用する項はハッシュコンされますが、$0 + $1 と $1 + $0 は同じようにハッシュコンされません。しかし、$0 + $2 と $0 + $1 は、シンニングアノテーションを使用していても、同じインターン化メモリにハッシュコンされます（編集済み） $n は自由変数 n を表します。$0 + $2 と $0 + $1 は、同じインターン化メモリを使用しているにもかかわらず、識別子のシンニングアノテーション（u32 IDからバイトを盗みました）により、観察可能に異なります。したがって、現在の実装では最大7つの自由変数が許可されます。最初のオーダーのコストをゼロに近づけようとしていました（編集済み）。

バウンド変数にも順序があります。自由変数とバウンド変数はすべて同じものです。しかし、順序はド・ブラウンインデックスやレベルのように、バインダーの順序によって定義されるため、バインダーサイトと使用サイトの両方でのアルファ名前変更は実際には何も影響しません（編集済み）。自由変数をアルファ名前変更した場合、対応するバインディングサイトの名前変更にはならないのでしょうか？順序なしコンテキストのセットのような性質が感染しています [x, y] |- x + y は [a,b] |- a + b と同じですが、[b,a] |- a + b とは同じではありません。名前は呪われています。そしてアルファ名前変更も呪われています。それはかなり悪い非意味論的な概念です。

どうかな、マン。

和の恒等式におけるシフトルールは興味深いようです。

バイナリAppを使用すべきか？

Maxが言ったように、左辺での項作成を許可すべきか？

常に多くのパターン前処理を行う誘惑があります。

大幅にマイクロ最適化していませんが、簡単な勝利を収め、無駄な割り当てをいくつか回避しました。無意味なマイクロベンチマークでは、eggの約3倍のパフォーマンスです。10倍未満なら問題ないと言えます。

右辺で使用できる組み込みのキャプチャ回避置換ルーチンがあります。これはe-graphを再帰的にコピーするか、別の意味では、多くの項を抽出し、置換してから再挿入することと同等です。各ポイントでのリフティング技術は、項を最小限必要なコンテキストに強化します。このため、どのeクラスから展開しても、どの変数が検出されるかを常に正確に把握できます。これは、ベータ置換を早期に終了できるブールグラウンドフラグの一般化のようなものです。

現在、シンニングのためにu32 IDから1バイトを盗んで「Fat ID」を作成しています。IDは実際にはそれほど太くなっていません。AIが素敵なエンコーディングトリックを作成しました。センチネル1がシンニングビットベクターの開始位置を示します（つまり、[false, true, true] = 0b00001011）。これにより、コンテキストで最大7つの変数をサポートできます。幅が任意のシンニングをどのように最適にサポートするかについては、まだ検討中です。Fat IDを64ビットにするために、シンニングを別のu32にするかもしれません。あるいは、「一時的なenode」の方向に向かい、シンニングが7より大きい場合は、非常にFat IDを格納する別のアリーナを作成するかもしれません。

私はソートレス時代に戻っているような気がします。型を避けることは解放感があります。Prologはそうしませんし、egglog0もしませんでした。なぜすべての宣言や余分なジャンクを書かなければならないのでしょうか？

AIを大幅に使用しました。過去数週間から数年、AIが私の大切にしてきたすべて、または自分自身に投資してきたすべてにとって何を意味するのかについて、かなり落ち込んでストレスを感じています。サイコシスを引き起こすだけなので、ソーシャルメディア、フォーラム、ニュースサイトから徐々に離れています。

プラス面（？）では、いくつかのことが実際に起こるのを見て楽しかったです。私にはプログラミングスキル以上のアイデアがたくさんあります。

マイナス面では、コード全体を数回レビューした後でも、まだ少し「緩い」ように見えます。インデックス操作の数学の詳細をチェックしようとはしませんでした。テストに基づくと、おそらく正しいと思います。AIは、そのようなローカルな作業では私よりも優れているようです。

自分でこれを書くという方向には乗っていなかったと思います。作業量が積み重なり、Rustは得意ですが、決して器用ではありません。パーサーを書くのは面白くなく苦痛なので、フロントエンドを書く傾向がありません。バインダーを持つ意味のあるパターンをどのように表現するかについてのアイデアを練り出すことが、私にとって最も新しく最も興味深い部分だと思います。

%%file /tmp/integ.sexp

(rewrite (@int x 1) $0)

書き換えの左辺と右辺が異なるコンテキストにあるのは無意味だと思います。右辺に?aを挿入するには、抽象化した追加の穴をどのように埋めるかを知る必要があります。スコープ内の任意のものをそれに使用できます。右辺に(lam x (lam y (?a x y )))を再度挿入したとしても、それはある意味ではノードップではありません。なぜなら、左辺と右辺のバウンド変数は、ある意味では同じであり、ある意味ではそうではないからです。実装上はノードップです。

私のトークではバインダーの扱いについてあまり触れませんでした。興味深い教訓だったと思うのは、バインダーは本質的なポイントではなく、バインダーについて話し始める前に明確にすべきことがたくさんあるということです。本質的なポイントは、コンテキストが項の一部であること（または変数を含む項の意味を理解するために必要であること [[ctx |- t]]）でした。次に、構築するのに役立つスマートな操作は、コンテキストの操作（弱化や交換など）です。リフティング/シンニングはその方法の1つです。

当初はすべての内部構造を構文レベルで公開していましたが、私もかなり混乱していました。名前は良いです。しかしそれにもかかわらず、人々（そして私も）見慣れたものを望むので、以前見たラムダマッチングデザイン（ラムダプロログなど）に近く留まるのは理にかなっています。私自身もリフティングを参照するパターンを書きたいとはあまり思っていません。

バインダーの紛らわしい点は、パターン内に複数のコンテキストを同時に使用することです。パターンのいくつかの位置は、他の部分とは異なる変数コンテキストにあり、これらの異なるコンテキスト間をどのように移動させたいかを指定する必要があります。a priori v7 がコンテキストAで、コンテキストBの v7 と同じではない可能性があるという感覚があります。なぜなら、項をAからBにトラバース中に、変数をシフト、挿入、削除、スワップする可能性があるからです。

パターンは、コンテキスト n |-> e42 での項に対してマッチングが試行されます。パターンの先頭はそのコンテキスト n にありますが、パターン内部では、より多くの変数が関与する可能性があります。

パターン (map (lam x ?b) ?l) が 7 |-> e4 に対してマッチングする場合、パターンの先頭はコンテキスト7にあり、?l もコンテキスト7にありますが、?b はコンテキスト8にあります。

右辺に持ち越したい置換を考える場合、lhs -> rhs、置換はパターンのトップコンテキストにあるべきです。[?l = n |-> e14, ?b = n+1 |-> e18] あるいは、n |-> [?l = +0 |-> e14, ?b = +1 |-> e18] と考える方が良いでしょうか？

?b をラムダとして考えることはあまりしたくありません。それは単にコンテキスト内の項ですが、コンテキストはその特定の場所で分割されていることが示されていると考える方が適切だと思います。

[[n |-> ]]

リフティングの視点は、新しい変数を現在の変数の先頭または末尾に入れることを主張するのではなく、コンテキストに持ち込むためのより豊かな方法を可能にしますが、これを公開することが有用な例は知りません。

明示的なシンニングパターンを持つことができます。また、変数禁止アノテーションや変数許可アノテーションを持つこともできます。

ミラーパターン (?a x y) は基本的に変数許可パターンです。すべての自由変数を許可し、実際、ルール内で自由変数に言及すべきではないでしょう。そうすることは、現在配線されていても、スコープの観点からは少し怪しいです。

メタ数学やメタ数学ゼロでも同様のものが現れることに注意します。おそらく名目上の # 制約でも同様です。

ミラーパターンに追加した異常な制限は、変数がバインドされた順序と同じ順序でパターンで適用される必要があることです。(lam x (lam y (?a x y))) はOKですが、(lam x (lam y (?a y x))) はそうではありません。実装の観点からは、この制限により複雑さが大幅に軽減され、右辺で使用する際に引数を入れ替えるだけで済むため、多くの力を失うことはありません。

この制限が真に力の損失となる可能性のある場所の1つは、非線形パターン、例えば (foo (lam x (lam y (?a x y))) (lam x (lam y (?a y x)))) のような場合です。この問題を解決する1つの方法は、Maxが提案しているように、パターンでの項作成を有効にすることです。おそらくそれが正しい方向でしょう。