Information Technology Reference
In-Depth Information
f
c4
S
S
f
c3
m
c10
S
g
f
c3
m
c10
c8
S
S
E
E
R
2
S
g
c6
h
c7
f
c2
g
c6
h
c7
S
1
EE
E
R
R
S
S
S
S
S
S
12
E
1
2
R
c
c
c5
a
b
c9
a
b
c9
c5
c1
c1
f
m
S
S
R
R
g
h
R
S
S
S
1
2
R
c
a
b
Fig. 4.
a) Initial DAG for
E
=
{f
(
f
(
f
(
a
)))
≈ a,
f
(
f
(
a
))
≈ a,
g
(
c, c
)
≈
f
(
a
)
,g
(
c, h
(
a
))
≈ g
(
c, c
)
,c≈ h
(
a
)
,b≈ m
(
f
(
a
))
}
, b) Saturated graph for
E
on
the extended signature, c) DAG on the original signature
the
E
edge from
c
6
to
c
2
is replaced by an
E
edge from
c
6
to
c
3
,andaself-loop
composed of an
S
edge is added from
c
3
to itself.
c
4
and
c
3
can be merged, and
c
4
is removed from the graph (
c
4
c
3
). The
S
edge between
c
4
and
c
3
is removed
from the graph, and the
R
edge from
c
4
to
c
1
is simply removed, because there
is already an
R
edge from
c
1
to
c
3
.Weorientthe
E
edge between
c
10
and
c
9
from
c
10
to
c
9
(
c
10
c
9
), the
E
edge between
c
7
and
c
5
from
c
7
to
c
5
(
c
7
c
5
),
and the
E
edge between
c
6
and
c
3
from
c
6
to
c
3
(
c
6
c
3
), and the
E
edge
between
c
8
and
c
6
from
c
8
to
c
6
(
c
8
c
6
). We can apply an
SR
transformation
that adds an
S
edge from
c
8
to
c
5
, and removes the
S
edge from
c
8
to
c
7
.
c
8
and
c
6
are merged, and
c
8
is removed from the graph. The
R
edge between
c
8
and
c
6
is removed from the graph. We obtain the saturated graph labeled by
{c
1
,c
3
,c
5
,c
6
,c
7
,c
9
,c
10
}
presented
in Figure 4 b). The convergent rewrite system over the extended signature is:
{c
7
→ c
5
,c
6
→ c
3
,c
1
→ c
3
,c
10
→ c
9
,c→ c
5
,a→ c
1
,b→ c
9
,h
(
c
3
)
such that
{c
6
c
3
,c
7
c
5
,c
1
c
3
,c
10
c
9
}
→
c
7
,g
(
c
5
,c
5
)
→ c
6
,f
(
c
3
)
→ c
3
,m
(
c
3
)
→ c
10
}
. By applying
Compression
for the
redundant constants
c
10
,
c
7
,
c
6
and
c
1
,
Selection 2
to eliminate
c
5
and
c
9
,and
Selection 1
to eliminate
c
3
,weobtain
{h
(
a
)
→ c, g
(
c, c
)
→ a, f
(
a
)
→ a, m
(
a
)
→
b}
, the convergent rewrite system over
Σ
that we read from 4 c).
Example 2.
Figure 5 presents the constructions of a)
DAG
(
E
)where
E
=
{f
(
a, b
)
≈ a}
, and its saturated counter-parts following two strategies. In b),
Search WWH ::
Custom Search