Complexity Classes and Rewrite Systems With Polynomial Interpretation

We are concerned with functions over words which are computable by means of a rewrite system admitting polynomial interpretation termination proofs. We classify them according to the interpretations of successor symbols. This leads to the definition of three classes, which turn out to be exactly the poly-time, linear exponential-time and doubly linear exponential time computable functions. As a consequence, we also characterize linear space computable. 1 Introduction We are interested in studying the relationship between termination orderings for rewrite systems and feasible computation. One might suspect that polynomial interpretations, introduced in [9], would be a good candidate for the investigation of small complexity classes of functions. Various implementations have been carried out [2, 6]. However, [8] have shown that any rewrite system with a polynomial interpretation termination proof admits doubly-exponential derivations. The work of [3] initiated an alternative analysis of..