This paper is concerned with the complexity analysis of constructor term rewrite systems and its ramification in implicit computational complexity. We introduce a path order with multiset status, the polynomial path order POP ∗ , that is applicable in two related, but distinct contexts. On the one hand POP ∗ induces polynomial innermost runtime complexity and hence may serve as a syntactic, and fully automatable, method to analyse the innermost runtime complexity of term rewrite systems. On the other hand POP ∗ provides an order-theoretic characterisation of the polytime computable functions: the polytime computable functions are exactly the functions computable by an orthogonal constructor TRS compatible with POP ∗ .
Furthermore, a strengthening of our first main theorem to runtime complexity can be obtained if one considers polynomial interpretations, where the interpretations of constructor symbols is restricted. Such restricted polynomial interpretations are called in @cite_27 . Note that additive polynomial interpretations also characterise the functions computable in polytime @cite_27 . Similarly, @cite_47 provide an elegant way to characterise time complexity classes through a combination of syntactic (via restrictions of reduction orders) and semantic (via quasi-interpretations) considerations. To date it is unknown whether quasi-interpretations can be used to assess polynomial runtime complexity of TRSs. Unarguable these semantic techniques admit a better intensionality than the syntactic characterisation provided through the path order . But semantic methods are notoriously difficult to implement efficiently in an automated setting. In particular we are only aware of one accessible implementation of quasi-interpretations, our own @cite_15 . Note that these semantic methods are not tailored for innermost rewriting, in particular Example given below cannot be handled, while it can be easily handled by .
@cite_27 @cite_47 @cite_15
2055717180 2025130727 86123047
We study the effect of polynomial interpretation termination proofs of deterministic (resp. non-deterministic) algorithms defined by con uent (resp. non-con uent) rewrite systems over data structures which include strings, lists and trees, and we classify them according to the interpretations of the constructors. This leads to the definition of six function classes which turn out to be exactly the deterministic (resp. non-deterministic) polynomial time, linear exponential time and linear doubly exponential time computable functions when the class is based on con uent (resp. non-con uent) rewrite systems. We also obtain a characterisation of the linear space computable functions. Finally, we demonstrate that functions with exponential interpretation termination proofs are super-elementary. This paper presents in a reasoned way our works on resource analysis by quasi-interpretations. The controlled resources are typically the runtime, the runspace or the size of a result in a program execution. Quasi-interpretations allow the analysis of system complexity. A quasi-interpretation is a numerical assignment, which provides an upper bound on computed functions and which is compatible with the program operational semantics. The quasi-interpretation method offers several advantages: (i) It provides hints in order to optimize an execution, (ii) it gives resource certificates, and (iii) finding quasi-interpretations is decidable for a broad class which is relevant for feasible computations. By combining the quasi-interpretation method with termination tools (here term orderings), we obtained several characterizations of complexity classes starting from Ptime and Pspace. Recent studies have provided many characterisations of the class of polynomial time computable functions through term rewriting techniques. In this paper we describe a (fully automatic and command-line based) system that implements the majority of these techniques and present experimental findings to simplify comparisons.