Information Technology Reference
In-Depth Information
of the strict monotonicity requirement which precludes interpretations like
+1
for binary function symbols. In connection with the dependency pair method
of Arts and Giesl [1], polynomial interpretations become much more useful be-
cause strict monotonicity is no longer required; weak monotonicity is sucient
and hence
x
+ 1 or even 0 as interpretation of a binary function symbol causes
no problems. Monotonicity is typically guaranteed by demanding that all coef-
ficients are positive.
In this paper we go a step further. We show that polynomial interpretations
over the integers with negative coecients like
x
x −
x − y
+1 can also
be used for termination proofs. To make the discussion more concrete, let us
consider a somewhat artificial example: the recursive definition
1and
f
x
x>
f
f
x −
(
)=if
0then
(
(
1)) + 1 else 0
from [8]. It computes the identity function over the natural numbers. Termina-
tion of the rewrite system
1:
f
(
s
(
x
))
→
s
(
f
(
f
(
p
(
s
(
x
)))))
2 :
f
(
0
)
→
0
3:
p
(
s
(
x
))
→ x
obtained after the obvious translation is not easily proved. The (manual) proof in
[8] relies on forward closures whereas powerful automatic tools like
AProVE
[11]
and
CiME
[5] that incorporate both polynomial interpretations and the depen-
dency pair method fail to prove termination. There are three dependency pairs
(here
f
and
p
are new function symbols):
4:
f
(
s
(
f
(
f
(
p
(
s
(
5 :
f
(
s
(
f
(
p
(
s
(
6 :
f
(
s
(
p
(
s
(
x
))
→
x
))))
x
))
→
x
)))
x
))
→
x
))
By taking the
natural
polynomial interpretation
)=
f
Z
)=
p
Z
f
Z
(
x
(
x
)=
x
s
Z
(
x
)=
x
+1
0
Z
=0
p
Z
(
x
(
x
)=
x −
1
over the integers, the rule and dependency pair constraints reduce to the follow-
ing inequalities:
1:
x
+1
x
+1
3:
x
x
5:
x
+1
>x
2:
0
0
4 :
x
+1
>x
6:
x
+1
>x
These constraints are obviously satisfied. The question is whether we are al-
lowed to conclude termination at this point. We will argue that the answer is
armative and, moreover, that the search for appropriate natural polynomial
interpretations can be eciently implemented.
The approach described in this paper is inspired by the combination of the
general path order and forward closures [8] as well as semantic labelling [24].
Concerning related work, Lucas [17, 18] considers polynomials with
real
coef-
ficients for automatically proving termination of (context-sensitive) rewriting
systems. He solves the problem of well-foundedness by replacing the standard
order on
.
In addition, he demands that interpretations are uniformly bounded from below
R
with
>
δ
for some fixed positive
δ ∈
R
:
x>
δ
y
if and only if
x−y
δ
Search WWH ::
Custom Search