Information Technology Reference
In-Depth Information
E
R
1
S
f c3
f c3
R
S
1
S
2
S1
S 2
f c3
S
2
a c1
b c2
a c1
b c2
a c1
b c2
R
f
S
S
2
1
a
b
Fig. 5.
a) Initial DAG for
E
=
{f
(
a, b
)
≈ a}
, b) Saturated graph for
E
with
c
3
c
1
,
c) Saturated graph for
E
with
c
1
c
3
, and d) DAG on the original signature
c
3
c
1
and in c),
c
1
c
3
. In c), there is a self-loop composed of an
S
edge. The two saturated graphs with respect to
Orient
,
SR
,
RRout
,
RRin
and
Merge
are labeled by
{c
1
,c
2
,c
3
}
. In b), the rewrite system on the extended
signature is
{f
(
c
1
,c
2
)
→ c
3
,c
3
→ c
1
,a→ c
1
,b→ c
2
}
,andinc),itis
{f
(
c
3
,c
2
)
→ c
3
,c
1
→ c
3
,a→ c
1
,b→ c
2
}
. Both saturated graphs generate
the DAG d) on the original signature representing
{f
(
a, b
)
→ a}
.
6
Complexity Results and Implementation
Our algorithms to obtain rewrite systems over extended and original signatures
use only polynomial space to store the rewrite systems. Let
n
be the number of
vertices of the initial DAG. During the abstract congruence process, there can
only be
n
2
1)
/
2 equality and rewrite edges, because
an edge can only be added once to a graph, and there are never two equality or
rewrite edges between the same vertices (because of the ordering on the constants
of
subterm edges, and
n
(
n −
K
.) Moreover, the number of vertices can only decrease (as a result of merging).
In comparing our graph-based approach with the logic-based approach of [2,
3], we find that graphs support full structure sharing and consequently our ap-
proach will tend to lead to fewer applications of transformation rules than cor-
responding applications of logical inference rules in the standard method. This
by itself does not imply that our approach will be more ecient as full struc-
ture sharing depends on systematic application of the
Merge
rule, which can be
expensive.
Ecient implementations of congruence closure require specialized data
structures. Also, abstract congruence closure eciency is parametrized by the
choice or construction “on the fly” of the ordering on the constants of
.In
our case,
E
edges are oriented into
R
edges using this ordering. There exist
naive ways to choose the ordering. For example, we can use a total and linear
K
Search WWH ::
Custom Search