Information Technology Reference

In-Depth Information

Polynomial Interpretations

with Negative Coecients

Nao Hirokawa and Aart Middeldorp

Institute of Computer Science, University of Innsbruck, 6020 Innsbruck, Austria

{
nao.hirokawa,aart.middeldorp
}
@uibk.ac.at

Abstract.
Polynomial interpretations are a useful technique for proving

termination of term rewrite systems. We show how polynomial interpre-

tations with negative coecients, like
x −
1 for a unary function symbol

or
x − y
for a binary function symbol, can be used to extend the class of

rewrite systems that can be automatically proved terminating.

1

Introduction

This paper is concerned with automatically proving termination of first-order

rewrite systems by means of polynomial interpretations. In the classical ap-

proach, which goes back to Lankford [16], one associates with every

n

-ary func-

tion symbol

indeterminates,

which induces a mapping from terms to polynomials in the obvious way. Then

one shows that for every rewrite rule

f

a polynomial

P
f

over the natural numbers in

n

l → r

the polynomial

P
l

associated with

the left-hand side

l

is strictly greater than the polynomial

P
r
associated with the

right-hand side

0 for all values of the indeterminates. In order to

conclude termination, the polynomial

r

, i.e.,

P
l
−P
r
>

P
f

associated with an

n

-ary function sym-

bol

indeterminates. Techniques for finding

appropriate polynomials as well as approximating (in general undecidable) poly-

nomial inequalities

f

must be strictly monotone in all

n

0 are described in several papers (e.g. [4, 6, 9, 15, 19]).

As a simple example, consider the rewrite rules

P>

x

+
0

→ x

x ×

0

→

0

x

+
s
(

y

)

→

s
(

x

+

y

)

x ×

s
(

y

)

→

(

x × y

)+

x

Termination can be shown by the strictly monotone polynomial interpretations

×
N
(

x, y

)=2

xy

+

y

+1

+
N
(

x, y

)=

x

+2

y

s
N
(

x

)=

x

+1

0
N
=1

over the natural numbers:

x

+2

>x

2

x

+2

>

1

x

+2

y

+2

>x

+2

y

+1

2

xy

+2

x

+

y

+2

>

2

xy

+2

x

+

y

+1

Compared to other classical methods for proving termination of rewrite sys-

tems (like recursive path orders and Knuth-Bendix orders), polynomial interpre-

tations are rather weak. Numerous natural examples cannot be handled because

Search WWH ::

Custom Search