E-graphs (Large Resource)
E-graphs (Large Resource)

E-graphs

E-graphs are a data structure that efficiently holds terms and equalities between terms.
Terms are contextually referred to as "e-nodes". A set of equivalent e-nodes is an "e-class", and each e-class is referred to by a numeric ID.
An e-graph contains the e-classes and equivalence relations between e-nodes. E-graphs are internally represented by a union-find data-structure of e-classs, and a mapping of e-classes to/from e-nodes (source: Wikipedia).
E-graphs are useful in semantic program analysis and rewriting, as well as theorem proving and other applications. There's even a conference workshop dedicated to them: EGRAPHS, part of PLDI 2023. A (almost) real-world example is their use in cranelift (link also provides another explanation of e-graphs and elaborates on why/how they're useful).