Complexity hierarchies and higher-order cons-free rewriting

DOI10.4230/LIPICS.FSCD.2016.23zbMATH Open1387.68145arXiv1604.08936OpenAlexW2963786708MaRDI QIDQ5369488FDOQ5369488

Authors: Cynthia Kop, Jakob Grue Simonsen 

Publication date: 17 October 2017

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 $geq$ 1, left-linear cons-free systems with type order k characterize E${}^k$TIME 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 = E${}^1$TIME $subseteq$ E${}^2$TIME $subseteq$ .... Our work confirms prior results that having full non-determinism (via overlaps of rules) does not directly allow 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.

Full work available at URL: https://arxiv.org/abs/1604.08936

Recommendations

• Complexity hierarchies and higher-order cons-free term rewriting
• The power of non-determinism in higher-order implicit complexity. Characterising complexity classes using non-deterministic cons-free programming
• An implicit characterization of the polynomial-time decidable sets by cons-free rewriting
• Implementing first-order rewriting with constructor systems
• The expressive power of higher-order types or, life without CONS

zbMATH Keywords

implicit complexityhigher-order term rewritingcons-freenessETIME hierarchy

Mathematics Subject Classification ID

Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Grammars and rewriting systems (68Q42)

Cited In (5)

• Complexity hierarchies and higher-order cons-free term rewriting
• Higher order interpretation for higher order complexity
• The power of non-determinism in higher-order implicit complexity. Characterising complexity classes using non-deterministic cons-free programming
• Term rewriting characterisation of LOGSPACE for finite and infinite data
• An implicit characterization of the polynomial-time decidable sets by cons-free rewriting

This page was built for publication: Complexity hierarchies and higher-order cons-free rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5369488)