Abstract

We define a new path order <_pop so that for a finite rewrite system R compatible with <_pop, the
complexity or derivation length function Dl_R^f for each function symbol f is guaranteed to be bounded by a polynomial in the length of the inputs. Our results yield a simplification and clarification of the results obtained by Beckmann and Weiermann (Archive for Mathematical Logic, 36:11–30, 1996).

BibTeX

@inproceedings{TAGM-FSTTCS05,
  author      = "Toshiyasu Arai and Georg Moser",
  title       = "Proofs of Termination of Rewrite Systems for Polytime
                 Functions",
  booktitle   = "Proceedings of the 25th International Conference on
                 Foundations of Software Technology and Theoretical
                 Computer Science",
  series      = "Lecture Notes in Computer Science",
  volume      = 3821,
  pages       = "529--540",
  publisher   = "Springer-Verlag",
  year        = 2005
}