The exact hardness of deciding derivational and runtime complexity

TY - GEN

T1 - The exact hardness of deciding derivational and runtime complexity

AU - Schnabl, Andreas

AU - Simonsen, Jakob Grue

N1 - Conference code: 25

PY - 2011

Y1 - 2011

N2 - For any class C of computable total functions satisfying some mild conditions, we prove that the following decision problems are complete for level Σ02 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 Σ02-complete. This places deciding polynomial derivational or runtime complexity of TRSs at the same level in the arithmetical hierarchy 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 Π01-complete. 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 Σ0 3-complete. 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.

AB - For any class C of computable total functions satisfying some mild conditions, we prove that the following decision problems are complete for level Σ02 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 Σ02-complete. This places deciding polynomial derivational or runtime complexity of TRSs at the same level in the arithmetical hierarchy 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 Π01-complete. 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 Σ0 3-complete. 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.

U2 - 10.4230/LIPIcs.CSL.2011.481

DO - 10.4230/LIPIcs.CSL.2011.481

M3 - Article in proceedings

T3 - Leibniz International Proceedings in Informatics

SP - 481

EP - 495

BT - Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL

A2 - Bezem, Marc

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - 25th International Workshop on Computer Science Logic

Y2 - 12 September 2011 through 15 September 2011

ER -