|
|
VOLUME 8, ISSUE 1, PAPER 19
|
Derivation Lengths Classification of Gödel's T Extending Howard's Assignment
|
©Gunnar Wilken, Structural Cellular Biology Unit, OIST Graduate University, Japan
©Andreas Weiermann, Ghent University
|
Abstract
Let T be Gödel'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.
|
Publication date: March 6, 2012
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-8(1:19)2012
Hit Counts: 930 |
 Creative Commons | |
