Bar recursion, sémantique dénotationnelle et réalisabilité classique

Carte non disponible

Date/heure
Date(s) - 26/03/2015
11 h 00 min - 12 h 30 min

Catégories


L’opérateur de bar recursion, introduit dans les années 60 par C. Spector pour “prouver” la consistance de l’Analyse, a été recyclé à partir de 1998, par Berardi, Bezem, Coquand, Berger, Oliva, Kohlenbach, … pour obtenir des programmes à l’aide de l’axiome du choix dépendant (DC).
Une autre méthode pour ce faire est, en réalisabilité classique, d’utiliser une instruction “quote”. La question se posait, du rapport entre ces deux méthodes. En fait, on verra que l’opérateur de “bar recursion” ne fonctionne que dans les modèles de sémantique dénotationnelle, où “quote” n’a aucun sens. On verra aussi que, dans ces modèles, cet opérateur fournit des programmes pour l’axiome du bon ordre sur R, et pour toutes les formules “vraies” d’Analyse.

[http://www.pps.univ-paris-diderot.fr/~krivine/]

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange