Classical realizability and side-effects

Étienne Miquey 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Résumé : Cette thèse s'intéresse au contenu calculatoire des preuves classiques, et plus spécifiquement aux preuves avec effets de bord et à la réalisabilité classique de Krivine. Le manuscrit est divisé en trois parties, donc la première consiste en une introduction détaillée aux concepts utilisés par la suite. La deuxième partie porte sur l’interprétation calculatoire de l’axiome du choix dépendant en logique classique, et en particulier au système dPAω d'Hugo Herbelin. Ce calcul fournit en effet, dans un cadre compatible avec la logique classique, un terme de preuve pour l'axiome du choix dépendant, qui peut être vu comme une adaptation de la preuve constructive de l’axiome du choix en théorie des types de Martin-Löf ou un internalisation dans un système de preuve de l'approche en réalisabilité de Berardi, Bezem et Coquand. L'objectif principal de cette partie est de démontrer la propriété de normalisation pour dPAω, sur laquelle repose la cohérence du système. La difficulté d'une telle preuve est liée à la présence simultanée de types dépendants (pour la partie constructive du choix), d'opérateurs de contrôle (pour la logique classique), d'objets co-inductifs (pour "encoder" les fonctions de type N → A par des streams (a₀,a₁,...)) et l'évaluation paresseuse avec partage (pour ces objets co-inductifs). On montre dans un premier temps la normalisation du call-by-need classique (présenté comme une extension du λµµ̃-calcul avec des environnements partagé), en utilisant notamment des techniques de réalisabilité à la Krivine. On développe ensuite un calcul des séquents classique avec types dépendants, dont la correction est prouvée à l'aide d'une traduction CPS tenant compte des dépendances. En combinant les deux points précédents, on définit enfin une variante en calcul des séquents du système dPAω dont on peut finalement prouver la normalisation. La dernière partie porte sur la structure algébrique des modèles induits par la réalisabilité classique. Ce travail se base sur une notion d'algèbres implicatives développée par Alexandre Miquel, une structure algébrique très simple généralisant à la fois les algèbres de Boole complètes et les algèbres de réalisabilité de Krivine, de manière à exprimer dans un même cadre la théorie du forcing (au sens de Cohen) et la théorie de la réalisabilité classique (au sens de Krivine). Le principal défaut de cette structure est qu’elle est très orientée vers le λ-calcul, et ne permet d’interpréter fidèlement que les langages en appel par nom. Pour remédier à cette situation, on introduit deux variantes des algèbres implicatives les algèbres disjonctives, centrées sur le “par” de la logique linéaire (mais dans un cadre non linéaire) et naturellement adaptées aux langages en appel par nom, et les algèbres conjonctives, centrées sur le “tenseur” de la logique linéaire et adaptées aux langages en appel par valeur. On prouve en particulier que les algèbres disjonctives ne sont que des cas particuliers d'algèbres implicatives et que l'on peut obtenir une algèbre conjonctive à partir d'une algèbre disjonctive (par renversement de l’ordre sous-jacent). De plus, on montre comment interpréter dans ces cadres les fragments du système L de Guillaume Munch-Maccagnoni en appel par valeur (dans les algèbres conjonctives) et en appel par nom (dans les algèbres disjonctives).
Type de document :
Thèse
Logic in Computer Science [cs.LO]. Université Sorbonne Paris Cité - Université Paris Diderot (Paris 7); Universidad de la República - Montevideo, Uruguay, 2017. English
Liste complète des métadonnées

Littérature citée [196 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01653733
Contributeur : Étienne Miquey <>
Soumis le : dimanche 31 décembre 2017 - 12:55:30
Dernière modification le : jeudi 11 janvier 2018 - 02:09:16

Fichier

these.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : tel-01653733, version 2

Collections

Citation

Étienne Miquey. Classical realizability and side-effects. Logic in Computer Science [cs.LO]. Université Sorbonne Paris Cité - Université Paris Diderot (Paris 7); Universidad de la República - Montevideo, Uruguay, 2017. English. 〈tel-01653733v2〉

Partager

Métriques

Consultations de la notice

23

Téléchargements de fichiers

5