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