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.

BibTeX

@inproceedings{MANEGM-APLAS12,
  author    = "Martin Avanzini and Naohi Eguchi and Georg Moser",
  title     = "New Order-theoretic Characterisation of the Polytime
               Computable Functions",
  booktitle = "Proceedings of the 10th Asian Symposium Programming
               Languages and Systems",
  series    = "Lecture Notes in Computer Science (Programming Languages
               and Systems)",
  number    = 7705,
  pages     = "280--295",
  publisher = "Springer-Verlag",
  year      = 2012
}