I've been out of the egraph world for a bit (so I admit I don't have the full context to understand this blog post), but it's cool to see the progress made toward properly supporting lambdas. Something my labmate was asking me about feels kind of like a related problem. He wanted to know how f(g(h(2)) and f(g(h(3)) would be represented and I told him that they'd be wholly different e-nodes and e-classes. I'm pretty sure I'm not wrong...
This seems like an obvious inefficiency, although I did remind him that it's only obvious when you're thinking with terms and that isn't really how things work in egraph land. But with the proper app rules couldn't your representation get something like app (f . g . h) 2 in which case sharing could then apply? Well... maybe this isn't actually too related to your blog post, but it reminded me of his question.
It's definitely related to this blog post, and also to the author's recent talk at EGRAPHS 2026, which partially solves the shared-composition issue by lifting all constants to functions.
Yes, one could represent app (f . g . h) 2 and app (f . g . h) 3 as [[[comp [comp f g] h] 2] and [[[comp [comp f g] h] 3] in the syntax of the blog post and share the f . g . h term, but these terms are not understood to be the same as [f [g [h 2]]] or [f [g [h 3]]] without a rewrite defining comp so this isn't really a savings. It feels like the intent of this example is to ask for fully built in beta egraph, which I suspect would be undesirably costly if possible (e-matching on such a thing would include full higher order matching, which is undecidable). The post is by and large about alpha/scoping with a little beta sprinkled in as built-in function treat for right hand sides of rules.
Yes, the lifting annotations can be seen as a relative of slotted. Liftings bake in less power to the e-graph than slotted, but I think it is implementation wise and semantically simpler. I think the biggest conceptual divergence is that the emphasis of liftings is on scope/context, whereas I see slotted as emphasizing names.
cole-k | a day ago
I've been out of the egraph world for a bit (so I admit I don't have the full context to understand this blog post), but it's cool to see the progress made toward properly supporting lambdas. Something my labmate was asking me about feels kind of like a related problem. He wanted to know how
f(g(h(2))andf(g(h(3))would be represented and I told him that they'd be wholly different e-nodes and e-classes. I'm pretty sure I'm not wrong...This seems like an obvious inefficiency, although I did remind him that it's only obvious when you're thinking with terms and that isn't really how things work in egraph land. But with the proper
apprules couldn't your representation get something likeapp (f . g . h) 2in which case sharing could then apply? Well... maybe this isn't actually too related to your blog post, but it reminded me of his question.Corbin | 20 hours ago
It's definitely related to this blog post, and also to the author's recent talk at EGRAPHS 2026, which partially solves the shared-composition issue by lifting all constants to functions.
[OP] philzook | 19 hours ago
Yes, one could represent
app (f . g . h) 2andapp (f . g . h) 3as[[[comp [comp f g] h] 2]and[[[comp [comp f g] h] 3]in the syntax of the blog post and share thef . g . hterm, but these terms are not understood to be the same as[f [g [h 2]]]or[f [g [h 3]]]without a rewrite definingcompso this isn't really a savings. It feels like the intent of this example is to ask for fully built in beta egraph, which I suspect would be undesirably costly if possible (e-matching on such a thing would include full higher order matching, which is undecidable). The post is by and large about alpha/scoping with a little beta sprinkled in as built-in function treat for right hand sides of rules.cole-k | 14 hours ago
Yes indeed, but like supporting reversing beta (at least from my examples as given) which seems obviously inefficient except for specific examples.
Still, having alpha equivalent terms have the same representation (which I understand slotted e-graphs also achieved?) is awesome stuff!!
[OP] philzook | 8 hours ago
Yes, the lifting annotations can be seen as a relative of slotted. Liftings bake in less power to the e-graph than slotted, but I think it is implementation wise and semantically simpler. I think the biggest conceptual divergence is that the emphasis of liftings is on scope/context, whereas I see slotted as emphasizing names.