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
Proceedings of the 10th Asian Symposium on Programming Languages and Systems, volume 7705 of Lecture Notes in Computer Science, pages 280–295, 2012.

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 upto depth d, the (innermost) runtime complexity is polynomially bounded of degree d. This bound is tight.

Categories

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