Ordinal Complexity of Recursive Programs and their Termination Proofs

Matthew V H Fairtlough

Abstract: A hierarchy of tree-classes \Omega_{0}, \Omega_{1}, ... \Omega_{n}, ... of tree-ordinals is introduced and the notion of a structured tree-ordinal is defined. We proceed to give a category-theoretic treatment of these tree-classes and of the Slow-Growing Hierarchy G defined over them. The treatment is based on that given by Dennis Jones and Wainer in their paper ``Subrecursive Hierarchies via Direct Limits''. The idea of a decomposable morphism is introduced, allowing us to define G as a functor in its ordinal arguments as well as in its numerical ones.

In chapter two new notions of elementary and primitive recursive ordinals are given, in the context of the material developed on tree-ordinals. The aim is to sidestep the collapsing phenomenon (every recursive function is definable by recursion on an elementarily coded well-order of order type w) which prevents a subrecursive classification using set-theoretic ordinals. The main theorem is a reformulation in terms of tree-ordinals of the result that every elementary number-theoretic function is bounded by some fixed iterate of the exponential function x maps to 2^{x}. The order-types of all elementary tree-ordinals are thus shown to be below e_{0}.

The third chapter explores the connection between hierarchies of number- theoretic functions and various developments of the w-arithmetic (Buchholz) with different forms of cut-rule. Versions of the bounding lemma (Buchholz and Wainer, 1987) are established and converses obtained, one for each hierarchy. Complexity characterisations of the functions provably computable in the various infinitary systems are given. Proofs are given of the embedding theorem (Buchholz) and of the facts that the provably recursive functions of \sum^{0}_{1}-Induction are primitive recursive and that the provably recursive functions of Peano Arithmetic are bounded by a member of the Fast-Growing hierarchy below e_{0}. There is a section on cut elimination, which shows how proofs in a proof system with one form of cut can be reduced to proofs in a system with a weaker form of cut.

The main results of the fourth chapter are as follows:Given a set A \subseteq \Gamma^{s}, T-WHILE(A) is the set of programs built from sequencing, conditionals and while-loops, from tree parameters \alpha \in A. HARDY(A) is an equivalent formulation, based on a Kleene style presentation which includes primitive recursion and adds in the Hardy functionals. REC(A) is a set of functions defined by composition, conditionals and nested recursions, with tree parameters in A. H(A) is a set of tail recursions parameterised by elements of A. If A satisfies suitable closure conditions such as ``Turing machine representability'' and closure under addition, multiplication then Theorem II tells us

Theorem III tells us that under somewhat weaker conditions on A,
REC(w.A) = T-WHILE(w^{A}).
(= between classes of programs denotes the fact that there are effective each-way compilations between them). Theorem III is a generalization of a theorem of Tait showing that nested recursions over a given well-ordering can be compiled to unnested ones but at the cost of an exponential increase in the size of the well-ordering.

Chapter five gives another equivalence in the style of theorems I,II and III. Theorem IV states that, if A satisfies certain conditions, then

PROV(\vdash^{w.A}_{\sum_1^0 C} = REC(w.A).
The chapter ends with some examples.

PhD Thesis - Price £7.00

LFCS report ECS-LFCS-92-196 (also published as CST-88-92)

Previous | Index | Next