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.

BibTeX

@inproceedings{MAGM-FLOPS08,
  author      = "Martin Avanzini and Georg Moser",
  title       = "Complexity Analysis by Rewriting",
  booktitle   = "Proceedings of the 9th International Symposium on
                 Functional and Logic Programming",
  series      = "Lecture Notes in Computer Science",
  volume      = 4989,
  publisher   = "Springer-Verlag",
  year        = 2008,
  pages       = "130--146"
}