Complexity Analysis by Rewriting
>
Functional and Logic Programming, 9th International Symposium,
FLOPS 2008, Ise, Japan, April 14-16, 2008. Proceedings, volume 4989 of Lecture Notes in Computer Science, pages 130–146, (2008).
Abstract
In this paper we introduce a restrictive version of the multiset path order, called polynomial path order. This recursive path order induces polynomial bounds on the maximal number of innermost rewrite steps. This result opens the way to automatically verify for a given program, written in an eager functional programming language, that the maximal number of evaluation steps starting from any function call is polynomial in the input size. To test the feasibility of our approach we have implemented this technique and compare its applicability to existing methods.
Categories
Term Rewriting, Complexity Analysis, Runtime Complexity Analysis, Path Orders, ICC