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