Information Technology Reference
In-Depth Information
s
N
t
, closure under contexts is obtained for free. So we could take (=
N
,>
N
)
as reduction pair. This works fine in the above example because the induced
algebra is a model of the set of usable rules
>
N
orients dependency
pair 15. However, requiring that all dependency pairs in a cycle are compatible
with =
N
∪>
N
is rather restrictive because dependency pairs that are transformed
into a polynomial constraint of the form
{
7
,
8
}
and
2
x
x
or
x
+2
y
x
+
y
cannot be
handled. So we will allow
N
for the orientation of dependency pairs in a cycle
C
C
>
N
.(Note
but insist that at least one dependency pair in
is compatible with
that the relation =
N
∪ >
N
is properly contained in
N
.) The theorems below
state the soundness of this approach in a more abstract setting. The proofs
are straightforward modifications from the ones in [13]. The phrase “there are
no minimal
is non-
terminating then this is due to a different cycle of the dependency graph.
C
-rewrite sequences” intuitively means that if a TRS
R
Theorem 11.
Let
R
beaTRSandlet
C
be a cycle in its dependency graph. If
there exists an algebra
A
equipped with a well-founded order
>
such that
R⊆
=
A
,
C⊆
A
,and
C∩>
A
=
∅
then there are no minimal
C
-rewrite sequences.
of the dependency graph
can be ignored if the conditions of Theorem 11 are satisfied. A similar statement
holds for innermost termination.
In other words, when proving termination, a cycle
C
Theorem 12.
Let
R
beaTRSandlet
C
be a cycle in its innermost dependency
graph. If there exists an algebra
A
equipped with a well-founded order
>
such
that
U
(
C
)
⊆
=
A
,
C⊆
A
,and
C∩>
A
=
∅
then there are no minimal innermost
C
-rewrite sequences.
The difference with Theorem 11 is the use of the
innermost
dependency
graph and, more importantly, the replacement of the set
R
of all rewrite rules
by the set
, which in general is a much smaller set.
Very recently, it has been proved [13, 22] that the usable rules criterion can also
be used for termination, provided the employed reduction pair is
U
(
C
)of
usable rules
for
C
C
E
-compatible.
However, replacing
R
by
U
(
C
) in Theorem 11 would be unsound. The reason is
that the TRS
C
E
admits no non-trivial models.
Example 13.
Consider the following non-terminating TRS
R
:
1:
h
(
f
(
a
,
b
,x
))
→
h
(
f
(
x, x, x
))
2 :
g
(
x, y
)
→ x
3:
g
(
x, y
)
→ y
The only dependency pair
h
(
f
(
a
h
(
f
(
)) forms a cycle in the
dependency graph. There are no usable rules. If we take the polynomial inter-
pretation
a
Z
=1,
b
Z
=0,
f
Z
(
,
b
,x
))
→
x, x, x
,and
h
Z
x, y, z
)=
x−y
(
x
)=
x
then the dependency
pair is transformed into 1
>
0. Note that it is not possible to extend the inter-
pretation to a model for
R
.Choosing
h
Z
(
x
) = 0 will take care of rule 1, but there
is no interpretation
g
Z
such that max
{
0
,
g
Z
(
x, y
)
}
=
x
and max
{
0
,
g
Z
(
x, y
)
}
=
y
for all natural numbers
x
and
y
.
Search WWH ::
Custom Search