Derivation Lengths Classification of G\"odel's T Extending Howard's Assignment

TL;DR

This paper develops a constructive method to assign natural numbers to G"odel's T terms, providing an optimal classification of derivation lengths and extending Howard's ordinal assignment to lambda calculus, with potential applications to other higher order systems.

Contribution

It introduces a new constructive approach to assign natural numbers to lambda terms of G"odel's T, extending Howard's ordinal assignment and improving termination analysis.

Findings

Provides an optimal derivation length classification for G"odel's T.

Extends Howard's ordinal assignment to lambda calculus terms.

Offers solutions to problems in lambda term analysis compared to combinatory logic.

Abstract

Let T be Goedel's system of primitive recursive functionals of finite type in the lambda formulation. We define by constructive means using recursion on nested multisets a multivalued function I from the set of terms of T into the set of natural numbers such that if a term a reduces to a term b and if a natural number I(a) is assigned to a then a natural number I(b) can be assigned to b such that I(a) is greater than I(b). The construction of I is based on Howard's 1970 ordinal assignment for T and Weiermann's 1996 treatment of T in the combinatory logic version. As a corollary we obtain an optimal derivation length classification for the lambda formulation of T and its fragments. Compared with Weiermann's 1996 exposition this article yields solutions to several non-trivial problems arising from dealing with lambda terms instead of combinatory logic terms. It is expected that the methods developed here can be applied to other higher order rewrite systems resulting in new powerful termination orderings since T is a paradigm for such systems.