Information Technology Reference
In-Depth Information
α
∗
(
Proof.
We show that [
α
]
N
(
t
)=
Q
(
t
)) by induction on
t
.If
t
is a variable
α
∗
(
α
∗
(
then [
α
]
N
(
t
)=
α
(
t
)=
t
)=
Q
(
t
)). Suppose
t
=
f
(
t
1
,...,t
n
). Let
P
=
α
∗
(
f
Z
(
Q
(
t
1
)
,...,Q
(
t
n
)). The induction hypothesis yields [
α
]
N
(
t
i
)=
Q
(
t
i
)) for
all
i
and thus
α
∗
(
,...,α
∗
(
[
α
]
N
(
t
)=
f
N
(
Q
(
t
1
))
Q
(
t
n
)))
α
∗
(
,...,α
∗
(
,α
∗
(
=max
{
0
,f
Z
(
Q
(
t
1
))
Q
(
t
n
)))
}
=max
{
0
P
)
}
We distinguish three cases, corresponding to the definition of
Q
(
t
).
α
∗
(
-
First suppose that
P ∈P
0
. This implies that
P
)
0 and thus we have
,α
∗
(
α
∗
(
α
∗
(
α
∗
(
max
{
0
P
)
}
=
P
). Hence [
α
]
N
(
t
)=
P
)=
Q
(
t
)).
α
∗
(
,α
∗
(
-
Next suppose that
P ∈P
<
0
.So
P
)
<
0 and thus max
{
0
P
)
}
=0.
α
∗
(
Hence [
α
]
N
(
t
)=0=
Q
(
t
)).
-
In the remaining case we do not know the status of
P
.Wehave
Q
(
t
)=
v
(
P
)
α
∗
(
,α
∗
(
and thus
Q
(
t
)) = max
{
0
P
)
}
which immediately yields the desired
α
∗
(
identity [
α
]
N
(
t
)=
Q
(
t
)).
Corollary 17.
Let
(
Z
, {f
Z
}
f∈F
)
be an
F
-algebra such that every
f
Z
is a poly-
α
∗
(
nomial. Let
s
and
t
be terms. If
Q
(
s
)=
Q
(
t
)
then
s
=
N
t
.If
Q
(
s
)
−Q
(
t
))
>
0
α
∗
(
for all assignments
α
:
V→
N
then
s>
N
t
.If
Q
(
s
)
− Q
(
t
))
0
for all as-
signments
α
:
V→
N
then
s
N
t
.
Example 18.
Consider again dependency pair 15 from Example 10:
mod
(
s
(
mod
(
s
(
x
)
,
s
(
y
))
→
x
)
−
s
(
y
)
,
s
(
y
))
(
mod
(
s
(
(
mod
(
s
(
We have
Q
x
)
,
s
(
y
))) =
x
+1 and
Q
x
)
−
s
(
y
)
,
s
(
y
))) =
v
(
x − y
).
Since
)asavariable),
the above corollary cannot be used to conclude that 15 is strictly decreasing.
However, if we estimate
x
+1
−v
(
x−y
) may be negative (when interpreting
v
(
x−y
v
(
x − y
)by
x
, the non-negative part of
x − y
,thenwe
obtain
x
+1
− x
= 1 which is clearly positive.
Given a polynomial
P
with coecients in
Z
, we denote the non-negative part
of
P
by
N
(
P
).
Lemma 19.
Let
Q
be a polynomial with integer coecients. Suppose
v
(
P
)
is
Q
an abstract variable that occurs in
Q
but not in
N
(
Q
)
.If
is the polynomial
α
∗
(
α
∗
(
Q
)
for all
obtained from
Q
by replacing
v
(
P
)
with
N
(
P
)
then
Q
)
assignments
α
:
V→
N
.
α
∗
(
Proof.
Let
α
:
V→
N
be an arbitrary assignment. In
Q
) every occurrence
α
∗
(
,α
∗
(
α
∗
(
of
v
(
P
) is assigned the value
v
(
P
)) = max
{
0
P
)
}
.Wehave
N
(
P
))
α
∗
(
α
∗
(
P
)
v
(
P
)). By assumption,
v
(
P
) occurs only in the negative part of
Q
.
α
∗
(
α
∗
(
Q
).
Hence
Q
is (strictly) anti-monotone in
v
(
P
) and therefore
Q
)
) holds, the idea now is to first
use standard techniques to test the non-negativeness of
In order to determine whether
s
N
t
(or
s>
N
t
Q
=
Q
(
s
)
− Q
(
t
) (i.e.,
Search WWH ::
Custom Search