Polynomial Path Orders

This paper is concerned with the complexity analysis of constructor termrewrite systems and its ramification in implicit computational complexity. Weintroduce 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 asyntactic, and fully automatable, method to analyse the innermost runtimecomplexity of term rewrite systems. On the other hand POP* provides anorder-theoretic characterisation of the polytime computable functions: thepolytime computable functions are exactly the functions computable by anorthogonal constructor TRS compatible with POP*.Comment: LMCS version. This article supersedes arXiv:1209.379