Data di Pubblicazione:
1999
Abstract:
We investigate how to characterize total set-theoretic functionals in game theoretic models, and prove that well-founded winning strategies give a proper subclass of them, exactly consisting in Tait-definable functionals. Within the framework of generalized Novikoff-Coquand games with transfinite plays, total functionals (of finite type) are exactly definable by winning strategies, possibly of transfinite height. We exhibit two computable total type 3 functionals (of interest in program extraction from classical proofs) such that no well-founded strategy may define them.
Tipologia CRIS:
04A-Conference paper in volume
Elenco autori:
STEFANO BERARDI; U. DE' LIGUORO
Link alla scheda completa:
Titolo del libro:
Typed Lambda Calculi and Applications, Proceedings of the 4th International Conference, TLCA'99
Pubblicato in: