Complexity Hierarchies and Higher-Order Cons-Free Rewriting

TL;DR

This paper explores how higher-order cons-free rewriting systems characterize exponential time complexity classes, revealing the impact of non-determinism and syntactic restrictions on computational power.

Contribution

It extends the characterization of complexity classes to higher-order, non-orthogonal rewriting systems, establishing a hierarchy of complexity classes based on type order.

Findings

Cons-free higher-order rewriting characterizes E^kTIME for each k ≥ 1.

Non-determinism via rule overlaps does not characterize non-deterministic classes like NE.

Minor syntactic changes significantly affect the complexity classes characterized.

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.