Polynomial Path Orders

Martin Avanzini and Georg Moser

Logical Methods in Computer Science 9(4), pp. 1 – 42, 2013.


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*.


  PDF |    doi:10.2168/LMCS-9(4:9)2013  |  © Creative Commons License – NC – ND


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"
Nach oben scrollen