On the Computational Content of Termination Proofs

Georg Moser and Thomas Powell

Proceedings of the 11th Conference on Computability in Europe (CiE 2015), Lecture Notes in Computer Science 9136, pp. 276 – 285, 2015.


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.


  PDF |    doi:10.1007/978-3-319-20028-6_28  |  © Springer International Publishing Switzerland


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"
Nach oben scrollen