BAR-RÉCURSION, ANALYSE ET RÉALISABILITÉ CLASSIQUE
Hadrien Batmalle, IRIF
Salle B107, bâtiment B, Université de Villetaneuse
16/06/2017 11:00 - 12:30
Résumé :
La réalisabilité classique est une théorie née des travaux de
Jean-Louis Krivine dans les années 1990, à la frontière entre la
logique et l'informatique théorique. Côté informatique, elle offre un
cadre adapté à l'interprétation calculatoire de preuves classiques.
Côté logique, elle apparaît comme une généralisation prometteuse du
forcing de Cohen. À un modèle du lambda-calcul, on peut ainsi associer
un modèle de la théorie des ensembles ZF.
On s'intéresse ici à des modèles de programmation vérifiant une
propriété de continuité: il peut s'agir de modèles basés sur les
domaines de la sémantique dénotationnelle, ou bien de modèles de
termes d'une version infinitaire du lambda-calcul. Dans ces modèles,
l'instruction 'quote' (qu'on utilise usuellement en réalisabilité
classique pour interpréter l'axiome du choix dépendant) n'est pas
disponible. On utilise donc la technique de la bar-récursion pour
interpréter l'axiome du choix dépendant. Or (en considérant la
réalisabilité classique comme une généralisation du forcing), il
apparaît que la bar-récursion est de plus l'analogue de la condition
de chaîne descendante dans les algèbres de forcing (qui correspond
à une propriété de préservation des réels). On obtient alors que toute
formule de l'analyse vraie dans le modèle ambiant est réalisée dans
ces nouveaux modèles, ce qui nous amène à la question suivante:
quel est le comportement des programmes réalisant des formules de
l'analyse?
