Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Complexity of Gödel’s T in λ-Formulation
verfasst von : Gunnar Wilken, Andreas Weiermann
Erschienen in: Typed Lambda Calculi and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Let T be Gödel’s system of primitive recursive functionals of finite type in the
λ
-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
) >
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
λ
-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
λ
-terms instead of combinatory logic terms.