Email Gateway (Sep 23 2025 at 19:42): Email Gateway (Sep 23 2025 at 19:42):From: Patrick Nicodemus <gadget142@gmail.com>
The Nelson-Oppen congruence closure paper gives a decision algorithm for
the theory of LISP lists. You can generalize this to other universal
algebra theories: to decide equality between two terms over an equational
theory, \forall x1...xn, t1 = t2. One starts by adding ground equations
whenever one side of an equation unifies with a subterm of the goal, adding
these as equivalence constraints, and taking the congruence closure. Then
one repeats the procedure, trying to unify one side of the universally
quantified theorems with a subterm of the new set of subterms (or sub-node
in the e-graph). If you are lucky then this process eventually hits a
fixpoint in the sense that every rewrite of an e-node in the graph yields
another e-node already in the graph, for such theories this gives a nice
decision procedure.
I'm interested in some sufficient conditions on the theory such that for
every term t, the e-graph built by repeatedly rewriting subterms in t
according to axioms in t eventually stabilizes. For example the theory
\forall x. x = f(x), after the first time I apply this to a term t, I have
a new term f(t) in my graph, but t ~ f(t) so I don't get any new
equivalence classes in the term graph. What references should I look at for
conditions on the theory that guarantee this stabilizes?
Last updated: Oct 08 2025 at 20:22 UTC