Polynomial Path Orders

Polynomial Path Orders
M. Avanzini and G. Moser
Logical Methods in Computer Science 9 (4), 2013.


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*.


Term Rewriting, Complexity Analysis, ICC, Automation, Path Orders, Predicative Recursion