A New Order-Theoretic Characterisation of the Polytime Computable Functions

Martin Avanzini, Naohi Eguchi, and Georg Moser

Theoretical Computer Science 585, pp. 3 – 24, 2015.


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.


  PDF |    doi:10.1016/j.tcs.2015.03.003  |  © Creative Commons License – CC   BY


author = "Martin Avanzini and Naohi Eguchi and Georg Moser",
title = "A New Order-Theoretic Characterisation of the Polytime Computable Functions",
journal = "Theoretical Computer Science",
volume = 585,
pages = "3--24",
year = 2015,
doi = "10.1016/j.tcs.2015.03.003"
Nach oben scrollen