Complexity hierarchies and higher-order cons-free rewriting

TY - GEN

T1 - Complexity hierarchies and higher-order cons-free rewriting

AU - Kop, Cynthia Louisa Martina

AU - Simonsen, Jakob Grue

N1 - Conference code: 1

PY - 2016/6/1

Y1 - 2016/6/1

N2 - Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the righthand 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 EkTIME 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 = E1TIME ⊈ E2TIME ⊈ ⋯. 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.

AB - Constructor rewriting systems are said to be cons-free if, roughly, constructor terms in the righthand 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 EkTIME 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 = E1TIME ⊈ E2TIME ⊈ ⋯. 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.

U2 - 10.4230/LIPIcs.FSCD.2016.23

DO - 10.4230/LIPIcs.FSCD.2016.23

M3 - Article in proceedings

SN - 978-3-95977-010-1

T3 - Leibniz International Proceedings in Informatics

BT - 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

A2 - Kesner, Delia

A2 - Pientka, Brigitte

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

T2 - International Conference on Formal Structures for Computation and Deduction 2016

Y2 - 22 June 2016 through 26 June 2016

ER -