Lambda MicroEgg

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.