Congruence is an equivalence relation, so the algorithm is a special case of union-find algorithms for finding partitions.

We represent expressions as directed acyclic graphs, which are syntax trees for expressions, with sharing.

Within this structure we have union of inverted trees, representing union-find data structure.

Inverted tree representing equivalence classes.

• Calculus of Computation Textbook, Section 9.3