Automation of Polynomial Path Orders

Automation of Polynomial Path Orders
M. Avanzini
Masters thesis, University of Innsbruck, 2009.


The automated complexity analysis of rewrite systems is a challenging topic that has recently gained much attention. As one practical application, techniques developed for the analysis of rewrite systems can in principle be employed for the automated analysis of functional programs. In this thesis, we present the polynomial path order, a syntactic restriction of the well known multi-set path order. The order is carefully crafted to induce polynomial bounds on the runtime-complexity of compatible rewrite systems. Semantic labeling and the dependency pair method are two prominent transformation techniques developed in the context of termination analysis. Both significantly strengthen the power of basic termination techniques. We show that suitable adaptations as proposed in the literature can be employed together with the polynomial path order for a complexity analysis. This severely widens the applicability of the polynomial path order. Furthermore, we give an efficient automation that works by a reduction to the Boolean satisfiability problem (SAT). Experimental results confirm the feasibility of our approach.


Term Rewriting, Complexity Analysis, Runtime Complexity Analysis, Path Orders, ICC, Predicative Recursion, Automation