Séminaire Cambium, Inria Paris
                                 Remote talk
                             Lundi 26 août, 10h30

                                Rudi Schneider
                                  TU Berlin

                Slotted E-Graphs - E-Graphs with Name Binding

Representing languages with bound variables in e-graphs is
challenging. Using plain names results in reduced sharing, as multiple
terms that are equivalent up to renaming are represented redundantly
in the e-graph. De-Bruijn indices suffer from the same problem.
Furthermore, rewriting can trigger the need to rename variables (or
shift de-bruijn indices), such as when performing 𝛽-reduction, which
can dramatically increase the size of the e-graph.

In this talk, we present a novel approach to represent bound variables
in e-graphs by making them a built-in feature of the data structure.
In our slotted e-graph, e-classes are parameterized by slots
abstracting over all free variables. Referring to an e-class now
requires instantiating it by assigning a name from the users context
to each slot. Renaming variables corresponds simply to different
instantiations of an e-class. This allows us to unify redundant
e-classes that only differ in variable names, resulting in stronger
sharing guarantees.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.