Polynomial path orders

DOI10.2168/LMCS-9(4:9)2013MaRDI QIDQ2865062zbMATH OpenOpenAlexFDO

Authors Martin Avanzini, Georg Moser

Publication date 28 November 2013

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1309.2394

zbMATH Keywords

implicit computational complexityautomationterm rewritingcomplexity analysis

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42)

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

Recommendations

• A new order-theoretic characterisation of the polytime computable functions
• Dependency Pairs and Polynomial Path Orders
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Complexity Analysis by Rewriting
• A lexicographic path order with slow growing derivation bounds

Cited in

(16)

• Query order in the polynomial hierarchy
• Analysing the implicit complexity of programs.
• A lexicographic path order with slow growing derivation bounds
• A path order for rewrite systems that compute exponential time functions
• A combination framework for complexity
• Complexity of conditional term rewriting
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Generating polynomial orderings
• Complexity hierarchies and higher-order cons-free term rewriting
• Dependency Pairs and Polynomial Path Orders
• Complexity Analysis by Rewriting
• A new order-theoretic characterisation of the polytime computable functions
• Polymorphic higher-order recursive path orderings
• On basic feasible functionals and the interpretation method
• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• Automated Implicit Computational Complexity Analysis (System Description)

Describes a project that uses

Uses Software

• MiniSat
• SPEED

This page was built for publication: Polynomial path orders

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2865062)