Information Technology Reference
In-Depth Information
4
Negative Coecients
Let us start with an example which shows that negative coecients in polynomial
interpretations can be useful.
Example 10.
Consider the following variation of a TRS in [2]:
1:
0
x →
true
7:
x −
0
→ x
2:
s
(
x
)
0
→
false
8:
s
(
x
)
−
s
(
y
)
→ x − y
3:
s
(
x
)
s
(
y
)
→ x
y
9:
if
(
true
,x,y
)
→ x
4:
mod
(
0
,
s
(
y
))
→
0
10:
if
(
false
,x,y
)
→ y
5:
mod
(
s
(
x
)
,
0
)
→
0
6:
mod
(
s
(
x
)
,
s
(
y
))
→
if
(
y
x,
mod
(
s
(
x
)
−
s
(
y
)
,
s
(
y
))
,
s
(
x
))
There are 6 dependency pairs:
s
(
→ x
y
11:
s
(
x
)
y
)
−
s
(
→ x −
y
12:
s
(
x
)
y
)
13:
mod
(
s
(
if
(
x
)
,
s
(
y
))
→
y
x,
mod
(
s
(
x
)
−
s
(
y
)
,
s
(
y
))
,
s
(
x
))
14:
mod
(
s
(
→ y
x
x
)
,
s
(
y
))
15:
mod
(
s
(
mod
(
s
(
x
)
,
s
(
y
))
→
x
)
−
s
(
y
)
,
s
(
y
))
16:
mod
(
s
(
−
s
(
x
)
,
s
(
y
))
→
s
(
x
)
y
)
Since the TRS is non-overlapping, it is sucient to prove innermost termination.
The problematic cycle in the (innermost) dependency graph is
C
=
{
15
}
.The
usable rewrite rules for this cycle are
U
(
C
)=
{
7
,
8
}
. We need to find a reduction
pair (
,>
) such that rules 4 and 5 are weakly decreasing (i.e., compatible with
)
and dependency pair 15 is strictly decreasing (with respect to
>
). The only way
to achieve the latter is by using the observation that
s
(
x
) is semantically greater
than the syntactically larger term
s
(
x
)
−
s
(
y
). If we take the natural interpretation
1, and
0
Z
= 0, together with
mod
Z
−
Z
(
x, y
x − y
,
s
Z
(
x
x −
x, y
x
)=
)=
(
)=
then
we obtain the following ordering constraints over the natural numbers:
7:
x
x
8: max
{
0
,x− y}
max
{
0
,x− y}
15:
x
+1
>
max
{
0
,x− y}
4.1
Theoretical Framework
The constraints in the above example are obviously satisfied, but are we allowed
to use an interpretation like
in (innermost) termination proofs?
The answer appears to be negative because Lemma 4 no longer holds. Because
the induced interpretation
−
Z
(
x, y
)=
x−y
−
N
(
x, y
)=max
{
0
,x− y}
is not weakly monotone in
its second argument, the order
N
of the induced algebra is not closed under
contexts, so if
s
N
t
then it may happen that
C
[
s
]
N
C
[
t
]. Consequently,
we do not obtain a reduction pair. However, if we have
s
=
N
t
rather than
Search WWH ::
Custom Search