Polynomial Path Orders
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*.
Cite
@article{arxiv.1309.2394,
title = {Polynomial Path Orders},
author = {Martin Avanzini and Georg Moser},
journal= {arXiv preprint arXiv:1309.2394},
year = {2015}
}
Comments
LMCS version. This article supersedes arXiv:1209.3793