Information Technology Reference
In-Depth Information
Table 3.
Negative coecients.
termination
innermost termination
interpretation
e
n
ne
e
n
ne
success
109
102
114
181
161
185
0.74
0.39
0.58
0.04
0.06
0.07
failure
71
96
66
30
62
28
2.50
0.71
2.48
1.72
0.33
2.00
ti
eo t
39
21
39
28
16
26
total time
1428.41 738.16 1400.60
899.01 511.14
848.25
very few additional examples can be han-
dled. For termination the only difference is [2, Example 3.18] which contains a
unary function double that requires 2
By using coecients from
{
0
,
1
,
2
}
x
as interpretation. The effect of allowing
1 as constant is more apparent. Taking default natural interpretations for cer-
tain common function symbols reduces the execution time considerably but also
reduces the termination proving power. However, the
columns clearly show
that fixing natural interpretations initially but allowing different interpretations
later is a very useful idea.
In Table 3 we use the negative coecient method developed in Section 4.
Not surprisingly, this method is more suited for proving innermost termination
because the method is incompatible with the recent modular refinements of the
dependency pair method when proving termination (for non-overlapping TRSs).
Comparing the first (last) three columns in Table 3 with the last three
columns in Table 1 (Table 2) one might be tempted to conclude that the approach
developed in Section 4 is useless in practice. We note however that several chal-
lenging examples can only be handled by polynomial interpretations with nega-
tive coecients. We mention TRSs that are (innermost) terminating because of
non-linearity (e.g. [2, Examples 3.46, 4.12, 4.25]) and TRSs that are terminating
because the difference of certain arguments decreases (e.g. [2, Example 4.30]).
ne
References
1. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. The-
oretical Computer Science , 236:133-178, 2000.
2. T. Arts and J. Giesl. A collection of examples for termination of term rewriting
using dependency pairs. Technical Report AIB-2001-09, RWTH Aachen, 2001.
3. F. Baader and T. Nipkow. Term Rewriting and All That . Cambridge University
Press, 1998.
4. A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial
interpretations and its implementation. Science of Computer Programming , 9:137-
159, 1987.
Search WWH ::




Custom Search