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 ∗ .
Although we consider here only time complexity, related work indicates that the overall approach is general enough to reason also about space complexity. For instance, the order @cite_36 can be miniaturised to characterise linear space @cite_37 . Likewise, @cite_55 provide a semantic technique capable of characterising polynomial space.
@cite_36 @cite_55 @cite_37
1583295953 2033656559 1506380991
Preface 1. Motivating examples 2. Abstract reduction systems 3. Universal algebra 4. Equational problems 5. Termination 6. Confluence 7. Completion 8. Grobner bases and Buchberger's algorithm 9. Combination problems 10. Equational unification 11. Extensions Appendix 1. Ordered sets Appendix 2. A bluffer's guide to ML Bibliography Index. The sup-interpretation method is proposed as a new tool to control memory resources of first order functional programs with pattern matching by static analysis. It has been introduced in order to increase the intensionality, that is the number of captured algorithms, of a previous method, the quasi-interpretations. Basically, a sup-interpretation provides an upper bound on the size of function outputs. A criterion, which can be applied to terminating as well as nonterminating programs, is developed in order to bound the stack frame size polynomially. Since this work is related to quasi-interpretation, dependency pairs, and size-change principle methods, we compare these notions obtaining several results. The first result is that, given any program, we have heuristics for finding a sup-interpretation when we consider polynomials of bounded degree. Another result consists in the characterizations of the sets of functions computable in polynomial time and in polynomial space. A last result consists in applications of sup-interpretations to the dependency pair and the size-change principle methods. We study three different space complexity classes: LINSPACE, PSPACE, and ESPACE and give complete characterisations for these classes. We employ rewrite systems, whose termination can be shown by Knuth Bendix orders. To capture LINSPACE, we consider positively weighted Knuth Bendix orders. To capture PSPACE, we consider unary rewrite systems, compatible with a Knuth Bendix order, where we allow for padding of the input. And to capture ESPACE, we make use of a non-standard generalisation of the Knuth Bendix order.