An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting

Abstract. We define the class of constrained cons-free rewriting systems and show that this class characterizes P, the set of languages decidable in polynomial time on a deterministic Turing machine. The main nov-elty of the characterization is that it allows very liberal properties of term rewriting, in particular non-deterministic evaluation: no reduction strategy is enforced, and systems are allowed to be non-confluent. We present a class of constructor term rewriting systems that character-izes the complexity class P—the set of languages decidable in polynomial time on a deterministic Turing machine. The class is an analogue of similar classes in functional programming that use cons-freeness–the inability of a program to construct new compound data during its evaluation–to characterize a range of complexity classes, including L and P [1, 2], and for higher-order programs PSPACE and hierarchies of exponential space and time classes [3]. The pri-mary novelty is that while previous work has crucially utilized the deterministic evaluation (in particular, call-by-value) and typing disciplines usually found i