Information Technology Reference
In-Depth Information
V31
V31
R
R
V3n3
R
R
...
V0'
V0
V3n3
R
E
...
V0'
f c0'
f c0
f c0'
V41
V41
...
...
R
S
E
S
V4n4
V4n4
...
...
V11
S
S
S
S
S
S
V11
S
E
...
S
S
S
S
E
V1n1
V1n1
...
...
...
V01
V0n
...
...
V01
V0n
V21
V21
E
E
V2n2
V2n2
C0>C0'
Fig. 2.
Merge
graph transformation rule
4
Rewrite System over the Original Signature
In this section we explain how to obtain a convergent rewrite system over the
original signature
Σ
)froma
graph
G
saturated with respect to
Orient
,
SR
,
RRout
,
RRin
and
Merge
.Basi-
cally, at this point, constructing the convergent rewrite system over
Σ
(independent from the ordering on constants of
K
from
G
K
from
G
. Indeed, the constants of
K
consists of eliminating the constants of
are
“names” of equivalence classes, and the same equivalence class may have several
“names.” There are two methods. The first method works on the convergent
rewrite system over
Σ ∪K
extracted from
G
. Redundant constants (constants
appearing on the left-hand side of a
C
rules) are eliminating by applications
of
compression
rules and non-redundant constants are eliminated by
selection
rules as described in [2, 3]. The second method, that we propose in this article,
permits us to work directly and only on the graph
G
, by transforming the graph
in a way reminiscent of the compression and selection rules. We define the no-
tion of redundant constants on a saturated graph with respect to
Orient
,
SR
,
RRout
,
RRin
and
Merge
, and introduce three mandatory graph transformation
rules:
Compression
,
Selection 1
and
Selection2
. These inference rules eliminate
Search WWH ::
Custom Search