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.

Total functionals and well-founded strategies

BERARDI, Stefano;DE' LIGUORO, Ugo
1999-01-01

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.
1999
Inglese
contributo
1 - Conferenza
TLCA'99
L'Aquila
7 - 9 Aprile 1999
Internazionale
Jean-Yves Girard
Typed Lambda Calculi and Applications, Proceedings of the 4th International Conference, TLCA'99
Esperti anonimi
Springer Verlag
Berlin, Heidelberg
GERMANIA
1581
54
68
15
978-3-540-65763-7
http://link.springer.com/chapter/10.1007%2F3-540-48959-2_6
no
3 – prodotto con deroga per i casi previsti dal Regolamento (allegherò il modulo al passo 5-Carica)
2
info:eu-repo/semantics/conferenceObject
04-CONTRIBUTO IN ATTI DI CONVEGNO::04A-Conference paper in volume
STEFANO BERARDI; U. DE' LIGUORO
273
reserved
File in questo prodotto:
File Dimensione Formato  
1999 Berardi dL - Total Functionals and Well-Founded Strategies.pdf

Accesso riservato

Descrizione: Articolo principale
Tipo di file: PDF EDITORIALE
Dimensione 313.43 kB
Formato Adobe PDF
313.43 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/17634
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact