Information Technology Reference
In-Depth Information
2
The function
half
(
) computes the number of bits that
are needed to represent all numbers less than or equal to
x
) computes
and
bits
(
x
. Termination of this
TRS is proved in [2] by using the dependency pair method together with the
narrowing refinement. There are three dependency pairs:
x
half
(
s
(
s
(
half
(
6:
x
)))
→
x
)
bits
(
s
(
bits
(
half
(
s
(
7:
x
))
→
x
)))
bits
(
s
(
half
(
s
(
8:
x
))
→
x
))
)=
half
Z
By taking the interpretations
0
Z
=0,
half
Z
(
x
)=
x −
1,
bits
Z
(
x
(
x
)=
x
,
)=
bits
Z
and
s
Z
(
x
(
x
)=
x
+ 1, we obtain the following constraints over
N
:
1:
0
0
5 :
x
+1
x
+1
2:
0
0
6 :
x
+2
>x
x
{
,x−
}
x
>x
3:
+1
max
0
1
+1
7:
+2
+1
x
>x
4:
0
0
8 :
+2
+1
These constraints are satisfied, so the TRS is terminating, but how can an in-
equality like
x
+1
max
{
0
,x−
1
}
+ 1 be verified automatically?
3.2 Towards Automation
Because the inequalities resulting from interpretations with negative constants
may contain the max operator, we cannot use standard techniques for comparing
polynomial expressions. In order to avoid reasoning by case analysis (
x −
1
>
0
or
0 for constraint 3 in Example 5), we approximate the evaluation
function of the induced algebra.
Definition 6.
Given a polynomial
x −
1
P
with coecients in
Z
, we denote the con-
stant part by
c
(
P
)
and the non-constant part
P −c
(
P
)
by
n
(
P
)
.Let
(
Z
, {f
Z
}
f∈F
)
be an
F
-algebra such that every
f
Z
is a weakly monotone polynomial. With every
term
t
we associate polynomials
P
left
(
t
)
and
P
right
(
t
)
with coecients in
Z
and
variables in
t
as indeterminates:
t
if
t
is a variable
P
left
(
t
)=
0
if
t
=
f
(
t
1
,...,t
n
)
,
n
(
P
1
)=0
,and
c
(
P
1
)
<
0
P
1
otherwise
where
P
1
=
f
Z
(
P
left
(
t
1
)
,...,P
left
(
t
n
))
and
t
if
t
is a variable
P
right
(
t
)=
n
P
2
)
t
f
t
1
,...,t
n
)
and
c
P
2
)
<
(
if
=
(
(
0
P
2
otherwise
where
P
2
=
f
Z
(
P
right
(
t
1
)
,...,P
right
(
t
n
))
.Let
α
:
V→
N
be an assignment. The
]
l
Z
result of evaluating
P
left
(
t
)
and
P
right
(
t
)
under
α
is denoted by
[
α
(
t
)
and
]
Z
[
α
(
t
)
. The result of evaluating a polynomial
P
under
α
is denoted by
α
(
P
)
.
Search WWH ::
Custom Search