Le Calcul des Constructions implicite: syntaxe et sémantique

De
Publié par

UNIVERSIT PARIS 7 - DENIS DIDEROT
U.F.R. D’INFORMATIQUE
oN attribuØ par la bibliothŁque
AnnØe 2001
T H ¨ S E
pour l’obtention du dipl me de
DOCTEUR DE L’UNIVERSIT PARIS 7
SpØcialitØ : Informatique fondamentale
prØsentØe et soutenue publiquement
par
Alexandre Miquel
le 14 dØcembre 2001
TITRE :
LE CALCUL DES CONSTRUCTIONS IMPLICITE :
SYNTAXE ET S MANTIQUE
Directeur de thŁse :
M. Hugo Herbelin
JURY
MM. Pierre-Louis Curien, PrØsident
Thierry Coquand
Furio Honsell, Rapporteurs
Jean-Yves Girard
Jean Goubault-Larrecq
Thomas Streicher, Examinateurs Remerciements
DØbuter une thŁse aprŁs avoir e ectuØ une parenthŁse de trois ans dans l’enseignement
secondaire loin du monde de la recherche n’Øtait pas une chose qui allait de soi. C’est pourquoi
je tiens ici remercier chaleureusement toutes les personnes qui m’ont assistØ dans cette
dØmarche et sans qui les fruits de ce travail n’auraient pas pu voir le jour.
Mes remerciements vont tout d’abord Hugo Herbelin, qui a encadrØ mon stage de DEA
au printemps 1998 et qui a ensuite pris en charge la direction de ma thŁse. Pendant plus de
trois ans, Hugo m’a aiguillØ et soutenu dans mon travail, en portant toujours un trŁs grand
intØrŒt aux directions que prenait ma recherche, quelles qu’elles Øtaient. Mais surtout, il m’a
apportØ son prØcieux soutien, dans les moments faciles comme dans ceux qui l’Øtaient moins,
avec la grande patience et l’extrŁme gentillesse qui sont les siennes, et je voudrais ici qu’il
sache quel point je lui en suis ...
Nombre de pages : 340
Voir plus Voir moins
UNIVERSIT PARIS 7 - DENIS DIDEROT U.F.R. D’INFORMATIQUE oN attribuØ par la bibliothŁque AnnØe 2001 T H ¨ S E pour l’obtention du dipl me de DOCTEUR DE L’UNIVERSIT PARIS 7 SpØcialitØ : Informatique fondamentale prØsentØe et soutenue publiquement par Alexandre Miquel le 14 dØcembre 2001 TITRE : LE CALCUL DES CONSTRUCTIONS IMPLICITE : SYNTAXE ET S MANTIQUE Directeur de thŁse : M. Hugo Herbelin JURY MM. Pierre-Louis Curien, PrØsident Thierry Coquand Furio Honsell, Rapporteurs Jean-Yves Girard Jean Goubault-Larrecq Thomas Streicher, Examinateurs Remerciements DØbuter une thŁse aprŁs avoir e ectuØ une parenthŁse de trois ans dans l’enseignement secondaire loin du monde de la recherche n’Øtait pas une chose qui allait de soi. C’est pourquoi je tiens ici remercier chaleureusement toutes les personnes qui m’ont assistØ dans cette dØmarche et sans qui les fruits de ce travail n’auraient pas pu voir le jour. Mes remerciements vont tout d’abord Hugo Herbelin, qui a encadrØ mon stage de DEA au printemps 1998 et qui a ensuite pris en charge la direction de ma thŁse. Pendant plus de trois ans, Hugo m’a aiguillØ et soutenu dans mon travail, en portant toujours un trŁs grand intØrŒt aux directions que prenait ma recherche, quelles qu’elles Øtaient. Mais surtout, il m’a apportØ son prØcieux soutien, dans les moments faciles comme dans ceux qui l’Øtaient moins, avec la grande patience et l’extrŁme gentillesse qui sont les siennes, et je voudrais ici qu’il sache quel point je lui en suis reconnaissant. Une thŁse est un travail de longue haleine qu’il n’est pas possible d’entreprendre sans un environnement de travail adØquat. C’est pourquoi je tiens remercier toute l’Øquipe du projet LogiCal (ex-Coq), et plus particuliŁrement Christine Paulin, Gilles Dowek, Benjamin Werner etBrunoBarras,quim’onto ertunenvironnementdetravaild’unegrandequalitØscienti que, et dans lequel j’ai disposØ d’une libertØ exceptionnelle. Cette libertØ, j’en ai pro tØ en grande partie pour assouvir ma soif de programmation, et les progrŁs que j’ai faits dans ce domaine n’auraient sans doute pas ØtØ possibles sans les conseils avisØs et l’attention permanente des membres du projet Cristal, qui va Øgalement toute ma gratitude. Paris 7, Chantal Berline a su dØbusquer une erreur subtile (que je n’aurais sans doute jamais vue sans elle) dans une premiŁre prØsentation de mes modŁles, et je l’en remercie. Je tiens remercier chaleureusement les rapporteurs de cette thŁse, Thierry Coquand et Furio Honsell, pour la relecture attentive du manuscrit comme pour l’intØrŒt qu’ils ont portØ mon travail, et cela maintes reprises. Pierre-Louis Curien, qui a trŁs t t portØ son regard sur mon travail, m’a fait bØnØ cier de ses conseils en relisant une version prØliminaire de ma thŁse, et je suis trŁs heureux qu’il ait acceptØ de prØsider le jury. Je remercie Øgalement Jean-Yves Girard pour les discussions ludiques et enrichissantes sur le sous-typage et la logique ainsi que Jean Goubault-Larrecq et Thomas Streicher pour l’honneur qu’il me font d’examiner ce travail, et qui ont eu la gentillesse de bien vouloir faire partie du jury. En n, je remercie mes proches, et plus particuliŁrement Thomas, Olivier et Patrice, pour le soutien moral qu’ils m’ont apportØ tout au long de cette thŁse. 1 2 Table des matiŁres Introduction 9 I Constructions implicites 13 1 Arguments implicites et systŁmes de types la Curry 15 1.1 Une introduction la thØorie des types . . . . . . . . . . . . . . . . . . . . . . . 15 1.1.1 Types, termes et jugements . . . . . . . . . . . . . . . . . . . . . . . . . 15 1.1.2 Le -calcul simplement typØ . . . . . . . . . . . . . . . . . . . . . . . . . 16 1.1.3 L’isomorphisme de Curry-Howard . . . . . . . . . . . . . . . . . . . . . . 19 1.1.4 Les types dØpendants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 1.1.5 Un type de tous les types . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1.2 SystŁmes de types purs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1.2.1 Le formalisme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1.2.2 Les systŁmes du cube . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 1.3 Arguments implicites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1.3.1 Les limites des PTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 1.3.2 Les arguments implicites de LEGO et de Coq . . . . . . . . . . . . . . . 37 1.3.3 Les arguments implicites de M. Hagiya et Y. Toda . . . . . . . . . . . . 39 1.4 SystŁmes de types la Curry . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 1.4.1 Les systŁmes F la Church et la Curry . . . . . . . . . . . . . . . . . 42 1.4.2 Le cube des Type Assignment Systems . . . . . . . . . . . . . . . . . . . 45 1.4.3 Type Assignment Systems et arguments implicites . . . . . . . . . . . . 50 1.4.4 Vers des systŁmes de types purs implicites? . . . . . . . . . . . . . . . . 51 2 Le Calcul des Constructions implicite 55 2.1 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 2.1.1 Les sortes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 2.1.2 Les termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 2.2 RØduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 2.2.1 Les rŁgles et . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 2.2.2 Traductions vers le -calcul . . . . . . . . . . . . . . . . . . . . . . . . . 58 2.2.3 Non-con uence de la -rØduction dans CC! . . . . . . . . . . . . . . . 60 2.3 Typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 2.3.1 Les ensembles Axiom et Rule . . . . . . . . . . . . . . . . . . . . . . . 61 3 2.3.2 Ordre de cumulativitØ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 2.3.3 Contextes de typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 2.3.4 Jugements et dØrivations . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 2.3.5 Signi cation des rŁgles d’infØrence . . . . . . . . . . . . . . . . . . . . . 63 2.4 PropriØtØs du typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 2.4.1 PropriØtØs ØlØmentaires dans CCI . . . . . . . . . . . . . . . . . . . . . . 67 2.4.2 Formes stables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 2.4.3 Le calcul implicite restreint CCI . . . . . . . . . . . . . . . . . . . . . . 71 2.4.4 DØrivations -directes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 2.4.5 PrØservation du typage par la -rØduction . . . . . . . . . . . . . . . . 80 2.5 Sous-typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 2.5.1 La relation de sous-typage . . . . . . . . . . . . . . . . . . . . . . . . . . 81 2.5.2 quivalence de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 2.6 RØsultats de cohØrence relative . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 2.6.1 CohØrence relative du calcul implicite . . . . . . . . . . . . . . . . . . . 84 2.6.2 logique et rŁgle de renforcement . . . . . . . . . . . . . . . . 87 2.7 Exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 2.7.1 Les listes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 2.7.2 Les listes dØpendantes (vecteurs) . . . . . . . . . . . . . . . . . . . . . . 91 2.7.3 galitØ de Leibniz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 2.7.4 Quanti cations existentielles . . . . . . . . . . . . . . . . . . . . . . . . . 97 2.7.5 IncohØrence forte . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100 II ModŁles cohØrents 103 3 Introduction aux modŁles 105 3.1 ModŁles du Calcul des Constructions avec univers . . . . . . . . . . . . . . . . . 105 3.1.1 Le modŁle ensembliste classique boolØen . . . . . . . . . . . . . . . . . . 107 3.1.2 Le modŁle intuitionniste . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 3.2 Les limites des modŁles purement ensemblistes . . . . . . . . . . . . . . . . . . 114 3.2.1 Church versus Curry . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 3.2.2 Quelle interprØtation pour le sous-typage? . . . . . . . . . . . . . . . . . 115 3.2.3 Une in typØe ou non-typØe . . . . . . . . . . . . . . . . . . . 116 3.3 ModŁles abstraits du Calcul des Constructions implicite . . . . . . . . . . . . . 117 3.3.1 -modŁles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 3.3.2 -modŁles sous-extensionnels . . . . . . . . . . . . . . . . . . . . . . . . 119 3.3.3 ModŁles abstraits du calcul implicite . . . . . . . . . . . . . . . . . . . . 121 3.3.4 Extension de l’interprØtation au termes du calcul implicite . . . . . . . . 123 3.3.5 ModŁles restreints et modŁles non-restreints . . . . . . . . . . . . . . . . 125 3.4 Quelques notions de thØorie des ensembles . . . . . . . . . . . . . . . . . . . . . 127 3.4.1 Ordinaux et cardinaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 3.4.2 Co nalitØ et rØguliers . . . . . . . . . . . . . . . . . . . . . . . 130 3.4.3 Ensembles transitifs et ensembles bien fondØs . . . . . . . . . . . . . . . 130 3.4.4 HiØrarchie cumulative (V ) . . . . . . . . . . . . . . . . . . . . . . . . . . 132x 3.4.5 Ensembles inaccessibles et cardinaux inaccessibles . . . . . . . . . . . . . 133 4 4 Espaces cohØrents 135 4.1 La catØgorie des espaces cohØrents . . . . . . . . . . . . . . . . . . . . . . . . . 136 4.1.1 DØ nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136 4.1.2 Structure de l’ensemble ordonnØ (A; ) . . . . . . . . . . . . . . . . . . 137 4.1.3 Fonctions stables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 4.1.4 Espaces cohØrents plats . . . . . . . . . . . . . . . . . . . . . . . . . . . 141 4.1.5 Produit direct de deux espaces cohØrents . . . . . . . . . . . . . . . . . . 141 4.1.6 Somme directe de deuxts . . . . . . . . . . . . . . . . . 142 4.1.7 Espace des fonctions stables . . . . . . . . . . . . . . . . . . . . . . . . . 143 4.1.8 Fonctions linØaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148 4.2 La catØgorie des plongements rigides . . . . . . . . . . . . . . . . . . . . . . . . 149 4.2.1 Plongements rigides . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 4.2.2 Colimites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152 4.2.3 Construction d’un modŁle du -calcul . . . . . . . . . . . . . . . . . . . 153 4.3 La stabilitØ revisitØe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 4.3.1 La catØgorie des quasi-espaces cohØrents . . . . . . . . . . . . . . . . . . 156 4.3.2 La des -espaces cohØrents . . . . . . . . . . . . . . . . . . . . 159 4.3.3 -modŁles -cohØrents . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162 5 Un modŁle restreint classique du calcul implicite 165 5.1 Types dans les espaces cohØrents . . . . . . . . . . . . . . . . . . . . . . . . . . 167 5.1.1 Bases de types et types sØmantiques . . . . . . . . . . . . . . . . . . . . 167 5.1.2 Sous-typage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169 5.1.3 Intersection et produit dØpendant . . . . . . . . . . . . . . . . . . . . . . 170 5.1.4 Une caractØrisation interne de8(a2X;Y ) et ( a2X;Y ) . . . . . . . . 173a a 5.1.5 Types - nis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175 5.1.6 Les types extrØmaux 0 et 1 . . . . . . . . . . . . . . . . . . . . . . . . . 176 5.1.7 Types comme citoyens de premiŁre classe . . . . . . . . . . . . . . . . . 177 5.2 Le modŁle classique du calcul implicite restreint . . . . . . . . . . . . . . . . . . 181 5.2.1 Le schØma gØnØral de l’interprØtation . . . . . . . . . . . . . . . . . . . . 181 5.2.2 RØsolution deA = [A!A] Ty (A) . . . . . . . . . . . . . . . . . . . 182 5.2.3 Structure de modŁle abstrait du calcul implicite . . . . . . . . . . . . . . 185 5.2.4 Un modŁle classique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 5.2.5 galitØ dans le modŁle . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188 6 RØalisabilitØ dans les espaces cohØrents 193 6.1 La catØgorie desK-espacests . . . . . . . . . . . . . . . . . . . . . . . . 193 6.1.1 Espace de calcul . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193 6.1.2 K-espaces cohØrents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194 6.1.3 ( ; K)-morphismes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195 6.1.4 Structure de catØgorie cartØsienne fermØe . . . . . . . . . . . . . . . . . 199 6.1.5 Plongements rigides et colimites . . . . . . . . . . . . . . . . . . . . . . . 200 6.1.6 Types dans lesK-espaces cohØrents . . . . . . . . . . . . . . . . . . . . . 202 6.1.7 OpØrateurs de produit dØpendant et d’intersection . . . . . . . . . . . . 204 6.1.8 K-espaces cohØrents locatifs . . . . . . . . . . . . . . . . . . . . . . . . . 205 6.2 Le modŁle intuitionniste . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 207 6.2.1 L’Øquation du modŁle intuitionniste . . . . . . . . . . . . . . . . . . . . 208 5 6.2.2 RØsolution de l’ØquationA = ( A) . . . . . . . . . . . . . . . . . . . . . 209 6.2.3 Structure de -modŁle sous-extensionnel . . . . . . . . . . . . . . . . . . 211 6.2.4 de modŁle du calcul implicite . . . . . . . . . . . . . . . . . . 213 6.2.5 Discrimination des programmes dans Set . . . . . . . . . . . . . . . . . . 215 6.2.6 InvaliditØ du tiers-exclu . . . . . . . . . . . . . . . . . . . . . . . . . . . 216 7 Le thØorŁme de normalisation forte 219 7.1 Une preuve abstraite de normalisation forte . . . . . . . . . . . . . . . . . . . . 220 7.1.1 Termes fortement normalisables . . . . . . . . . . . . . . . . . . . . . . . 220 7.1.2 Ensembles saturØs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221 7.1.3 ModŁles de normalisation . . . . . . . . . . . . . . . . . . . . . . . . . . 224 7.1.4 PropriØtØs des modŁles de normalisation . . . . . . . . . . . . . . . . . . 224 7.1.5 L’invariant de . . . . . . . . . . . . . . . . . . . . . . . . . 227 7.1.6 ModŁles de normalisation et rØalisabilitØ modi Øe . . . . . . . . . . . . . 231 7.2 Le modŁle concret de . . . . . . . . . . . . . . . . . . . . . . . . . 232 7.2.1 L’Øquation du modŁle de normalisation . . . . . . . . . . . . . . . . . . . 233 7.2.2 Types saturØs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234 7.2.3 Construction du modŁle de . . . . . . . . . . . . . . . . . 235 7.2.4 Structure du -modŁle sous-extensionnelA . . . . . . . . . . . . . . . . 236 7.2.5 Types bien formØes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 7.2.6 OpØrateurs de produit dØpendant et d’intersection . . . . . . . . . . . . 239 7.2.7 La hiØrarchie d’univers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 240 III Types et ensembles 243 8 Le Paradoxe de Russell dans les systŁmes U et U 245 8.1 Une prØsentation des systŁmes U et U . . . . . . . . . . . . . . . . . . . . . . 246 8.1.1 Les systŁmes de types purs U et U . . . . . . . . . . . . . . . . . . . 246 8.1.2 Strati cation des termes . . . . . . . . . . . . . . . . . . . . . . . . . . . 247 8.1.3 La logique des systŁmes U et U . . . . . . . . . . . . . . . . . . . . . . 249 8.1.4 Connecteurs, quanti cateurs et ØgalitØ de Leibniz . . . . . . . . . . . . . 252 8.2 ReprØsentation des ensembles en thØorie des types . . . . . . . . . . . . . . . . . 254 8.2.1 La reprØsentation na ve . . . . . . . . . . . . . . . . . . . . . . . . . . . 254 8.2.2 Une dØ nition incorrecte . . . . . . . . . . . . . . . . . . . . . . . . . . . 254 8.2.3 ReprØsentation des ensembles hØrØditairement nis . . . . . . . . . . . . 255 8.2.4 ReprØsentation des ensembles par des arbres bien fondØs . . . . . . . . . 257 8.3 ReprØsentation des ensembles par des graphes pointØs . . . . . . . . . . . . . . 258 8.3.1 Graphes pointØs et hyper-ensembles . . . . . . . . . . . . . . . . . . . . 259 8.3.2 Existence et unicitØ de l’atome . . . . . . . . . . . . . . . . . . . . . . 260 8.3.3 galitØ et bissimulation . . . . . . . . . . . . . . . . . . . . . . . . . . . 261 8.4 La thØorie des ensembles de Frege dans le systŁme U . . . . . . . . . . . . . . . 264 8.4.1 Les grandes lignes de la preuve . . . . . . . . . . . . . . . . . . . . . . . 265 8.4.2 Graphes pointØs dans le systŁme U . . . . . . . . . . . . . . . . . . . . . 266 8.4.3 Le type universel des graphes pointØs . . . . . . . . . . . . . . . . . . . . 268 8.4.4 Le schØma de comprØhension non-restreint . . . . . . . . . . . . . . . . . 271 8.4.5 Une reformulation du paradoxe dans le systŁme U . . . . . . . . . . . . 274 6 9 Un modŁle de la thØorie des ensembles de Zermelo dans F!:3 277 9.1 La thØorie des types de Church avec deux univers . . . . . . . . . . . . . . . . . 278 9.1.1 Le systŁme de types purs !: 3 . . . . . . . . . . . . . . . . . . . . . . . 278 9.1.2 Une prØsentation strati Øe . . . . . . . . . . . . . . . . . . . . . . . . . . 279 9.1.3 La logique intuitionniste de F!:3 . . . . . . . . . . . . . . . . . . . . . . 282 9.2 Un type prouvablement in ni dans Type . . . . . . . . . . . . . . . . . . . . . . 2822 9.2.1 Le type des entiers de Church dans Type . . . . . . . . . . . . . . . . . 2832 9.2.2 InjectivitØ de la fonction successeur . . . . . . . . . . . . . . . . . . . . . 285 9.2.3 Quelques propriØtØs arithmØtiques . . . . . . . . . . . . . . . . . . . . . 287 9.3 Graphes pointØs dans F!:3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289 9.3.1 BissimilaritØ et appartenance . . . . . . . . . . . . . . . . . . . . . . . . 289 9.3.2 Quelques structures de donnØes . . . . . . . . . . . . . . . . . . . . . . . 291 9.4 La traduction des axiomes de Zermelo . . . . . . . . . . . . . . . . . . . . . . . 294 9.4.1 L’axiome de la paire . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 296 9.4.2 Les axiomes de comprØhension . . . . . . . . . . . . . . . . . . . . . . . 297 9.4.3 L’axiome des parties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 300 9.4.4 de la rØunion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 302 9.4.5 Ensemble vide et successeur . . . . . . . . . . . . . . . . . . . . . . . . . 304 9.4.6 L’axiome de l’in ni . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 306 9.5 Le type des graphes pointØs dans Type . . . . . . . . . . . . . . . . . . . . . . 3103 9.5.1 Une premiŁre traduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 310 9.5.2 Le type des ensembles . . . . . . . . . . . . . . . . . . . . . . . . . . . . 312 9.5.3 Inclusion et prØdicats compatibles . . . . . . . . . . . . . . . . . . . . . 314 9.5.4 Les axiomes de Zermelo dans le type U . . . . . . . . . . . . . . . . . . . 315 9.6 Le tiers-exclu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 319 9.6.1 Le systŁme F!:3 + cl . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 319 9.6.2 La A-traduction de Coquand-Herbelin . . . . . . . . . . . . . . . . . . . 320 9.6.3 Traduction des termes fonctionnels . . . . . . . . . . . . . . . . . . . . . 321 9.6.4 T des de preuves . . . . . . . . . . . . . . . . . . . . . . 322 9.6.5 Traduction de la constante cl . . . . . . . . . . . . . . . . . . . . . . . . 323 9.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 324 9.7.1 La puissance thØorique de F!:3 . . . . . . . . . . . . . . . . . . . . . . . 324 9.7.2 La de Z . . . . . . . . . . . . . . . . . . . . . . . . . 326 9.7.3 La puissance thØorique de CC! . . . . . . . . . . . . . . . . . . . . . . . 328 7 8
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.