Information Technology Reference
In-Depth Information
ordering on the constants of
. There is a tradeoff between the effort spent in
constructing an ordering, the time spent in comparing two constants, and the
lengths of derivations (number of graph transformations). The graph data struc-
ture permits us to understand the influence of the ordering on the length of
any derivation, and to construct “on the fly” orderings that control the number
of inferences. It suggests new ecient procedures for constructing ecient ab-
stract congruence closures. Indeed, the number of times we apply
SR
and
RRout
depends on how we apply
Orient
. Applying an
RRout
rule can create an
SR
configuration; so we would orient an
E
edge in the direction that creates the
less
SR
and
RRout
configurations.
Merge
configurations can be created after
the application of an
SR
rule.
When constructing the ordering, we do not allow backtracking, so we are
only interested in
feasible
orderings, i.e. orderings that will produce
unfailing
derivations, i.e. derivations terminating with a saturated graph (as defined in
definition 1). Starting from an initial state representing the initial DAG, the
maximal derivation is in
O
(
nδ
), where
n
is the number of vertices of the initial
DAG, and
δ
is the depth of the ordering (i.e. the longest chain
c
0
c
1
...
c
δ
.) So, any maximal derivation starting from an initial state is bounded by a
quadratic upper bound. Indeed, any total and linear order is feasible and can be
used. There exits a feasible ordering with smaller depth that can be computed
“on the fly,” and produces a maximal derivation of length
nlog
(
n
) [2, 3]. This
ordering is based on orienting an
E
edge from
v
0
to
v
1
if the number of elements
of the equivalence class of
Constant
(
v
0
) is less than or equal to the number
of elements of the equivalence class of the
Constant
(
v
1
). This can be applied
only if all
RRout
and
RRin
inference rules have been processed for
v
0
and
v
1
.
The number of elements in an equivalence class of a constant
Constant
(
v
)is
computed by counting the number of incoming
R
edges in a vertex
v
.
A first implementation of our method is available for online experimentation
at:
http://www.csis.pace.edu/
∼
scharff/CC
.Itiswritteninjava,anduses
java servlets, and XML. The implemented system contains (i) a parsing com-
ponent that also transforms a given set of equalities into a DAG, (ii) a graph
component that manages the graph, and (iii) an inferences component that deals
with the application of the transformation rules. In particular, the strategy for
application of rules is coded in XML, and therefore, is modifiable. An ecient
strategy applies simplifications before orienting equalities (one at a time):
(
Orient .
((
SR . Merge
)
∗
)
∗
.
(
RRout . RRin .
((
SR . Merge
)
∗
)
∗
)
∗
)
∗
4
The ordering that is used in the implementation is a total and linear ordering.
Given a signature and a set of equalities, the system displays the initial
C
equal-
ities and
D
rules, the convergent rewrite system over the extended signature and
the convergent rewrite system over the original signature. Some statistics results
are also provided: the number of inferences of each type, and the processing
times.
K
4
∗
means that the strategy is applied 0 or more times.
X.Y
means that
Y
is applied
after
X
.
Search WWH ::
Custom Search