Search Results

Documents authored by Grue Simonsen, Jakob


Document
Complexity Hierarchies and Higher-Order Cons-Free Rewriting

Authors: Cynthia Kop and Jakob Grue Simonsen

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)


Abstract
Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the right-hand sides of rules are subterms of constructor terms in the left-hand side; the computational intuition is that rules cannot build new data structures. It is well-known that cons-free programming languages can be used to characterize computational complexity classes, and that cons-free first-order term rewriting can be used to characterize the set of polynomial-time decidable sets. We investigate cons-free higher-order term rewriting systems, the complexity classes they characterize, and how these depend on the order of the types used in the systems. We prove that, for every k >= 1, left-linear cons-free systems with type order k characterize E^kTIME if arbitrary evaluation is used (i.e., the system does not have a fixed reduction strategy). The main difference with prior work in implicit complexity is that (i) our results hold for non-orthogonal term rewriting systems with possible rule overlaps with no assumptions about reduction strategy, (ii) results for such term rewriting systems have previously only been obtained for k = 1, and with additional syntactic restrictions on top of cons-freeness and left-linearity. Our results are apparently among the first implicit characterizations of the hierarchy E^1TIME != E^2TIME != .... Our work confirms prior results that having full non-determinism (via overlaps of rules) does not directly allow for characterization of non-deterministic complexity classes like NE. We also show that non-determinism makes the classes characterized highly sensitive to minor syntactic changes such as admitting product types or non-left-linear rules.

Cite as

Cynthia Kop and Jakob Grue Simonsen. Complexity Hierarchies and Higher-Order Cons-Free Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


Copy BibTex To Clipboard

@InProceedings{kop_et_al:LIPIcs.FSCD.2016.23,
  author =	{Kop, Cynthia and Grue Simonsen, Jakob},
  title =	{{Complexity Hierarchies and Higher-Order Cons-Free Rewriting}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.23},
  URN =		{urn:nbn:de:0030-drops-59972},
  doi =		{10.4230/LIPIcs.FSCD.2016.23},
  annote =	{Keywords: higher-order term rewriting, implicit complexity, cons-freeness, ETIME hierarchy}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail