cl-banner

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.

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.

 

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

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