Information Technology Reference
1428.41 738.16 1400.60
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
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]).
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
4. A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial
interpretations and its implementation. Science of Computer Programming , 9:137-