home > publications > AEM:APLAS:12

A New Order-Theoretic Characterisation of the Polytime Computable Functions

A New Order-Theoretic Characterisation of the Polytime Computable
Functions
Martin Avanzini, Naohi Eguchi and Georg Moser
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

, , , , ,