Lambda MicroEgg

It’s an egraph that supports well-scoped alpha aware binders. Everything old is new again. I made a tool that attaches my lifting e-graph ideas arxiv youtube to an s-expression based frontend. repo https://github.com/philzook58/lambda-microegg wasm demo https://www.philipzucker.com/lambda-microegg/ . The oooooold playbook. It’s heavily based around Max’s microegg https://pavpanchekha.com/blog/microegg.html . But I added built in binders, higher order miller patterns, and capture avoiding substitution in right hand sides. Here is using the binders for some $\sum$ rewrite rules. @ marks sum as a unary binding form. {?a x} is Miller pattern notation. More on that below. %%file /tmp/sum.sexp (insert (@sum x (@sum y (* 2 y)))) (rewrite (@sum x (* ?a {?b x})) (* ?a (@sum x {?b x}))) ; constant factoring (rewrite (@sum x ?a) (* ?a N)) ; constant sum (rewrite (* ?a ?b) (* ?b ?a)) ; mul commutativity (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 Here is an AC-10 saturation run. This is a reasonable no thinking way to kind of know perf you’re in the ball park of. On my computer, egg is ~0.6s for a similar thing, so we’re slower but not extremely so. Since liftings are stored as a byte stolen from the u32 Id, there hopefully isn’t really much overhead associated with them, especially if not used. %%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 There is a tension between the typical first order notion of application FOApp(Symbol, Vec<Id>) and the higher order binary version HOApp(Id,Id). The latter can be encoded into the former using a ubiquitout “app” symbol (app (app f x) y). This is burdensome to write though, so I added a different constructor and notation [] which automatically curries and uses HOApp. %%file /tmp/comp.sexp (insert [map [comp f g] [cons 3 nil]]) (rewrite [[comp ?f ?g] ?x] [?f [?g ?x]]) ; comp definition ; (rewrite [map ?f [map ?g ?x]] [map [comp ?f ?g] ?x]) ; map fusion (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 If I switch out in an AC saturation example the first order () for the higher order [] there is a cost to it. But, perhaps with some optimizations (like precomputing ground ids in the pattern) this could be improved. %%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 Superposition provers like e-prover and zipperposition have received special smarts for this lambda free higher order fragment https://inria.hal.science/hal-03485227/document. It’s a useful but simple thing. Or a simple but useful thing? Miller Patterns But in addition to this, it is really nice to support actual binders. The variation of higher order patterns supported is Miller patterns. A Miller pattern {?a x y} is basically a bound variable allowance pattern. Another way of saying it it Miller patterns are higher order patterns where the metavariable must be applied to distinct bound variables, not arbitrary terms. The pattern ?a is allowed to contain the bound variables x and y, but not z (if there happens to be a bound z in the pattern). It is allowed to contain any free variables in scope at the top of the pattern, which is kind of interesting. Miller patterns are basically the minimal way of making sense of patterns in a scoped syntax. There is some extra stuff you can do, but by and large it is decidable oasis in higher order matching / unification problems. Some more description of the concept: https://www.philipzucker.com/ho_unify/ https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/proghol/extract.html Chapter 4 https://en.wikipedia.org/wiki/Unification_(computer_science)#Higher-order_unification https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/jlc91.pdf Is this the original reference on Miller patterns? If you want to model beta substitution on an object @lam term, this is actually the following rule: %%file /tmp/beta.sexp (insert [(@lam x x) 42]) (rewrite [(@lam x {?body x}) ?e] {?body ?e}) ; beta substitution. Matches app(lam,e) basically. (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 What I think the thing I’ve actually added is the ability of pattern variables to have more context lying around than the base context. This first example returns a substitution in a context of size 1. ?b is the free variable in that context %%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} However in this very similar example, the context the substitution is in is context 0 (the empty context). ?b refers to an extra bound variable. This is kind of, sort of a lambda, but it’s a meta lambda. %%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} I debated to myself about whether to suppress ctx0 |-> annotations. I ended up doing so because they are noisy, but it was an important conceptual realization to me that ctx0 |-> is conceptually prior to “context-less” terms / “context-less” terms are not a thing, merely a shorthand for ctx0. Constants are “merely” 0-arity functions. I’m used to this idea that the term a is actually shorthand for a(). This really is the same observation but instead applied to the semantics of judgements [[t]] is actually [[{} |- t]]. Also check it out. Alpha equivalent terms hash cons to the same thing. The l_10 annotations are the lifting annotations, which are held in a byte stolen from the u32 Id. The <- lines are listing the enodes in the eclass. Liftings in the union find appear as liftings on the eid l_01(eclass) <- enode somewhat counterintuitively. That is the place they must appear to be conceptually/semantically correct. The enode always points to an eclass lifted from an equal or smaller context. %%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) Kind of more interesting (in it’s unusualness) is there is memory sharing between terms that are not alpha equivalent but are heavily thinning related. All of the the deeper terms in these (@lam z (@lam w (@lam v x))) and (@lam z (@lam w (@lam v y))) actually hash cons to the same form, whereas a naive de bruijn index approach would not (they’d be (lam (lam (lam var4)))) and (lam (lam (lam var3))))). Kind of you only pay hash cons memory for variables actually in use, not for the ones in scope. %%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))