Gunnar Wilken ; Andreas Weiermann - Derivation Lengths Classification of Gödel's T Extending Howard's Assignment

lmcs:1073 - Logical Methods in Computer Science, March 6, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:19)2012
Derivation Lengths Classification of Gödel's T Extending Howard's AssignmentArticle

Authors: Gunnar Wilken ORCID; Andreas Weiermann ORCID

    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.


    Volume: Volume 8, Issue 1
    Published on: March 6, 2012
    Imported on: November 15, 2009
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,F.4.1,F.1.3

    4 Documents citing this article

    Consultation statistics

    This page has been seen 1181 times.
    This article's PDF has been downloaded 347 times.