TY - GEN
T1 - On the computational content of termination proofs
AU - Moser, Georg
AU - Powell, Thomas
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-319-20028-6_28
DO - 10.1007/978-3-319-20028-6_28
M3 - Chapter in a published conference proceeding
T3 - Lecture Notes in Computer Science
SP - 276
EP - 285
BT - Evolving Computability
ER -