A New Order-Theoretic Characterisation of the Polytime Computable Functions
>
Programming Languages and Systems - 10th Asian Symposium,
APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings, 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, Path Orders, ICC, Predicative Recursion, TCT