Abstract

In this paper, we present a variant of the dependency pair method for
analysing runtime complexities of term rewrite systems automatically.
This method is easy to implement, but significantly extends
the analytic power of existing direct methods.
Our findings extend the class of TRSs
whose linear or quadratic runtime complexity can be detected automatically.
We provide ample numerical data for assessing the viability of the method.

BibTeX

@inproceedings{NHGM-IJCAR08,
  author      = "Nao Hirokawa and Georg Moser",
  title       = "Automated Complexity Analysis Based on the Dependency
                 Pair Method",
  booktitle   = "Proceedings of the 4th International Joint Conference on
                 Automated Reasoning",
  series      = "Lecture Notes in Artificial Intelligence",
  volume      = 5195,
  pages       = "364--380",
  publisher   = "Springer-Verlag",
  year        = 2008
}

Erratum

Unfortunately the conference paper contains a bug. As stated Theorem 23 is not valid as the condition that TRS S is non-duplicating
is missing. The mistake happens in the seemingly trivial Lemma 22, where also
non-duplication of S needs to be assumed.

We are grateful to Dieter Hofbauer and Andreas Schnabl who compiled a counter-example that shows
the need for the additional restriction. Consider the TRSs R = { f(s(x),y) → f(x,d(y,y,y) }
and S = { d(0,0,x) → x, d(s(x),s(y),z) → d(x,y,s(z)) }. Then Theorem 23 would be applicable and wrongly concludes
linear runtime complexity for the combined system, while the combined system actually has at least
exponential runtime complexity. By introducing the assumption ‘non-duplication of S’ the results in
Section 5 can be re-established.