hegg VS sdsl-lite

Equality graphs (e-graphs) for theorem proving and equality saturation and other equality-related things.

They're awesome data structures that efficiently maintain a congruence relation over many expressions

> At a high level, e-graphs extend union-find to compactly represent equivalence classes of expressions while maintaining a key invariant: the equivalence relation is closed under congruence.

e.g. If I were to represent "f(x)" and "f(y)" in the e-graph, and then said "x == y" (merged "x" and "y" in the e-graph), then the e-graph, by congruence, would be able to tell me that "f(x) == f(y)"

e.g. If I were to represent "a(2/2)", in the e-graph, then say "2/2 == 1", and "x1 == x", by congruence the e-graph would know "a*(2/2) == a" !

The most recent description of e-graphs with an added insight on implementation is https://arxiv.org/pdf/2004.03082.pdf to the best of my knowledge.

P.S: I'm currently implementing them in Haskell https://github.com/alt-romes/hegg

Succinct Data Structures [0] [1]. It encompass many different underlying data structure types but the overarching idea is that you want small data size while still keeping "big O" run time.

In other words, data structures that effectively reach a 'practical' entropy lower bound while still keeping asymptotic run time.

[0] https://en.wikipedia.org/wiki/Succinct_data_structure

[1] https://github.com/simongog/sdsl-lite

The book mentioned in another comment is probably the best way to go. But FYI, documentation for some data structures include references. An SDSL-lite example can be found here. And its equivalent in SDSL-RS can be found here.