License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2011.481
URN: urn:nbn:de:0030-drops-32516
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3251/
Go to the corresponding LIPIcs Volume Portal

Schnabl, Andreas ; Simonsen, Jakob Grue

The Exact Hardness of Deciding Derivational and Runtime Complexity

pdf-format:
38.pdf (0.6 MB)

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 ierarchy. 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.

All of our results are easily extended to the notion of minimal complexity (where the length of shortest reductions to normal form is considered) and remain valid under any computable reduction strategy. Finally, all results hold both for unrestricted TRSs and for the class of orthogonal TRSs.

BibTeX - Entry

@InProceedings{schnabl_et_al:LIPIcs:2011:3251,
  author =	{Andreas Schnabl and Jakob Grue Simonsen},
  title =	{{The Exact Hardness of Deciding Derivational and Runtime Complexity}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{481--495},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Marc Bezem},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3251},
  URN =		{urn:nbn:de:0030-drops-32516},
  doi =		{10.4230/LIPIcs.CSL.2011.481},
  annote =	{Keywords: term rewriting, derivational complexity, arithmetical hierarchy}
}

Keywords: term rewriting, derivational complexity, arithmetical hierarchy
Collection: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
Issue Date: 2011
Date of publication: 31.08.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI