Information Technology Reference
( E s ,E e ,E r ,V,K, ∅
), the first five components of which are derived from
DAG ( E )(sothat E r is empty) 3 . Transformation rules can then be applied non-
deterministically. The rules SR , RRout and RRin are only applied if they result
in a new edge.
There are various possible strategies for orienting equality edges. One may
start with a fixed, total ordering on constants, or else construct an ordering “on
the fly.” Different strategies may result in different saturated graphs, see Exam-
ple 2. The choice of the ordering is crucial for eciency reasons, as discussed in
section 6. The ordering also prevents the creation of cycles of with equality or
rewrite edges, though the SR rule may introduce self-loops or cycles involving
subterm edges. (Such a cycle would indicated that a term is equivalent to one of
its subterms in the given equational theory.) See section 3.3 and example 2 for
Definition 1. We say that a graph G is saturated if it contains only subterm
and rewrite edges and no further graph transformation rules can be applied.
3.3 Extraction of Rules
We can extract D -rules, C -rules and C -equalities from the initial and trans-
formed graphs as follows. A vertex v 0 with ExtTerm ( v 0 )= t and Constant ( v 0 )
= c 0 induces a D -rule t → c 0 . An equality edge v 1 − E v 2 induces a C -equality
c 1 ≈ c 2 ,where Constant ( v 1 )= c 1 and Constant ( v 2 )= c 2 .Arewriteedge v 1 → R
v 2 induces a C -rule c 1 ≈ c 2 ,where Constant ( v 1 )= c 1 and Constant ( v 2 )= c 2 .
With each tuple ( E s ,E e ,E r ,V,K,KC ) we associate a triple (
where Ex is the set of C -equalities and Rx is the set of D and C -rules extracted
from the graph G specified by the first four components of the given tuple. Thus,
with the initial graph we associate a triple (
K 0 ,Ex 0 ,Rx 0 ), where Rx 0 is empty
and Ex 0 represents the same equational theory over Σ -terms as the given set of
equations E . The goal is to obtain a triple (
K n ,Ex n ,Rx n ), where Ex n is empty
and Rx n is an abstract congruence closure of E .
The following can be established:
- Exhaustive application of the graph transformation rules is sound in that
the equational theory represented over Σ -terms does not change.
- Exhaustive application of the graph transformation rules terminates .This
can be proved by assigning a suitable weight to graphs that decreases with
each application of a transformation rule.
- Exhaustive application of the rules is complete in that the rewrite system
that can be extracted from the final graph is convergent and an abstract con-
gruence closure for E . (If the optional RRin rule has been applied exhaus-
tively, the final rewrite system over the extended signature is right-reduced.)
3 We essentially begin with the same graph as the Nelson-Oppen procedure, as de-
scribed in the abstract congruence closure framework [2, 3].