Information Technology Reference
In-Depth Information
(i.e., there exists an
m ∈
R
such that
f
R
(
x
1
,...,x
n
)
m
for all function symbols
f
and
x
1
,...,x
n
m
). The latter requirement entails that interpretations like
x −
+ 1 cannot be handled.
The remainder of the paper is organized as follows. In Section 3 we discuss
polynomial interpretations with negative constants. Polynomial interpretations
with negative coecients require a different approach, which is detailed in Sec-
tion 4. In Section 5 we discuss briefly how to find suitable polynomial interpreta-
tions automatically and we report on the many experiments that we performed.
1or
x − y
2
Preliminaries
We assume familiarity with the basics of term rewriting [3, 21] and with the
dependency pair method [1] for proving (innermost) termination. In the latter
method a term rewrite system (TRS for short) is transformed into a collection
of ordering constraints of the form
l
r
and
l>r
that need to be solved in
order to conclude termination. Solutions (
,>
)mustbe
reduction pairs
which
consist of a rewrite preorder
(i.e., a transitive and reflexive relation which
is closed under contexts and substitutions) on terms and a compatible well-
founded order
>
which is closed under substitutions. Compatibility means that
the inclusion
· > ⊆ >
or the inclusion
> ·
⊆ >
holds. (Here
·
denotes
relational composition.)
A general semantic construction of reduction pairs, which covers traditional
polynomial interpretations, is based on the concept of algebra. If we equip the
carrier
such
that every interpretation function is weakly monotone in all arguments (i.e.,
f
A
(
A
of an
F
-algebra
A
=(
A, {f
A
}
f∈F
) with a well-founded order
>
x
1
,...,x
n
)
f
A
(
y
1
,...,y
n
) whenever
x
i
y
i
for all 1
i
n
, for every
n
-
ary function symbol
f ∈F
)then(
A
,>
A
) is a reduction pair. Here the relations
A
and
>
A
are defined as follows:
s
A
t
if [
α
]
A
(
s
)
[
α
]
A
(
t
)and
s>
A
t
if
[
α
]
A
(
s
)
>
[
α
]
A
(
t
), for all assignments
α
of elements of
A
to the variables in
s
and
t
([
α
]
A
(
·
) denotes the usual evaluation function associated with the algebra
A
). In general, the relation
>
A
is not closed under contexts,
A
is a preorder
but not a partial order, and
>
A
is not the strict part of
A
. Compatibility holds
because of the identity
A
· >
A
=
>
A
.Wewrite
s
=
A
t
if [
α
]
A
(
s
)=[
α
]
A
(
t
)
for all assignments
α
.Wesaythat
A
isamodelforaTRS
R
if
l
=
A
r
for all
rewrite rules in
.
In this paper we use the following results from [10] concerning dependency
pairs.
R
R
C
Theorem 1.
ATRS
is terminating if for every cycle
in its dependency
graph there exists a reduction pair
(
,>
)
such that
R⊆
,
C⊆
∪ >
,and
C∩>
=
∅
.
Theorem 2.
ATRS
R
is innermost terminating if for every cycle
C
in its in-
nermost dependency graph there exists a reduction pair
(
,>
)
such that
U
(
C
)
⊆
,
C⊆
∪ >
,and
C∩>
=
∅
.
Search WWH ::
Custom Search