Polynomial path orders

DOI10.2168/LMCS-9(4:9)2013zbMATH Open1314.68170arXiv1309.2394OpenAlexW2053054452MaRDI QIDQ2865062FDOQ2865062

Authors: Martin Avanzini, Georg Moser 

Publication date: 28 November 2013

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

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

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

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

zbMATH Keywords

implicit computational complexityautomationterm rewritingcomplexity analysis

Mathematics Subject Classification ID

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

Cited In (15)

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

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)