home > publications > AEM:TCS:15

A new Order-theoretic Characterisation of the Polytime Computable Functions

A new Order-theoretic Characterisation of the Polytime Computable Functions
M. Avanzini and N. Eguchi and G. Moser
Theoretical Computer Science 585:3–24, 2015.

Abstract

We propose a new order-theoretic characterisation of the class of polytime computable functions. To this avail we define the small polynomial path order (sPOP* for short). This termination order entails a new syntactic method to analyse the innermost runtime complexity of term rewrite systems fully automatically: for any rewrite system compatible with sPOP* that employs recursion up to depth d, the (innermost) runtime complexity is polynomially bounded of degree d. This bound is tight. Thus we obtain a direct correspondence between a syntactic (and easily verifiable) condition of a program and the asymptotic worst-case complexity of the program.

Categories

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