Library / Symbolic Computation
Equality saturation is an optimization strategy that accumulates many equivalent expressions before choosing a preferred result. It is one of the clearest examples of symbolic search becoming practical.
In ordinary rewriting, a system often chooses one valid rewrite and moves on. Equality saturation takes a different approach. It keeps adding equivalent forms into a shared structure, usually an e-graph, until enough of the search space has been exposed to make a better-informed decision.
The goal is not to apply every rewrite forever. The goal is to avoid losing good alternatives simply because the system committed too early to one path.
Equality saturation separates two questions:
Once these are separated, the extraction step can use a meaningful cost model rather than inheriting the accidental biases of one rewrite order.
This change in control flow is what makes equality saturation feel so different from traditional simplification. It turns rewrite choice into a search problem with an explicit decision stage.
Equality saturation does not define one universal notion of simplicity. A preferred result might be shorter to print, cheaper to evaluate, more numerically stable, easier to differentiate, or better suited to tensor fusion. The extraction rule depends on what the system is optimizing for.
This is one of the strongest reasons to separate saturation from extraction. The graph can record equivalence broadly, while the cost model can stay honest about the actual target: readability, runtime, memory behavior, numerical quality, or some domain-specific objective.
Sym uses e-graphs and cost models, including tensor-aware cost logic. That makes equality saturation more than a theoretical curiosity here. It is part of the story of how symbolic search can support practical optimization tasks.
That practical angle matters. Equality saturation becomes much easier to appreciate once it is tied to actual extraction decisions rather than described only as an abstract data-structure technique.
In broad outline, a system starts with one expression, adds it to an e-graph, applies a set of valid rewrites, merges any newly discovered equivalent forms, and repeats until a stopping condition is reached. The stopping condition might be a node budget, a rewrite budget, or a point where new rewrites no longer add useful structure.
Extraction comes afterward. That separation is why equality saturation often feels different from traditional simplifiers. It behaves less like a single rewrite path and more like a managed search over a space of equivalent forms.
Equality saturation is not free. Rich rule sets can make the graph grow quickly, and cost-model design can become a serious engineering problem. The technique pays off when there are many valid alternatives and the best final form genuinely depends on context.
That is why it belongs beside e-graphs, canonical forms, and tensor optimization in this library. It is a disciplined answer to the question of how symbolic software can explore widely without losing track of mathematical equivalence.
In that sense, equality saturation is not only a technique for optimization. It is also a way of organizing symbolic search so that exploration and preference do not get tangled together too early.