Information Technology Reference
In-Depth Information
Construction
of
a
congruence
closure
starts
from
an
initial
tuple
(
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
more details.
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 (
K,Ex,Rx
),
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
.
3.4 Correctness
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].
Search WWH ::
Custom Search