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