Lambda MicroEgg

これは、スコープ付きのアルファ対応バインダーをサポートするegraphです。すべてが新しくなります。私は、s式ベースのフロントエンドに私のリフティングegraphのアイデア（arxiv youtube）をアタッチするツールを作成しました。リポジトリはhttps://github.com/philzook58/lambda-microegg、wasmデモはhttps://www.philipzucker.com/lambda-microegg/です。非常に古いプレイブックです。Max's microegg（https://pavpanchekha.com/blog/microegg.html）に大きく基づいています。しかし、組み込みバインダー、高階ミラーパターン、および右辺のキャプチャ回避置換を追加しました。ここでは、バインダーを使用していくつかのΣ書き換えルールを示します。@は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)))) /tmp/sum.sexp を上書きします ! lambda-microegg /tmp/sum.sexp ; e4 を挿入しました ; rewrite 1 を追加しました ; rewrite 2 を追加しました ; rewrite 3 を追加しました ; 5ラウンド実行、17ユニオン：9クラス、22 eノード ; マッチ 21.72µs、適用 14.991µs、再構築 19.347µs ; ガードパスしました これはAC-10飽和実行です。これは、パフォーマンスがどの程度かを知るための、思考を必要としない合理的な方法です。私のコンピューターでは、eggは約0.6秒で同様のことを行うため、遅いですが極端ではありません。リフティングはu32 Idからバイトを盗んで格納されるため、特に使用されない場合は、実際にはほとんどオーバーヘッドがないはずです。 %%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) /tmp/basic.sexp を上書きします ! lambda-microegg /tmp/basic.sexp ; e18 を挿入しました ; rewrite 1 を追加しました ; rewrite 2 を追加しました ; 9ラウンド実行、262291ユニオン：1023クラス、57012 eノード ; マッチ 350.089112ms、適用 999.980826ms、再構築 152.433662ms ラムダフリー高階適用 典型的な一階の適用 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]]) /tmp/comp.sexp を上書きします ! lambda-microegg /tmp/comp.sexp ; e12 を挿入しました ; rewrite 1 を追加しました ; rewrite 2 を追加しました ; rewrite 3 を追加しました ; 2ラウンド実行、4ユニオン：16クラス、19 eノード ; マッチ 28.954µs、適用 8.015µs、再構築 19.358µs ; ガードパスしました 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) /tmp/ho_ac.sexp を上書きします ! lambda-microegg /tmp/ho_ac.sexp ; e28 を挿入しました ; rewrite 1 を追加しました ; rewrite 2 を追加しました ; 9ラウンド実行、262143ユニオン：2046クラス、58035 eノード ; マッチ 685.163722ms、適用 1.287551403s、再構築 150.952363ms e-proverやzipperpositionのような超位証明器は、このラムダフリー高階フラグメント（https://inria.hal.science/hal-03485227/document）のために特別なスマートさを受け取っています。それは有用ですが単純なものです。あるいは単純だが有用なもの？ ミラーパターン しかし、それに加えて、実際のバインダーをサポートすることは非常に良いことです。サポートされている高階パターンのバリエーションはミラーパターンです。ミラーパターン {?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]) /tmp/beta.sexp を上書きします ! lambda-microegg /tmp/beta.sexp ; e3 を挿入しました ; rewrite 1 を追加しました ; 1ラウンド実行、1ユニオン：3クラス、4 eノード ; マッチ 6.092µs、適用 4.989µs、再構築 5.892µs 42 私が実際に追加したと思うのは、パターン変数がベースコンテキストよりも多くのコンテキストを保持できる能力です。この最初の例は、サイズ1のコンテキストでの置換を返します。?bはそのコンテキスト内の自由変数です。 %%file /tmp/ctx.sexp (insert (@lam x (@lam y (+ 3 y)))) (match (+ ?a ?b)) /tmp/ctx.sexp を上書きします ! lambda-microegg /tmp/ctx.sexp ; e4 を挿入しました ; マッチ 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}))) /tmp/ctx2.sexp を上書きします ! lambda-microegg /tmp/ctx2.sexp ; e4 を挿入しました ; マッチ 1: {?a = 3, ?b = ctx1 |-> $0} ctx0 |-> アノテーションを抑制するかどうかを自問自答しました。ノイズが多いので最終的に抑制しましたが、ctx0 |-> が概念的に「コンテキストレス」項よりも先行する、あるいは「コンテキストレス」項は単なる省略形であるという重要な概念的認識でした。定数は「単に」0項関数です。項aは実際にはa()の省略形であるという考えに慣れています。これは実際には同じ観察ですが、代わりに判断のセマンティクスに適用されます [[t]] は実際には [[{} |- t]] です。 アルファ等価な項は同じものにハッシュコンされます。l_10アノテーションはリフティングアノテーションであり、u32 Idから盗まれたバイトに保持されます。<- の行はeclass内のenodeをリストしています。ユニオンファインドのリフティングは、反直観的ではありますが、eid l_01(eclass) <- enodeとしてリフティングとして現れます。それは概念的/意味論的に正しい場所でなければならない場所です。enodeは常に、等しいかより小さいコンテキストからリフトされたeclassを指します。 %%file /tmp/alpha.egg (insert (@lam x (@lam y (+ x y)))) (insert (@lam a (@lam b (+ a b)))) (print-egraph) /tmp/alpha.egg を書き込みます ! lambda-microegg /tmp/alpha.egg ; e3 を挿入しました ; e3 を挿入しました ; egraph: 4クラス、4 eノード ; 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) より興味深い（その珍しさにおいて）のは、アルファ等価ではないが非常に似ている項間でメモリ共有があることです。