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 ∗ .
There are several accounts of predicative analysis of recursion in the (ICC) literature. We mention Marion's ( for short) @cite_26 . The path order provides an order-theoretic characterisation of the class @math and can be also consider as a miniaturisation of of sorts: it is a restriction of and yields an order-theoretic characterisation of a complexity class. On the other hand cannot be used to characterise the (innermost) runtime complexity of TRSs. This follows from Example below. In particular, although @math is compatible with @math , from this we can only conclude that @math is computable on a nondeterministic Turing machine in polynomial time. However, this follows by design as @math is complete for @math . For a precedence @math that fulfils @math and @math we obtain that @math is compatible with @math . However it is straightforward to verify that the family of terms @math admits (innermost) derivations whose length grows exponentially in @math . Still the underlying function can be proven polynomial, essentially relying on memoisation techniques @cite_26 .
@cite_26
2072482695
We study termination proofs in order to (i) determine computational complexity of programs and (ii) generate efficient programs from the complexity analysis. For this, we construct a termination ordering, called light multiset path ordering (LMPO), which is a restriction of the multiset path ordering. We establish that the class of first order functional programs on lists which is terminating by LMPO characterises exactly the functions computable in polynomial time.