Information Technology Reference
In-Depth Information
4.2
Towards Automation
How do we verify a constraint like
? The approach that
we developed in Section 3.2 for dealing with negative constants is not applicable
because Lemma 7 relies essentially on weak monotonicity of the polynomial
interpretations.
Let
x
+1
>
max
{
0
,x− y}
P
0
be a subset of the set of polynomials
P
with integer coecients
such that
α
(
P
)
0 for all
α
:
V→
N
for which membership is decidable. For
instance,
P
0
could be the set of polynomials without negative coecients. We
define
P
<
0
in the same way.
Definition 14.
Let
(
Z
, {f
Z
}
f∈F
)
be an algebra. With every term
t
we associate
a polynomial
Q
(
t
)
as follows:
t
if
t
is a variable
P
if
t
=
f
(
t
1
,...,t
n
)
and
P ∈P
0
Q
(
t
)=
0
if
t
=
f
(
t
1
,...,t
n
)
and
P ∈P
<
0
v
(
P
)
otherwise
where
P
=
f
Z
(
Q
(
t
1
)
,...,Q
(
t
n
))
. In the last clause
v
(
P
)
denotes a fresh
abstract
variable that we uniquely associate with
P
.
There are two kinds of indeterminates in
Q
(
t
): ordinary variables occurring
in
t
and abstract variables. The intuitive meaning of an abstract variable
v
(
P
)is
max
. The latter quantity is always non-negative, like an ordinary variable
ranging over the natural numbers, but from
{
0
,P}
v
(
P
) we can extract the original
polynomial
and this information may be crucial for a comparison between
two polynomial expressions to succeed. Note that the polynomial
P
P
associated
with an abstract variable
v
(
P
) may contain other abstract variables. However,
because
) is different from previously selected abstract variables, there are
no spurious loops like
v
(
P
P
1
=
v
(
x − v
(
P
2
)) and
P
2
=
v
(
x − v
(
P
1
)).
P
<
0
in the above definition is to make our ap-
proach independent of the particular method that is used to test non-negativeness
or negativeness of polynomials.
The reason for using
P
0
and
Definition 15.
With every assignment
α
:
V→
N
we associate an assignment
α
∗
:
V→
N
defined as follows:
)=
max
,α
∗
(
{
0
P
)
}
if
x
is an abstract variable
v
(
P
)
α
∗
(
x
α
(
x
)
otherwise
The above definition is recursive because
P
may contain abstract variables.
However, since
) is different from previously selected abstract variables, the
recursion terminates and it follows that
v
(
P
α
∗
is well-defined.
Theorem 16.
Let
(
Z
, {f
Z
}
f∈F
)
be an algebra such that every
f
Z
is a polynomial.
t
α
α
t
α
∗
(
Q
t
Let
be a term. For every assignment
we have
[
]
N
(
)=
(
))
.
Search WWH ::
Custom Search