Le Calcul des Constructions implicite: syntaxe et sémantique

Alexandre Miquel

Sujets

• Propriété Camalon
• Concept
• Cubewano
• Normes et standards industriels
• Relation de un à un
• Liste des microprocesseurs Intel

Informations

• Publié par: Ossa
• Nombre de lectures: 129
• Langue: Français
• Poids de l'ouvrage: 2 Mo

Extrait

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