Abstract

Given that a program has been shown to terminate using a particular proof, it is natural to ask what we can infer about its complexity. In this paper we outline a new approach to tackling this question in the context of term rewrite systems and recursive path orders. From an inductive proof that recursive path orders are well-founded, we extract an explicit realiser which bounds the derivational complexity of rewrite systems compatible with these orders. We demonstrate that by analysing our realiser we are able to derive, in a completely uniform manner, a number of results on the relationship between the strength of path orders and the bounds they induce on complexity.

BibTeX

@inproceedings{GMTP15,
  author    = "Georg Moser and Thomas Powell",
  title     = "On the Computational Content of Termination Proofs",
  booktitle = "Proceedings of the 11th Conference on Computability in
               Europe (CiE 2015)",
  year      = 2015,
  editor    = "Arnold Beckmann and Victor Mitrana and Mariya Ivanova
               Soskova",  
  series    = "Lecture Notes in Computer Science",
  volume    = 9136,
  pages     = "276--285",
  doi       = "10.1007/978-3-319-20028-6_28"
}