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