Complexity Bounds for Ordinal-Based Termination

TL;DR

This paper develops a method to derive complexity bounds on program termination times using length function theorems applied to ordinal-based ranking functions, advancing understanding of program complexity in formal systems.

Contribution

It introduces a novel approach to prove length function theorems for ordinals, enabling complexity bounds for programs proven to terminate via ordinal ranking functions.

Findings

Length function theorems are established for ordinals.

Complexity bounds are derived for programs with ordinal-based termination proofs.

The approach extends existing methods to a new class of well quasi orders.

Abstract

`What more than its truth do we know if we have a proof of a theorem in a given formal system?' We examine Kreisel's question in the particular context of program termination proofs, with an eye to deriving complexity bounds on program running times. Our main tool for this are length function theorems, which provide complexity bounds on the use of well quasi orders. We illustrate how to prove such theorems in the simple yet until now untreated case of ordinals. We show how to apply this new theorem to derive complexity bounds on programs when they are proven to terminate thanks to a ranking function into some ordinal.