2026-07-21T19:26:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5997 2024-03-06T10:37:26Z ddc:004 open_access

Complexity Hierarchies and Higher-Order Cons-Free Rewriting Kop, Cynthia Grue Simonsen, Jakob higher-order term rewriting implicit complexity cons-freeness ETIME hierarchy 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Cynthia Kop and Jakob Grue Simonsen 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.23 urn:nbn:de:0030-drops-59972 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.23 eng https://creativecommons.org/licenses/by/3.0/legalcode