How to deal with alpha-equivalence?

[silversquirl]

I'm trying to apply egg to optimization of lambda calculus terms, but it's proving rather difficult because e-graphs don't have any concept of alpha-equivalence. If I add a rule that can generate fresh variables, it ends up generating hundreds of equivalent terms that all have to be stored in the e-graph because they use different names.

I've heard some mentions of using de Bruijn indexing to work around this problem but I'm not sure how to write rules for this nicely - anything that removes an abstraction would require rewriting the entire nested tree to adjust all the indices, which gets quite annoying quite quickly.

Any suggestions on how to handle this problem?

[goens]

There's a preprint by @Bastacyclop where they address that issue with some ideas for mitigation. It doesn't sound like it from the title, but it's exactly what they discuss in 4.1: https://arxiv.org/abs/2111.13040

[mwillsey]

@goens is correct that this is a good way to address this, but it's also worth noting that you've come across one of the major challenges when working with e-graphs: poor support for binding. If you have any good ideas, let us know!

[pavpanchekha]

I wrote a blog post about one idea for this: https://pavpanchekha.com/blog/egg-bindings.html

It basically proposes using an explicit-substitution calculus plus de Bruijn indices. It's "e-graphy" but I'm not sure it's faster than rewriting the whole tree to remove an abstraction layer.

[Bastacyclop]

Interesting, I did not know about this post. We've also explored a similar design point in the paper mentioned above (https://arxiv.org/abs/2111.13040). You can also find a slightly updated version in my thesis (https://theses.gla.ac.uk/83323/, Sections 5.4 and 5.5).

I think it's worth mentioning that:

1. de Bruijn indices do not fully fix alpha renaming issues. Consider f (λx. f ) = %0 (λ. %1), where %i are De Bruijn indices. Although %0 and %1 are structurally different, they both correspond to the same variable f (paragraph 5.4.2, "True Equality Modulo α-renaming" in my thesis; this phenomenon is also discussed in https://www.microsoft.com/en-us/research/publication/hashing-modulo-alpha-equivalence-2/).
2. there exists relatively simple rewrite goals where this design point falls short (see line 'extraction? no', 'de Bruijn? yes', 'goal: binomial' in Table 5.3 of my thesis).