On the Combination of Congruence Closure and Completion - Artificial Intelligence and Symbolic Computation - page 107

for which Constant ( v ) = Constant ( w ) can be replaced by a rewrite edge (one

way or the other).
The ordering needs to be defined on constants in K only, not on terms

over Σ ∪K . Term orderings, as employed in SOUR-graphs, are inherently more

restrictive and may be detrimental to the eciency of the congruence closure
construction. For instance, well-founded term orderings must be compatible with
the subterm relation, whereas we may choose an ordering with Constant ( v )

Constant ( w ) for eciency reasons, even though Term ( v ) may be a subterm of
Term ( w ).
The SR rule replaces one subterm edge by another one. In logical terms it
represents the simplification of a subterm by rewriting, or in fact the simulta-
neous simplification of all occurrences of a subterm, if the graph presentation
encodes full structure sharing for terms.
The RRout and RRin each replace one rewrite edge by another. They corre-
spond to certain equational inferences with the underlying rewrite rules (namely,
critical pair computations and compositions, which for ground terms are also
simplifications). The RRin rule is useful for eciency reasons, though one can
always obtain a congruence closure without it. If the rule is applied exhaustively,
the resulting congruence closure will be a right-reduced rewrite system over the
extended signature.
The Merge rule collapses two vertices that represent the same term over the
extended signature into a single vertex. It ensures closure under congruence and
full structure sharing.
The graph transformation rules are formally defined as pairs of tuples of
the form ( E s ,E e ,E r ,V,K,KC ) ( E s ,E e ,E r ,V , K ,KC ), where the

individual components specify a graph, an extended signature, and an ordering
on new constants, before and after rule application. Specifically,

→

- the first three components describe the sets of subterm, equality, and rewrite
edges, respectively;
- the fourth component describes the set of vertices;
- the fifth component describes the extension of the original signature

2 ;

Σ

and
- the last component describes the (partial) ordering on constants. Specifically,
KC is a set of “ordering constraints” of the form

.
(A set of such constraints is considered satisfiable if there is an irreflexive,
transitive relation on

{c i c j | c i ,c j ∈K}

K that meets all of them.)

The specific conditions for the various rules are shown in Figures 1 and 2. For
example, if two vertices v and w represent the same flat term (over the extended
signature), then the merge rule can be used to delete one of the two vertices,
say v , and all its outgoing subterm edges. All other edges that were incident on
v need to be redirected to w , with the proviso that outgoing rewrite edges have
to be changed to equality edges.

2 We have K ⊆K , which is different from abstract congruence closure [2, 3], where
new constants can be introduced.