Martin Avanzini ; Georg Moser - Polynomial Path Orders

lmcs:807 - Logical Methods in Computer Science, November 1, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:9)2013
Polynomial Path OrdersArticle

Authors: Martin Avanzini ; Georg Moser

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


    Volume: Volume 9, Issue 4
    Published on: November 1, 2013
    Imported on: October 24, 2012
    Keywords: Computer Science - Logic in Computer Science

    9 Documents citing this article

    Consultation statistics

    This page has been seen 1501 times.
    This article's PDF has been downloaded 258 times.