Information Technology Reference
In-Depth Information
3
Negative Constants
3.1
Theoretical Framework
When using polynomial interpretations with negative constants like in the ex-
ample of the introduction, the first challenge we face is that the standard order
>
Z
N
on
is not well-founded. Restricting the domain to the set
of natural
numbers makes an interpretation like p Z (
1 ill-defined. Dershowitz and
Hoot observe in [8] that if all (instantiated) subterms in the rules of the TRS
are interpreted as non-negative integers, such interpretations can work correctly.
Following their observation, we propose to modify the interpretation of p to
p N (
x
)=
x −
x
)=max
{
0
,x−
1
}
.
Definition 3. Let
F
beasignatureandlet (
Z , {f Z } f∈F ) be an
F
-algebra such
f Z is weakly monotone in all its arguments.
The interpretation functions of the induced algebra (
that every interpretation function
N , {f N } f∈F ) are defined as
follows:
f N (
x 1 ,...,x n )=max
{
0
,f Z (
x 1 ,...,x n )
}
for all
x 1 ,...,x n N
.
With respect to the interpretations in the introduction we obtain s N ( p N (
x
)) =
max
{
0
,
max
{
0
,x−
1
}
+1
}
=max
{
0
,x−
1
}
+1, p N ( 0 N )=max
{
0
,
0
}
=0,and
p N ( s N (
x
)) = max
{
0
,
max
{
0
,x
+1
}−
1
}
=
x
.
Lemma 4. If (
Z , {f Z } f∈F ) is an
F
-algebra with weakly monotone interpreta-
tions then (
N ,> N ) is a reduction pair.
Proof. It is easy to show that the interpretation functions of the induced alge-
bra are weakly monotone in all arguments. Routine arguments reveal that the
relation
> N is a well-founded order which is closed under substitutions and that
N is a preorder closed under contexts and substitutions. Moreover, the identity
> N · N =
> N holds. Hence (
N ,> N ) is a reduction pair.
It is interesting to remark that unlike usual polynomial interpretations, the
relation
> N does not have the (weak) subterm property. For instance, with re-
spect to the interpretations in the example of the introduction, we have s ( 0 )
> N
p ( s ( 0 )) and not p ( s ( 0 ))
> N p ( 0 ).
In recent modular refinements of the dependency pair method [23, 13, 22]
suitable reduction pairs (
,>
) have to satisfy the additional property of
C E -
compatibility :
must orient the rules of the TRS
C E
consisting of the two
rewrite rules cons (
,where cons is a fresh func-
tion symbol, from left to right. This is not a problem because we can simply
define cons N (
x, y
)
→ x
and cons (
x, y
)
→ y
x, y
)=max
{x, y}
. In this way we obtain a reduction pair (
,
)
on terms over the original signature extended with cons such that
∪C E
and
> ⊆
.
Example 5. Consider the TRS consisting of the following rewrite rules:
half ( 0 )
0
bits ( 0 )
0
1:
4:
2:
half ( s ( 0 ))
0
5:
bits ( s (
x
))
s ( bits ( half ( s (
x
))))
3:
half ( s ( s (
x
)))
s ( half (
x
))
Search WWH ::




Custom Search