Wilken, Gunnar and Weiermann, Andreas - Derivation Lengths Classification of G\"odel's T Extending Howard's Assignment

lmcs:1073 - Logical Methods in Computer Science, March 6, 2012, Volume 8, Issue 1
Derivation Lengths Classification of G\"odel's T Extending Howard's Assignment

Authors: Wilken, Gunnar and Weiermann, Andreas

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.


Source : oai:arXiv.org:1203.0115
DOI : 10.2168/LMCS-8(1:19)2012
Volume: Volume 8, Issue 1
Published on: March 6, 2012
Submitted on: November 15, 2009
Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,F.4.1,F.1.3


Share

Consultation statistics

This page has been seen 42 times.
This article's PDF has been downloaded 7 times.