Information Technology Reference
In-Depth Information
According the following lemma,
P
left
(
t
) is a lower bound and
P
right
(
t
)isan
upper bound of the interpretation of
t
in the induced algebra.
Lemma 7.
Let
(
Z
, {f
Z
}
f∈F
)
be an
F
-algebra such that every
f
Z
is a weakly
monotone polynomial. Let
t
be a term. For every assignment
α
:
V→
N
we have
]
Z
]
l
Z
[
)
.
Proof.
By induction on the structure of
α
(
t
)
[
α
]
N
(
t
)
[
α
(
t
t
.If
t ∈V
then [
α
]
Z
(
t
)=[
α
]
l
Z
(
t
)=
α
(
t
)=[
α
]
N
(
t
). Suppose
t
=
f
(
t
1
,...,t
n
). According to the induction hypothesis,
]
Z
]
l
Z
[
α
(
t
i
)
[
α
]
N
(
t
i
)
[
α
(
t
i
) for all
i
.Since
f
Z
is weakly monotone,
]
Z
(
]
Z
(
]
l
Z
(
]
l
Z
(
f
Z
([
α
t
1
)
,...,
[
α
t
n
))
f
Z
([
α
]
N
(
t
1
)
,...,
[
α
]
N
(
t
n
))
f
Z
([
α
t
1
)
,...,
[
α
t
n
))
By applying the weakly monotone function max
{
0
, ·}
we obtain max
{
0
,α
(
P
2
)
}
[
α
]
N
(
t
)
max
{
0
,α
(
P
1
)
}
where
P
1
=
f
Z
(
P
left
(
t
1
)
,...,P
left
(
t
n
)) and
P
2
=
f
Z
(
P
right
(
t
1
)
,...,P
right
(
t
n
)). We have
)=
0
if
n
(
P
1
)=0and
c
(
P
1
)
<
0
]
l
Z
(
[
α
t
α
(
P
1
)oth rw e
]
l
Z
and thus [
α
(
t
)
max
{
0
,α
(
P
1
)
}
. Likewise,
)=
α
(
n
(
P
2
))
if
c
(
P
2
)
<
0
]
Z
(
[
α
t
α
(
P
2
)
other ise
In the former case,
α
(
n
(
P
2
)) =
α
(
P
2
)
− c
(
P
2
)
>α
(
P
2
)and
α
(
n
(
P
2
))
0. In the
]
Z
latter case
α
(
P
2
)
0.Soinbothcaseswehave[
α
(
t
)
max
{
0
,α
(
P
2
)
}
. Hence
we obtain the desired inequalities.
Corollary 8.
Let
(
Z
, {f
Z
}
f∈F
)
be an
F
-algebra such that every
f
Z
is a weakly
monotone polynomial. Let
s
and
t
be terms. If
P
left
(
s
)
−P
right
(
t
)
>
0
then
s>
N
t
.
If
P
left
(
s
)
− P
right
(
t
)
0
then
s
N
t
.
P
left
Example 9.
Consider again the TRS of Example 5. By applying
to the
left-hand sides and
P
right
to the right-hand sides of the rewrite rules and the
dependency pairs, the following ordering constraints are obtained:
1: 0
0 :
x
+1
x
+1
5:
x
+1
x
+1
7:
x
+2
>x
+1
2: 0
0 :
0
0
6 :
x
+2
>x
8:
x
+2
>x
+1
The only difference with the constraints in Example 5 is the interpretation of
the term
s
(
half
(
x
)) on the right-hand side of rule 3. We have
P
right
(
half
(
x
)) =
n
(
x −
1) =
x
and thus
P
right
(
s
(
half
(
x
))) =
x
+ 1. Although
x
+ 1 is less precise
than max
+ 1, it is accurate enough to solve the ordering constraint
resulting from rule 3.
So once the interpretations
{
0
,x−
1
}
f
Z
are determined, we transform a rule
l → r
into the polynomial
). Standard techniques can then be used
to test whether this polynomial is positive (or non-negative) for all values in
P
left
(
l
)
− P
right
(
r
N
for the variables. The remaining question is how to find suitable interpretations
for the function symbols. This problem will be discussed in Section 5.
Search WWH ::
Custom Search