Polynomial Path Orders

TL;DR

This paper introduces the polynomial path order POP* for analyzing the complexity of term rewrite systems, enabling automatic complexity analysis and characterizing polytime computable functions.

Contribution

It presents POP*, a novel path order that ensures polynomial runtime complexity and characterizes polytime functions in term rewriting systems.

Findings

POP* induces polynomial innermost runtime complexity.

POP* characterizes exactly the polytime computable functions.

The method is automatable for analyzing term rewrite systems.

Abstract

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