Refinement E-Graphs
25 points by philzook
25 points by philzook
I've been looking for a data structure that solves some of the problems I have with polyhedral compilation. This may be it.
I have previously been considering the problem purely geometrically: "this polytope (a loop nest) is literally larger in every way than this other polytope." Using a refinement e-graph, this becomes "this polytope implies this polytope." This means that I can consider the combinatorially massive "set of all loop nests that imply or are strictly equivalent to this loop nest." Transformations like tiling can emerge from hardware-conscious heuristics (even if practically speaking they shouldn't) as equivalent expressions, and projection can become extraction rather than Fourier-Motzkin, which may be a better problem to solve.
So Phil is this how we get to unifying the SSI/union-find stuff?
me dunno. SSI seems a bit more like versioned egraphs https://dl.acm.org/doi/10.1145/3808249 / assume nodes https://arxiv.org/html/2404.12336v1 / colored e-graphs to me. I do think I have a blog post to be written suggested by Russel about how this can fit into a fat eid methodology.
In my mind the intuitive word "context" can be interpreted as assumptions/hypotheticals, refinement, or variable scope, which I think of as radically different things, but maybe from a deeper perspective they are all the same. There is a tendency during the process of understanding to go from "nothing is related -> everything is the same -> actually there are differences" and then maybe rinse and repeat.