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

ABSTRACT. A constructor rewriting system $R$ is said to characterize a language $D \subseteq \{ 0, 1 \}^\{< \infty}$ if there are designated function symbols $f_0$ and $\mathrm{true}$ such that for every constructor term $s$ that represents a string $\mathtt{s} \in \{0,1\}^{< \infty}$, we have $f_0(s) \rightarrow^* \mathrm{true}$ iff $\mathtt{s} \in D$. A class $\mathfrak{R}$ of rewriting systems is said to characterize a class $\mathfrak{D}$ of languages if every language in $\mathfrak{D}$ is characterized by a system in $\mathfrak{R}$ and every element of $\mathfrak{R}$ characterizes a language in $\mathfrak{D}$. We define the class of \emph{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 novelty 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.