Abstract

This paper is concerned with the complexity analysis of constructor term rewrite systems and its ramification in implicit computational complexity. We introduce a path order with multiset status, the “polynomial path order” POP*, that is applicable in two related, but distinct contexts. On the one hand POP* induces polynomial innermost runtime complexity and hence may serve as a syntactic, and fully automatable, method to analyse the innermost runtime complexity of term rewrite systems. On the other hand POP* provides an order-theoretic characterisation of the polytime computable functions: the polytime computable functions are exactly the functions computable by an orthogonal constructor TRS compatible with POP*.

BibTeX

@article{MAGM-LMCS13,
  author  = "Martin Avanzini and Georg Moser",
  title   = "Polynomial Path Orders",
  journal = "Logical Methods in Computer Science",
  volume  = 9,
  number  = 4,
  pages   = "1--42",
  year    = 2013,
  doi     = "10.2168/LMCS-9(4:9)2013"
}