Information Technology Reference

In-Depth Information

4

Negative Coecients

Let us start with an example which shows that negative coecients in polynomial

interpretations can be useful.

Example 10.
Consider the following variation of a TRS in [2]:

1:

0

x →

true

7:

x −

0

→ x

2:

s
(

x

)

0

→

false

8:

s
(

x

)

−

s
(

y

)

→ x − y

3:

s
(

x

)

s
(

y

)

→ x
y

9:
if
(
true

,x,y

)

→ x

4:

mod
(
0

,

s
(

y

))

→

0

10:
if
(
false

,x,y

)

→ y

5:

mod
(
s
(

x

)

,

0
)

→

0

6:
mod
(
s
(

x

)

,

s
(

y

))

→

if
(

y
x,

mod
(
s
(

x

)

−

s
(

y

)

,

s
(

y

))

,

s
(

x

))

There are 6 dependency pairs:

s
(

→ x
y

11:

s
(

x

)

y

)

−
s
(

→ x −
y

12:

s
(

x

)

y

)

13:
mod
(
s
(

if
(

x

)

,

s
(

y

))

→

y
x,

mod
(
s
(

x

)

−

s
(

y

)

,

s
(

y

))

,

s
(

x

))

14:
mod
(
s
(

→ y
x

x

)

,

s
(

y

))

15:
mod
(
s
(

mod
(
s
(

x

)

,

s
(

y

))

→

x

)

−

s
(

y

)

,

s
(

y

))

16:
mod
(
s
(

−
s
(

x

)

,

s
(

y

))

→

s
(

x

)

y

)

Since the TRS is non-overlapping, it is sucient to prove innermost termination.

The problematic cycle in the (innermost) dependency graph is

C

=

{

15

}

.The

usable rewrite rules for this cycle are

U

(

C

)=

{

7

,

8

}

. We need to find a reduction

pair (

,>

) such that rules 4 and 5 are weakly decreasing (i.e., compatible with

)

and dependency pair 15 is strictly decreasing (with respect to

>

). The only way

to achieve the latter is by using the observation that
s
(

x

) is semantically greater

than the syntactically larger term
s
(

x

)

−

s
(

y

). If we take the natural interpretation

1, and
0
Z
= 0, together with
mod
Z

−
Z
(

x, y

x − y

,
s
Z
(

x

x −

x, y

x

)=

)=

(

)=

then

we obtain the following ordering constraints over the natural numbers:

7:

x
x

8: max

{

0

,x− y}

max

{

0

,x− y}

15:

x

+1

>

max

{

0

,x− y}

4.1

Theoretical Framework

The constraints in the above example are obviously satisfied, but are we allowed

to use an interpretation like

in (innermost) termination proofs?

The answer appears to be negative because Lemma 4 no longer holds. Because

the induced interpretation

−
Z
(

x, y

)=

x−y

−
N
(

x, y

)=max

{

0

,x− y}

is not weakly monotone in

its second argument, the order

N
of the induced algebra is not closed under

contexts, so if

s
N
t

then it may happen that

C

[

s

]

N
C

[

t

]. Consequently,

we do not obtain a reduction pair. However, if we have

s

=
N
t

rather than

Search WWH ::

Custom Search