On First-order Cons-free Term Rewriting and PTIME

TL;DR

This paper demonstrates that first-order cons-free term rewriting with call-by-value reduction precisely characterizes PTIME, providing an alternative proof for existing linearity-based characterizations of this complexity class.

Contribution

It establishes a new characterization of PTIME using cons-free term rewriting with call-by-value, extending previous linearity-based results.

Findings

Cons-free term rewriting with call-by-value characterizes PTIME.

Provides an alternative proof for linearity-based PTIME characterization.

Strengthens the connection between rewriting systems and computational complexity.

Abstract

In this paper, we prove that (first-order) cons-free term rewriting with a call-by-value reduction strategy exactly characterises the class of PTIME-computable functions. We use this to give an alternative proof of the result by Carvalho and Simonsen which states that cons-free term rewriting with linearity constraints characterises this class.