Abstract

For any class C of computable total functions satisfying some mild conditions, we prove that the following decision problems are complete for the existential part of the second level of the arithmetical hierarchy: (A) Deciding whether a term rewriting system (TRS for short) has runtime complexity bounded by a function in C. (B) Deciding whether a TRS has derivational complexity bounded by a function in C.

In particular, the problems of deciding whether a TRS has polynomially (exponentially) bounded runtime complexity (respectively derivational complexity) are complete for this level of the arithmetical hierarchy. This places deciding polynomial derivational or runtime complexity of TRSs at the same level as deciding nontermination or nonconfluence of TRSs. We proceed to show that the related problem of deciding for a single computable function f whether a TRS has runtime complexity bounded from above by f is complete for the universal part of the first level of the arithmetical hierarchy. We further prove that analysing the implicit complexity of TRSs is even more difficult: The problem of deciding whether a TRS accepts a language of terms accepted by some TRS with runtime complexity bounded by a function in C is complete for the existential part of the third level of the arithmetical hierarchy.

BibTeX

@inproceedings{ASJGS-CSL11,
  author    = "Andreas Schnabl and Jakob Grue Simonsen",
  title     = "The Exact Hardness of Deciding Derivational and Runtime
               Complexity",
  booktitle = "Proceedings of the 25th International Workshop on Computer
               Science Logic / 20th Annual Conference of the EACSL",
  series    = "Leibniz International Proceedings in Informatics",
  volume    = 12,
  pages     = "481--495",
  year      = 2011
}