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.
|Title of host publication||Evolving Computability|
|Subtitle of host publication||11th Conference on Computability in Europe, CiE 2015, Bucharest, Romania, June 29-July 3, 2015. Proceedings|
|Publication status||Published - 2015|
|Name||Lecture Notes in Computer Science|