Information Technology Reference
In-Depth Information
constants from
, and redirect
R
and
S
edges. They also remove cycles of
S
edges from the graph. Their exhaustive nondeterministic application produces a
DAG representing a convergent rewrite system over the original signature. The
graph data structure permits us to visualize in parallel what happens on the
original and extended signatures. For example, the
Selection 1
rule redirects
R
edges that were oriented in the “wrong” way during the abstract congruence
process. Indeed, if we need to redirect an
R
edge, it means that the ordering on
the constants of
K
K
that was used or constructed “on the fly” is in contradiction
with any ordering on terms of
T
(
Σ
).
4.1
Graph-Based Inference Rules
Definition 2.
A constant
c
0
of
K
labeling a vertex with an incident outgoing
R
edge is called
redundant
.
The
Compression
,
Selection 1
and
Selection 2
rules are provided in Figure 3.
Redundant constants of
are eliminated by the
Compression
rule. Both
Selec-
tion 1
and
Selection 2
implement the original selection rule of [2, 3].
Selection
1
is implemented by finding an
K
R
edge from a vertex
v
representing a term
t
of
T
(
Σ
) (i.e. all the vertices reachable from
v
following
S
edges are labeled by
constants of
Σ
K
on the graph, inversing the direction of this
R
edge, redirecting all the incoming
S
and
R
edges incident to
c
0
to
v
, and eliminating
c
0
from the graph. Hence, it
consists of picking a representative term
t
over
Σ
for the equivalence class of
c
0
.
Selection 2
is described as follows. If a vertex
v
is labeled by a constant
c
0
of
only) to a vertex labeled by a non redundant constant
c
0
of
,
and all the vertices reachable from
v
following
S
edges are labeled by constants
of
Σ
K
only, then the constant
c
0
of
K
is eliminated from the graph. A particular
case of this rule occurs when a vertex is labeled by a constant
c
0
of
K
and a
constant
c
of
Σ
.
4.2
Correctness
When applying
Compression
,
Selection 1
and
Selection 2
, the graph is in its
maximal structure sharing form. It can be represented by a state (
K,R
), where
K
is the set of constants disjoint from
Σ
labeling the vertices of the graph,
and
R
is the set of rewrite rules read from the graph over
Σ ∪K
.Weusethe
symbol
to denote the one-step transformation relation on states induced by
Compression
,
Selection 1
,and
Selection 2
.A
derivation
is a sequence of states
(
K,R
)
final
,ifno
mandatory
transformation rules (
Compression
,
Selection 1
,
Selection
2
) are applicable to this state. We prove that the
Compression
,
Selection 1
and
Selection 2
are sound in that the equational theory represented over
K
0
,R
0
)
(
K
1
,R
1
)
...
,and
K
i
⊆K
j
for
i ≥ j ≥
0. We call a state (
Σ
-terms
does not change. If there is a constant of
labeling a vertex of the graph, then
either
Compression
,
Selection 1
or
Selection 2
can be applied, and the exhaustive
application of
Compression
,
Selection 1
and
Selection 2
terminates. The termi-
nation is easily shown because the application of
Compression
,
Selection 1
or
K
Search WWH ::
Custom Search