Avanzini, Martin and Moser, Georg - Polynomial Path Orders

lmcs:807 - Logical Methods in Computer Science, November 1, 2013, Volume 9, Issue 4
Polynomial Path Orders

Authors: Avanzini, Martin and Moser, Georg

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


Source : oai:arXiv.org:1309.2394
DOI : 10.2168/LMCS-9(4:9)2013
Volume: Volume 9, Issue 4
Published on: November 1, 2013
Submitted on: October 24, 2012
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 89 times.
This article's PDF has been downloaded 18 times.