Title: A proof theoretic study of abstract termination principles,
Abstract: We define a variety of abstract termination principles which form
generalisations of simplification orders, and investigate their computational
content. Simplification orders, which include the well-known multiset and
lexicographic path orderings, are important techniques for proving that
computer programs terminate. Moreover, an analysis of the proofs that these
orders are wellfounded can yield additional quantitative information: namely an
upper bound on the complexity of programs reducing under these orders. In this
paper we focus on extracting computational content from the typically
non-constructive wellfoundedness proofs of termination orders, with an eye
towards the establishment of general metatheorems which characterise bounds on
the derivational complexity induced by these orders. However, ultimately we
have a much broader goal, which is to explore a number of deep mathematical
concepts which underlie termination orders, including minimal-bad-sequence
constructions, modified realizability and bar recursion. We aim to describe how
these concepts all come together to form a particularly elegant illustration of
the bridge between proofs and programs.