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.

BibTeX

@article{MANGEM15,
  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"
}