D IAGRAMMES P IERRE A RGERON Sémantique catégorique des types : comprendre le système F Diagrammes, tome 19 (1988), exp. no 2, p. PA1-PA40 © Université Paris 7, UER math., 1988, tous droits réservés. L’accès aux archives de la revue « Diagrammes » implique l’accord avec les conditions générales d’utilisation (http://www.numdam.org/legal.php). Toute utilisation commerciale ou impression systématique est constitutive d’une infraction pénale. Toute copie ou impression de ce fichier doit contenir la présente mention de copyright. Article numérisé dans le cadre du programme Numérisation de documents anciens mathématiques http://www.numdam.org/ OXAQRAMMCS VOLUME SEMANTIQUE 19, 1988 CATEQORIQUE DES TYPES: COMPRENDRE LE SYSTEME I Pierre Ageron ABSTRACT This paper introduces new ideas in categorical theory of types. It is divided into two parts (tuo chapters of a forthcoming "thèse de doctorat"), In the first part, we are concerned with the question "what is a type in a category ?" . The usual "type • functor" point of view is criticized and replaced by a nore gênerai and more expressive framework in the spirit of Ehresmann's sketches, thus providing a unification between algebraic theory of types and logical theory of types. In the second parti we apply thèse ideas to give a new categorytheoretical interprétation of Girard1s System F of second order X-calculus. Afflong other things, we discuss equational présentâtions, variances analysis and uniformity. REMERCIEMENTS Je remercie mon directeur de thèse J.Y, Girard de bien vouloir accepter ce texte comme témoignage de mon admiration pour ses travaux. A. M. S. 8U8 CLASS. 10 A 18. 03 8 30, 18 O 38, 03 B 11 Je veux exprimer toute ma reconnaissance « C. Lair pour sa disponibilité aux étudiants et l'aide considérable qu'il m'a apportée. . Enfin, je remercie C. Even et C. encouragements et remarques constructives. Retoré pour leurs PARTIE QU'EST-CE QU'UN TYPE I; DANS UNE CATEGORIE? Ce qui suit est une discussion autour de la notion de type, en particulier de quelques-unes de ses représentations en termes de théorie des catégories. L'idée de type est, on le sait, un héritage de Bertrand Russe11 qui avait en vue d'éliminer les paradoxes de la théorie des ensembles. Il subsiste deux traditions vivantes en matière de types, nettement séparées*. - les systèmes de types issus de la logique, - les types abstraits de données en informatique. On peut y ajouter (sans jeu de mots!): - la théorie des esquisses et des types de structures mathématiquesf fondée en 1966 par C. Ehresmann, Les définitions que nous proposerons ont» entre autres* l'avantage de rendre consubstantiels ces trois points de vue. Pourquoi choisir le langage de la théorie des catégories pour parler de types? Un argument de départ peut être le suivant: - la notion de type est intuitivement peu différente de celle d'ensemble, or chaque catégorie est une sorte de variante de la théorie des ensembles, il est alors normal de chercher à faire vivre les types dans certaines catégories convenables, la catégorie E n s n'est alors plus qu'une catégorie parmi les autres, adaptée ou non au type ou système de types considéré. Nous suggérons donc de chercher systématiquement à définir des assertions du style: - la catégorie C est une sémantique pour le type i (resp. pour le système de types T ) , que l'on pourra aussi formuler ainsi: - le type ? (resp. le système de types -xr) est C-iste, PART, Il OtU'EST-CC QU'UN TYPE DAMS U N E CATEQORZE ? C'est ce que nous ferons dans une deuxième partie pour les types du système F. Pour l'heure, revenons à la question de fond: qu'est-ce un type dans une catégorie C ? La première idée qui vient à l'esprit, c'est de considérer que: TYPE = OBJET DE C . Ce point de vue impose de se donner arbitrairement un certain nombre de types de base, à partir desquels les autres types sont construits par produits, exponentielles, sommes ,,. On retrouve ici les limitations d'expressivité du X-calcul typé ordinaire de Curry-Church, dans lequel il n'est pas possible de manipuler les types de données courants (booléen, entier, liste ... ), à moins de considérer ceux-ci comme des types atomiques et d'introduire pour chacun d'eux de nouveaux schémas non-logiques. C'est précisément l'intérêt du système F , ou X-calcul typé du deuxième ordre ([<3irard7l], [6irard86]), que d'échapper à la fiction de l'atomicité, tout en restant purement logique (c'est la version fonctionnelle du calcul propositionnel intuitionniste du deuxième ordre). Dans ce système, comme dans d'autres voisins, il n'y a plus de types de base: tous les types y sont construits, conformément à leur "géométrie11 intrinsèque. Ceci est rendu possible par la considération de types variables, c'est-à-dire de types où figurent librement des variables de type: X , Y ... (nous y reviendrons plus en détail dans la deuxième partie). Comment représenter catégoriquement un type variable % , avec n variables de type libres? On est d'abord tenté de répondre: - par un foncteur T : C " -* C . Mais on se rend vite compte qu'imposer la covariance par rapport aux arguments est une condition trop forte (sauf dans le cas de certaines catégories "hémiplégiques11: notamment des catégories de plongements - comme dans [6irard86] ou aussi [Coquand88]). Par l»A 4 PART. X: QU'EST-CE QU'UN TYPE DANS UNE CATEGORIE ? exemple, il faut pouvoir séparer occurrences négatives et positives d'une même variable par rapport au constructeur * . X 9 Une solution consiste alors à dédoubler chaque variable X en et Xe1 , donc à opter pour un "bifoncteur": x : (C")0*» x cn -» c . Ce point de vue, qui est celui de [Freyd-Qirard-ScedrovScott88], peut paraître assez artificiel ("schizophrène11). De plus, il est un obstacle à une représentation équationnelle du type T , car l'endofoncteur (-)°** de Ca*t n'est pas co-représentable (autrement dit: G 0 9 n'est pas M C à la puissance op " ! ) . Or on sait l'intérêt que les informaticiens (en particulier) portent aux représentations équationnelles des concepts catégoriques ([Curien86], [Coquand-Ehrhard87]). Autre critique: une telle représentation ne prend pas en compte la structure interne des types, ce qui est un péché contre l'esprit même du système F. Si l'on veut être plus précis, il faut cesser d'assimiler un type à un seul objet de C et le voir plutôt comme un diagramme dans C , figurant les fonctions de construction, les fonctions d'accès ... Que faut-il entendre par diagramme ? Au sens strict, un diagramme dans C est un foncteur de J dans C , où J est une petite catégorie (ou encore, ce qui est à peine plus général, un petit compographe - voir la définition plus loin). Hais il faut à J une structure supplémentaire, permettant de spécifier que certains des objets et/ou des flèches de C , en lesquels il se réalise, obéissent à telle ou telle propriété universelle. Ainsi, si l'on n'a à spécifier que des produits, la structure de signature est suffisante (cas des types abstraits de données en informatique). La notion d'esquisse ([Ehresmann68]) permet plus généralement de spécifier des cônes limite projective ou limite induetive. Mais pour spécifier aussi des propriétés universelles plus complexes, car "à plusieurs niveaux" (comme celles définissant une exponentielle ou un objet des entiers naturels), il nous faut recourir à la notion de trame ([Lair87]). PART. X: QU'EST-CE QU'UN TYPE DANS UNE CATEGORIE ? 1, Trames, homomorphismes Compographes, fondeurs, transformations et modèles, naturelles. Un compographe <3 est un graphe (orienté), dans lequel (seulement) certains couples de flèches consécutives ont un composé d é f i n i . On suppose de plus que l'on dispose pour tout objet G d'une flèche I d * : G - * G , de sorte que pour toute flèche g : 6 - » G', les composés g. I d 0 e t I d e - . g soient définis e t égaux à g. Les graphes, les catégories sont des cas p a r t i c u l i e r s de compographes, On d é f i n i t sans d i f f i c u l t é l a notion de foncteur entre deux compographes <3 e t <3' , ainsi que c e l l e de transformation naturelle entre deux foncteurs F 1 f F 2 : <3 -» C , s i C est une catégorie. Trames et homomorphismes de trames (par récurrence sur n e |\|). a) Une trame d'ordre 0 est un compographe e t un homomorphisme de trames d'ordre 0 est un foncteur entre compographes. b) T - ( T , f - f - ( T ) , M * ( T > ) est une trame d'ordre < n+1 si, et seulement si: - T est un compographe, - H - ( T ) et *-T(T) sont des ensembles de triplets (F',HF) où + H\T%H -» TH est un homomorphisme de trames d'ordre < n, • F1 : T ' w -» T est un foncteur, + F : TH -* T est un foncteur, + F o H » F' . c) H • (T',H, T") est un homomorphisme de trames d'ordre < n+1 si, et seulement si: - T 1 , T sont des trames d'ordre < n+1 , - H : T ' -* T est un foncteur tel que: + (F'^AtiF*) e H-iT') *> (HoF'2l /fe, HoF2) e #-#-( T ) , + € H*iTl) «> (HoF',, W,, HoF, ) e ht+i T ) . Remarquons que: - il faut faire attention à la façon de lire cette définition, par exemple, pour avoir la définition d'une trame d'ordre < 3 , il faut parcourir les alinéas dans l'ordre suivant: PART, X: QU'EST-CE QU'UN TYPE DANS UNE CATEGORIE ? a),b),c),b),c),b), - si T est d'ordre 0, on convient que hi~i T ) » fnf*( T ) » 0 , - en remplaçant dans cette définition le mot "compographe" par le mot "graphe", on obtient une structure plus particulière que celle de trame que nous appellerons graphotrame, - si s est un entier naturel, le graphe discret à s objets sera (encore) noté s et la catégorie associée à la relation d'ordre i sur C 0, 1 ,.., s ) sera notée ; la trame d'ordre 0 de support s (resp. ) sera aussi notée s (resp ) , - on peut représenter une trame par le schéma suivant (remarquer les signes - et + ): Catégorie des modèles d'une trame T dans une catégorie C On note C " la sous-catégorie pleine de la catégorie des foncteur s de T vers C dont les objets M , appelés modèles de 7" dans C , sont définis (par récurrence sur l'ordre de T ) comme suit: - V (F', H F) e /-7-( T ) , MoF1 est un modèle de T1 „ , MoF est un modèle de TH * et pour tout modèle N de TH dans C rH vérifiant NoH « MoF' , il existe dans C une unique flèche & de N vers MoF qui vérifie &oH • IdMoR- (on dit alors que MoF' est un prolongement co-universel de MoF le long de H ), - V (F«, «, F) c ht+lT), MoF' est un modèle de T ' „ , MoF est un modèle de TH # et pour tout modèle N de TH dans C rH vérifiant NoH » MoF' , il existe dans C une unique flèche & de MoF vers N qui vérifie &oH » IdMOF- (on dit alors que MoF' est un prolongement universel de MoF le long de H ) , RA T RART. Z| QU'EST—CE QU'UN TVRE DANS UNE CATEGORIE T On peut également définir des modèles faibles, en supprimant le mot "unique" de cette définition; autrement dit en ne demandant que des prolongements quasi-co-universels, Nous noterons Mod( T , C ) la classe des objets de (attention: la notation n'est pas celle de [Lair87]>. C"*"" En notant T r a m la catégorie des trames, on a donc un bimodule de T r a m à C a t , i.e un foncteur Mod : T r a m o p x C a t -» Ens 2, Syntaxes de types et types, Préliminaires, Revenons à la présentation des types. Toute la discussion qui a précédé nous amène à voir un type variable comme une application - et non plus un foncteur - telle que: T : Mod (n, C ) -» Mod(J, C ) où *7 est une (petite) trame figurant la "géométrie" du type. Bien entendu, il doit être précisé comment n s'envoie dans JT . On peut facilement aller un peu plus loin et accepter des types variables qui contiendraient des hypothèses sur leurs arguments (non-vacuité, inclusions, . . , ) . Pour de tels types, il convient d'admettre des arités autres que des entiers naturels, c'est-à-dire de considérer plus généralement des applications % : Mod(X, C ) -* Mod(J\ C ) associées d'une façon plus ou moins naturelle à un homomorphisme de trames H \ I -» JT , RART. X: QU*EST—CE QU'UN TYPE DANS UNE CATEGORIE 7 Il y a au moins deux (familles de) telles applications qui sont naturelles dorsqu' elles sont définies): ce sont les applications "choix de prolongement co-universel (resp. choix de prolongement universel) le long de H ". Elles conduisent à deux notions de types (sans préjuger la possibilité d'en imaginer d'autres). Syntaxes de types, syntaxe Une H: r de types est un homomorphisme de trames -* jr . Types inductifs et types Un type induetif projectifs, (resp. projectiO dans C de syntaxe H est une application x : Mod(J, C ) -* Mod(J, C ) telle que: - Mod(W, O o t • IdViocKjc. o * - V N e Mod(J, C ) , V M € M o d ( J , C ) , on a: Motf » N => 3 ! S: 3! &: M -» T(N) / SoW= IdN ). Classiquement, on voit par exemple que: -si I est un compographe, si J est le compographe I** obtenu en ajoutant à I un (nouvel) objet terminal et si H est le foncteur d'inclusion de I dans J , alors un type indue tif dans C de syntaxe H est un choix de limites les foncteur s de I dans C , induetives pour -si I est un compographe, si JT est le compographe I" obtenu en ajoutant à I un (nouvel) objet initial et si H est le foncteur d'inclusion de I dans JT , alors un type projectif dans C de syntaxe H est un choix de limites RART. QU'EST—CE QU'UN TYPE DANS UNE CATEGORIE T Il projectives pour les fondeurs de I dans C , - s i I est la trame d'ordre 0 suivante: si JT est la trame d'ordre 1 suivante: Pa t B<— P —»E a |p* P Pi Pi et si H H t 1 ' hoftomorphisee canonique de I d a m J" « alors un type projectif dans C de syntaxe H est un choix de diagrammes 'exponentielle" pour les couples d'objets de C , - s i I est la traite d'ordre 0 suivante: si J est la traae d'ordre 0 suivante: M » lO QU'EST-CE QU'UN TVRE DANS UNE CATEGORIE ? et si H est l'homomorphisme canonique de I dans J , alors un type indue tif de syntaxe H est une structure de catégorie die Peano sur C ([Coppey84]), -si I est vide , un type inductif (resp. projectif) dans C de syntaxe H (de source I et de but *X ) s'identifie à un modèle initial (resp. terminal) de *X dans C i un tel type peut être dit clos (exemples: un objet initial, un objet terminal, un objet des entiers naturels dans C ). Catégorie des sémantiques d'un type. Soit H : I -* JT une syntaxe de types. La catégorie Sém*(H) (resp. S ô m " ( M ) des sémantiques catégoriques du type inductif (resp, projectif) de syntaxe H est définie comme suit: - ses objets sont les couples (C,*) tels que: + C est une petite catégorie, + x est un type inductif (resp. projectif) dans C de syntaxe H , - les flèches de ( C l f T,) vers ( C 2 , ta) sont les foncteur s F: d -* C 2 vérifiant: Mod( J", F) o Ti » T 2 o Mod( X, F). Si £ « (£~# S*') est un couple de classes de syntaxes de types, on définit de façon analogue une catégorie S e m ( E ) , Par exemple, la catégorie C a r t f N des petites catégories cartésiennes fermées avec objet des entiers naturels apparaît comme étant S e m ( (H,, H2, H 3 ) , (H*) ),où : - Hi spécifie un objet terminal, - H 2 spécifie des cônes produit, - H 3 spécifie des diagrammes "exponentielle", - H* spécifie un objet des entiers naturels, (bien entendu, H* spécifie en particulier un objet terminal; on pourrait donc penser faire l'économie de Ht ; ce n'est pas une bonne idée, car on perdrait une propriété remarquable du système £ : son caractère héréditaire - voir [Lair87]). Mentionnons pour finir quelques résultats sur la structure de "sémantique catégorique d'un système de syntaxes de types S " comparée à celle de catégorie et à celle de graphe, PART, X: QU'EST-CE QU'UN TYPE DANS UNE CATEGORIE ? Les questions (qui sont évidemment liées à certains problèmes d'équationnalité) se posent ainsi: l.a. le foncteur d'oubli canonique de S e m ( Z ) dans C a t admet-il un adjoint à gauche ? I.b. ce foncteur est-il, de plus, monadique (autrement dit: S e m ( S ) est-elle une catégorie doctrinale)? 2.a. le foncteur d'oubli canonique de S e m ( E ) dans G r a p h admet-il un adjoint à gauche ? 2.b. ce foncteur est-il, de plus, monadique (autrement dit: S e m ( E ) est-elle une catégorie graphique)? Les réponses aux questions l.a et 2.a sont oui (pourvu que S soit héréditaire): toute catégorie petite (resp. tout graphe petit) engendre librement une sémantique catégorique pour Z ([Lair87]) . En revanche, les réponses aux questions l.b et 2,b dépendent de Z , Voici quelques résultats connus: - la catégorie des catégories à choix de X-limites inductives et V-limites projectives (où X et Y sont des classes de compographes) est doctrinale ([Lair75]), - la catégorie des catégories à choix de produits (resp. sommes, noyaux, conoyaux, produits fibres, sommes amalgamées) est doctrinale et graphique ([Burronidl], [Coppey-Lair8S]), - la catégorie des catégories de Peano est doctrinale, mais non graphique ([Coppey-LairSS]), - la catégorie des catégories cartésiennes fermées est doctrinale et graphique ([MacDonald-Stone84] , [Ageron-Even88]). Ce genre de questions peut être abordé systématiquement par la théorie des esquisses, qui fournit des critères généraux et commodes pour y répondre ([Lair75] , [Lair79]) . PARTIE II: SEMANTIQUE GEOMETRIQUE DU SYSTEME F On sait (voir par exemple le chapitre 1 de [Lambek-Scott86]) que la structure de catégorie cartésienne fermée permet d1 interpréter les types et les termes du X-calcul typé, ou encore, via 1'isomorphisme de Curry-Howard, les propositions et les preuves de la logique intuitionniste, En 1970, Jean-Yves Girard introduisait une extension du X-calcul typé, le système F ([Girard7l]): il s'agit de la version fonctionnelle de la logique (propositionnelle) intuitionniste du deuxième ordre. La question se pose alors de déterminer un cadre mathématique général, du type "catégorie + une certaine structure algébrique", permettant de donner un sens (formel) aux types et aux termes du système F. Cette interprétation devra préserver les idées sémantiques natves suggérées par la logique (type = ensemble de preuves) ou par l'informatique (type » ensemble d'algorithmes): elle devra aussi être fidèle au principe qui pour nous est l'esprit même du système F; présenter chaque type comme construit conformément à sa géométrie intrinsèque, (Notons que le formalisme à base d'hyperdoctrinés, introduit dans [Seely87] et repris dans [Pitts87] et [Coquand-Ehrhard87], ne répond pas à ces préoccupations; de plus, les types y sont des foncteur s internes - , ce que nous avons critiqué dans la discussion précédente. ) 1. Types: taxinomi Syntaxe des types du système F, Voici la syntaxe des types du système F, dans sa version la plus récente et la plus dépouillée ([Girard86] , [Girard88]). On se donne un ensemble infini H * { X , Y ,,,,} appelé ensemble PART. II: SEMANTIQUE Û C O M S T R I Q U E O U S Y S T E M E F" des variables de type, On définit (inductivement) comme suit l'ensemble F-Typ(W) des types du système F en les variables de W , ainsi que pour tout type A l'ensemble W(A) des variables de type libres dans A : - s i X € V , alors X e F-Typ(U) et W(X) » (X) , -si A,, Aa e F-Typ(W), alors A, * A 2 e F-Typ(W) et W(A, ** Aa) » U(Ai) u W(A 2 ) , -si X e W et si A € F-Typ(W), alors VX.A e F-Typ(U) et W(VX.A) • W(A)\CX>. Cette syntaxe est extraordinairement simple: hormis les variables (et les parenthèses), elle admet exactement deux symboles =* et V , Nous convenons que =* est prioritaire sur Taxinomie, La syntaxe précédente induit la taxinomie suivante: - nous appellerons =*-types (resp. V-types) les types de la forme AT =* A 2 (resp. VX.A), On peut qualifier cette taxinomie de superficielle, en ce sens qu'elle ne tient compte que du dernier symbole introduit encore celui-ci n'a-t-il pas nécessairement de signification profonde: sémantiquement, nous pourrons identifier tout type A au =>-type (VX.X^X) => A ainsi qu'au y-type VX. (A =* X) =* X (si X n'appartient pas à U(A)), La thèse générale qui préside à notre interprétation peut se résumer dans les trois points suivants; - le symbole =» permet certaines constructions de types de nature projective (stuctures co-libres), - le symbole V permet certaines constructions de types de nature induetive (stuctures libres), - c'est justement la possibilité d'entremêler ces symboles, d'alterner constructions projectives et constructions inductives, qui donne au système F son énorme pouvoir expressif en matière de types, On mesure facilement, par exemple, la supériorité de F sur le langage de programmation ML: en effet, celui-ci n'accepte que les quantifications prénexes (toute occurence de V doit PA 14 PART. Ils SEMANTIQUE GEOMETRIQUE O U S Y S T E M E F" précéder toute occurence de =» ), ce qui empêche notamment de typer convenablement l'addition entre entiers de Church ([Huet88]). Par ailleurs, la possibilité d'emboîter, à la façon des poupées russes, constructions projectives et constructions induetives est tout à fait caractéristique des notions de type dans une catégorie, développées dans la première partie de cet article. Nous allons donc montrer ici que les types du système F peuvent se traduire dans ce formalisme catégorique, plus puissant et plus symétrique, tout en préservant les idées sémantiques naïves transmises par la tradition orale. Tous les types de F prendront alors, nous l'espérons, une signification, une pure écriture signifiant à l'esprit la formation d'une image géométrique. 2. Types: géométrie, Aperçu sur la géométrie des types. Soit A un type du système F, avec W(A) « CX,, ...X,.}. Nous appellerons géométrie de A un certain diagramme de trames et d'homomorphismes de trames de la forme: W(A) où W(A) *i # • • • H(A) -» G(A) est la trame discrète d'ordre WA) +- 1 0 dont les objets sont i X|», Le rôle des homomorphismes H(A) et W A ) est de pointer à l'intérieur de la trame <3(A) les emplacements des variables libres X,, ... , X. et celui du type A , "déshabillé11 de toute structure. On notera abusivement W A ) l'objet WA)(0), PA IS PART, Définition Ils SEMANTIQUE GEOMETRIQUE OU SVSTEME F» de la géométrie des types. Voici la définition précise de <3 , par - 1*" cas: A * X est une variable de type. Dans ce cas, on pose: <3(A) » W(A>, H(A) » Idwi 1KA) - X. - 2 * ~ cas: A « Ai =» Aa est un =»-type. Dans ce cas, soit la graphotrame d'ordre 1 suivante: E Alors, on pose: <3(A) « <3(AO + E + <3(A*) où les symboles "+• indiquent que l'on fait une somme amalgamée dans laquelle: - on identifie les objets WAi) et E 2 ainsi que les objets KAa) et Eo i -pour tout Y e W(AT ) A W(A*), PA 16 on identifie les objets PART. II! SEMANTIQUE GEOMETRIQUE DU SYSTEME F H(A,HY) et H(A2)(Y). Si l'on note I,, I0> Iz les trois inductions de <3 : W -+ <3(A) est défini sans ambiguïté par; H(A)(Y) = X J C H C A J H Y ) ) , pour tout Y e VKAj) . Enfin, on pose: « A ) • I0 (A„ => A° 0 ) ... ), Ai « A'4 * (A2t = » . . . * (A*1* =» A° t ) ... ) Pour n e N et F°, fi Soit K - C(i, j ) / H i < n <3(A) - F < k , . et 0 + S t i . j ^ - K <3(AJi), où le symbole "+" indique que l'on effectue une somme amalgamée dans laquelle: - pour tout (i,j) e K , on identifie les objets W A J t ) et FJt , PA 17 PART. II: SEMANTIQUE GEOMETRIQUE DU SYSTEME P" - à chaque fois qu'il existe (i,j) € K , (i',j') e K et Y e W(A J 4 ) n U(A j a t .) , on identifie les objets H(A"t)(Y) et H(A J, i.)(Y). Pour (i,j) € K , notons donc IJA V induction de <3(AJi) dans <3(A) , Alors H(A) : W ( A ) -* <3(A) est défini sans ambiguïté par: H(A)(Y) » IMH(A'i>> f F»ur tout Y € W(A**) . Enfin, on pose: 1KA) - I°o(TtA°o)) . Remarques, Pour conclure, notons que: - les trames de la forme G ( A ) sont des graphotrames, - les (grapho)trames El et R(ki, ... k n ) sont elles-mêmes de la forme <3(A) : ceci révèle bien que le système F est fondé sur le choix de certains (constructeurs de) types, choix qui, finalement, est à peine moins arbitraire que celui de types atomiques clos dans le X-calcul typé du premier ordre, mais comment y échapper tant qu'une syntaxe de types reste une écriture ? 3. Types: sémantique, Préliminaires, Conformément au programme présenté dans la première partie de cet article, nous allons maintenant chercher à définir 1'assertion: la catégorie C est une sémantique pour le type A. En fait, nous nous intéresserons au cas où A est un V-type, Bien entendu, le cas des =»-types pourrait être traité de façon rigoureusement symétrique, mais il est beaucoup plus PART. II: SEMANTIQUE GEOMETRIQUE OU SVSTEME P banal, car il se ramène simplement à demander l'existence de certaines exponentielles. Nous supposerons donc toujours, a priori, que C est une catégorie cartésienne fermée, ce qui permettra de mettre l'accent sur le constructeur le plus original: V. Soient donc A un V-type du système F et C une catégorie cartésienne fermée, On dispose des deux ensembles suivants: - Mod(<3(A), O = ensemble des modèles de <3(A) dans C , - Mod(UKA), C ) • ensemble des assignations des variables libres de A dans C , ainsi que de l'application "assignation sous-jacente": Mod(H(A), C ) : Mod(G(A), C ) -» M h* Mod(W(A), C ) . M o H(A) Remarquons que cette application est l'induction aux objets du foncteur d'oubli U(A) = C H(A) <3(A) : C -* C W(A) Une idée naturelle consisterait à dire que C est une sémantique pour le type A si, et seulement si, U(A) admet un adjoint à gauche L(A). Mais cette condition est beaucoup trop forte: elle impose en effet que A soit "covariant" par rapport à toutes ses variables. C'est pourquoi il faut se retourner vers des définitions ensemblistes, Types schématisables et sémantisables. On dit que A est un type schématisable dans C si, et seulement si: - l'application Mod(H(A), C ) est surjective, ceci est équivalent à dire qu'il existe (au moins) une application: choix(A) : Mod(UKA), C ) vérifiant la condition (a) suivante: -+ Mod«3(A), C ) , PART. a) IX: SEMANTIQUE GEOMETRIQUE OU SYSTEME P Mod(H(A), O On dit que A o choix(A) » Id Hod(W(A),C) est sémantisable dans C si, et seulement si: - on peut choisir cette application de sorte que soient vérifiées la condition (a) précédente et la condition (b) suivante: b) V N e Mod(W(A), C ) , V M c Mod(Q(A), C ) , MoH(A) » N => 3 ! & : choix(AHN) -» M, <3(A) C telle que &oH(A) « Id» . Avec la terminologie de la première partie , il est clair qu'un V-type A est sémantisable dans C si, et seulement si, C est sous-jacente à une sémantique catégorique du type inductif de syntaxe H(A) : on dit alors que celle-ci est une sémantique catégorique de A et l'on pose S é m ( A ) » Sém^(H(A)) . Par abus de langage, on dira aussi que C est une sémantique catégorique pour le type A si C est la catégorie sousjacente à un objet de S é m ( A ) ; mais cet abus peut être dangereux I En effet, les deux notions (avec ou sans choix) sont structurel lement très différentes (et sont les objets de catégories qui ne sont même pas équivalentes), Enfin, on laisse le lecteur préciser lui-même ce qu'il faut entendre par sémantique catégorique pour un =*-type. Exemple, La classe d'exemples la plus importante est celle des types "naturels" qui seront étudiés en détail dans la section suivante. Donnons seulement ici un exemple très différent, inspiré de [GirardSS], Considérons le type (clos): A 0 - VX.(X =* (X =* X)) => (((X => X) => X) => X). La géométrie de ce type est: PART. IIS SEMANTIQUE GEOMETRIQUE DU SVSTEME P G(A0) • WAo) » X . Par définition, un modèle M de <3<À0> dans une catégorie cartésienne fermée C s'appelle une \-structure dans C (pour la raison que ces structures permettent d'interpréter la formation des termes du X-calcul pur, voir [Barendregt84])a Le type A 0 est clairement schématisable dans toute catégorie cartésienne fermée C , car on dispose toujours de la Xstructure dégénérée sur l'objet terminal, Il est sémantisable si et seulement si C possède une "X-structure initiale". Notons au passage que si une X-structure vérifie C(H(r))oM(s) » Id , (où C : Hom(M(X)*M(X), H(X)) *» Hom(H(X), M(X)" CX> ) est la bijection de Curry), alors M valide la ^-conversion et, dans ce cas, on dit que M est une \-algèbre (voir [Barendregt84]), Il est facile de voir que les X-algèbres sont aussi les modèles d'une certaine trame, mais celle-ci n'est pas la géométrie d'un type du système F. Présentation équationnelle des types semantisables, Nous allons montrer maintenant, en utilisant des méthodes de [Lair79], que la notion de type sémantisable peut être présentée de façon purement équationnelle. Fixons quelques notations: - O ( A ) est la trame discrète d'ordre 0 qui a les mêmes objets que Gi(A) , - il est facile de construire, à partir de deux copies de O ( A ) , PART. II! SEMANTIQUE GEOMETRIQUE OU SYSTEME P une trame 0 2 ( A ) dont les modèles s'identifient aux transformations naturelles entre modèles de O ( A ) , - i l est facile de construire, à partir de deux copies de <3(A) , une trame <3 2 (A) dont les modèles s'identifient aux transformations naturelles & entre modèles de <3(A) qui vérifient SoH(A) = Id , - de même, il est facile de construire, à partir de trois copies de <3(A) , une trame Q 3 ( A ) dont les modèles s'identifient aux triangles commutâtifs de telles transformations naturelles, (On constate que Gi2(A) , <33(A) ne sont plus nécessairement des graphotrames, ) De plus, on utilisera les homomorphismes de trames suivants, où les schémas symbolisent l'injection de ce qui est en gras dans le tout (par exemple, D(A) est l'injection de la seconde copie de <3(A> dans <32(A) >: ->• - D(A) <3(A) Q2(A> injection - 6(A) G(A) Q2(A) injection - M(A) 02(A) Q2(A) injection - B(A) W(A> -» Q(A) injection canonique - P(A) O(A) -» Q(A) injection canonique - I(A) 02(A) -* O(A) i d e n t i f i e les objets homologues - E(A) G2(A) -* Q3(A) injection - F(A) G2(A) -» e3(A> injection - J(A) G2(A) -> G3(A) injection «•—••••>> > > — j » > —^r Dans ces conditions, on dispose du théorème qui suit. - Théorème, Soient A un W-type du système F et C une catégorie cartésienne fermée, Le type A est sémantisable dans C si et seulement si il existe trois applications". choix(A) : Mod(W(A), C ) Mod(G(A), C ) PART. vérifiant a) IX: SEMANTIQUE QEOMETRIQUE DU SVSTEME P fact(A) : ModCQ(A), C ) -* Mod«32, C ) unic(A) : Mod(Q2(A), C ) -» Mod«33CA>, C ) les sept équations suivantes: Mod(H(A>, O o choixCA) » Id ModCW, C ) bi) Mod(D(A>, C ) o fact(A) = Id Mod(G(A>, C ) b 2 ) Mod(6(A>, C ) o fact(A) = choix(A) o Mod(B(A), C ) D3) Mod 0 fact(A) 0 choix(A) Mod(KA), C ) 0 Mod(F(A>, C ) 0 choix(A) b*) Mod(E(A), C ) 0 unic(A) « fact(A) 0 Mod, C ) b s ) Mod(F(A), C ) 0 unie (A) = Id Mod Mod(J(A>, C ) 0 unic(A) » fact(A) 0 Mod(DCA), C ) . - Preuve, L'assertion b) se réécrit ici; V M € Mod«3(A), C ) 3! & : choix(A)(MoH(A)) -* M tel que SoH(A) • IdMeH. Soient donc M e Mod«3(A>, C ) et N » choix(AXMoH). Alors b*> et b a ) expriment exactement l'existence d'(au moins) une factorisation 8 = fact(AXM) : N -» M , telle que ôoH(A) soit égal à IOVIOH . De plus, les équations b*), b s ), b s ) jointes à b 3 ) traduisent équationnellement que toute autre transformation naturelle S' : N -» M , telle que &'oH(A> soit égale à IdMoH 1 est égale à & : il suffit de vérifier que ce sont des conditions nécessaires, puis de constater que l'application de unie(A) à &' donne le diagramme suivant: f»A 2 3 PART. qui force IIî SEMANTIQUE & » &' , F i n de «EOMCTRIQUE OU la SVSTE preuve, Remarques, Les trois lois (ou opérations algébriques) qui apparaissent dans la présentation équationnelle précédente ont pour arités certaines trames: Uf(A), G(A), GS(A), Nous dirons qu'on a une présentation équationnelle tramique. Pour répondre aux préoccupations des informaticiens, il serait intéressant d1 "éliminer la composition11 de cette présentation équationnelle, autrement dit de disposer d'une présentation équationnelle graphotramiquei une telle présentation dispense de devoir tester la commutativité de diagrammes. Or, si W ( A ) et G ( A ) sont effectivement des graphotrames, nous avons noté que G 2 ( A ) n'en est pas une, Toutefois, dans certains cas, la donnée d'un modèle de G 2 ( A ) équivaut à celle d'un modèle d'une graphotrame G 3 ^ 2 ( A ) : c'est le cas si A est un type naturel (voir le chapitre suivant). On peut alors écrire une présentation équationnelle qui est de la même nature que celle de la structure de catégorie cartésienne fermée dans [Curien86] ou [Lambek-Scott86], Mais pour A = A 0 , ceci n'est pas faisable. Notons, au passage, que dans [Lambek-Scott86] (resp, [Coquand-Ehrhardd?]), les auteurs fournissent une "présentation équationnelle" des catégories cartésiennes fermées (resp, des hyperdoc tri ries de Seely) en se réclamant de la "notion générale" (resp, de la "tradition") des algèbres graphiques de [Burronidl], Hais les présentations équationnelles qu'ils indiquent ne suffisent absolument pas à prouver qu'on a bien des algèbres graphiques, en particulier parceque ce sont des présentations graphotramiques et non graphiques! On trouvait déjà une mise en garde à ce sujet dans [Dubuc-Kelly83], Pour une preuve du fait que les petites catégories cartésiennes fermées sont les objets PA 2 4 PART. IIî SEMANTIQUE GEOMETRIQUE OU SVSTEME P d'une catégorie d'algèbres graphiques voir [MacDonald-3tone86] ou, pour une preuve détaillée, [Ageron-Even88], 4. Types naturels. Les types que nous appellerons naturels sont probablement les types les plus intéressants du système F, Ils permettent de représenter, en particulier, toutes les structures de données (inductives) usuelles: voir [GirardSS], D'autre part, ils obéissent à des propriétés structurelles simples que nous allons étudier, Notations et conventions, Fixons tout d'abord quelques notations et conventions, systématiquement utilisées dans ce n*4, mais aussi aux n°* S et 6. Soit A un V-type du système F , On considère les homomorphismes de trames; W A ) : <1> « A ) : <2> -+ -» G ( A ) déjà défini, G2(A) tel que «A)(0) = G(A)(rtA>) et «A)(1) » D(A)(WA>), Si C pose: est une sémantique catégorique (avec choix) pour A , on £bgJL^(A) - Mod< W A), C ) o choix(A) làCJtCA) s Mod(ttA), C ) o fact(A). On notera encore plus simplement & = cJhûixXA), Alors: (i) si A est clos, & s'identifie à un objet de C , que l'on notera encore A. * (ii) si A a exactement une variable libre X, EL s'identifie à une application de Ob(C) dans Ob(C), que l'on notera encore PA 2 « PART. II: SEMANTIQUE GEOMETRIQUE OU SYSTEME P &. (iii) si A a au plus une variable libre X , on convient d'identifier & à une application de O b ( C ) dans O b ( C ) , qui est celle définie en ii) si A a exactement une variable libre et qui est l'application constante de valeur & si A est clos , Enfin on utilisera les mêmes lettres X, Y, ... pour désigner tantôt des variables de type, tantôt des objets de C . Variables complètement positives. Soit A un type du système F . On définit inductivement l'ensemble CP(A) des variables de type couÊplètement positives dans A par: CP(X) * W CP(Ai =» A 2 ) - CP(A 3 ) \ W(A,) CP(A) = A CP(A'±) si A est un V-type, (i, j)€K Types naturels. On dit qu'un V-type A du système F est naturel seulement si il vérifie les deux conditions suivantes: - A « VX.Ai =» (Aa =» ... =>(A„ =* X) ... ) où chaque type A* est de la forme: A± » A1* ** (A2! s» ... ^(A* 4 i => X) ...) avec si, et n e N kt € N X complètement positive dans chacun des A ± J , - tous les V-sous-types de A sont naturels, - Théorème préparatoire, Soit A un type naturel du système F admettant au plus une variable libre X, supposée complètement positive dans A , Soit (C,choix(A)) une sémantique catégorique pour A , Alors, l'application PA 3« II: SEMANTIQUE GEOMETRIQUE OU SYSTEME P &Ob(C> -* Ob(C) est l'induction aux objets d'un endofoncteur de C , - Preuve, Soit x : X -r X' une flèche de C . On voudrait définir &(x) : &(X) -» &(X') . On dispose de M , modèle de G ( A ) initial parmi ceux qui sont construits sur X , et de H' modèle de G(A) initial parmi ceux qui sont construits sur X' , A partir de 111 et de x , il est possible de construire un autre modèle M, de G (A) construit sur X et tel que l'on ait M(rtA)) » &(X') , Alors il existe une unique transformation & : M -* Mi telle que &x = Idx ; on obtient donc une flèche de &(X) vers &(X') que l'on appelle &(x) . La fonctorialité se vérifie alors facilement, Fin de la preuve. C Remarquons qu'il est, de même, bien connu que pour tout objet de C , l'application: Ob(C) -* X *-* Ob(C) Xe est l'induction aux objets (démonstration analogue), Sémantisabilité (tes types d'un endofoncteur de C A C. est naturels, Nous avons d'abord la proposition suivante, - Proposition, Soit A un type naturel. Alors schématisable dans toute catégorie cartésienne fermée - Preuve, Il existe toujours un modèle vérifiant M(«A)) » 1 , Fin de la preuve, Considérons maintenant un type naturel A , que, pour simplifier, nous supposerons clos, Soit C une catégorie cartésienne fermée qui soit déjà une sémantique (avec choix) pour tous les types A 4 t : d'après le théorème préparatoire et la remarque qui le suit, on peut associer à chaque AJt un PA 2 T PART. II: SEMANTIQUE GEOMETRIQUE OU SYSTEME P endofoncteur de C noté P i , On considère alors la famille d'endofoncteurs (T,, ... ,T„) où T 4 » T 1 ! x ... x Tki* . Enfin, on note Alg(Ti, ... , T„> la catégorie ainsi définie: - ses objets sont les cônes indue tifs de C de la forme x « (Xt : Tt(X) -* X ) 1 < 1 < r % - une flèche de x « (xt : Tt(X) -» X) vers y » (y* : Ti(Y) -p Y) est une flèche h : X -* Y telle que h.Xt » yi.Ti(h) pour l(i dans C si et admet un objet est sémantisable si, et seulement si: G(A) C admet un objet initial, G(A) Or les catégories C et Alg(Ti, ,,, , T„) sont isomorphes (remarquer qu'une transformation entre deux modèles de G(A) est entièrement définie par sa trace h en WA)). Fin de la preuve, Nous pouvons également établir les deux lemmes qui suivent, - Lemme 1, Soit T un endofoncteur d'une catégorie C . Supposons que Alg(T) admette un objet initial a: T(A)-»A . Alors a est un isomorphisme de T(A) sur A . - Preuve, Par initialité de a, il existe une unique flèche h : A -* T(A) telle que h.a » T(a).T(h) , ou encore h.a « T(a,h) . On en déduit l'égalité suivante: (a,h),a a a,T(a,h) . Hais on a aussi évidemment: IdA.a a IOV , En utilisant à nouveau l'initialité de a , on conclut que a, h a idA et on obtient aussi h, a a T(a.h) a T(IdA) a IÛV . Alors a est bien un isomorphisme, d'inverse h , Fin de la preuve. PA : PART. II: SEMANTIQUE GEOMETRIQUE OU SYSTEME P - Lemme 2, Soient Tt, .,, , T„ des endofoncteurs d'une catégorie C , Supposons que pour tout objet X de C , la somme Ti(X) + ... +Tn(X) existe, et que Alg(Ti, .,, ,Tr») admette un objet initial a , Alors a est un cône somme, -Preuve, Soit £ le foncteur T, + .,, +T„ : par définition d'une somme, on a Alg(Ti, ... ,T„) S Alg(Z) . Supposons maintenant a = (a,, ... ,a„) initial dans Alg(Ti, ,,. ,T„) , Alors (ai, ,. ,a„) est initial dans Alg(E) ; par le lemme précédent, c'est un isomorphisme, d'où il résulte que (ai, ... , a„) est un cône somme. Fin de la preuve, On en déduit le corollaire qui suit, - Corollaire, Si le type naturel et si C admet les sommes finies, de l'équation de point fixe: A est sémantisable dans C alors l'objet A est solution X 3 T,(X) • . . . + T„(X) - Preuve, Ceci résulte immédiatement lemmes précédents. Fin de la preuve. X c Ob(C), du théorème et des deux Exemples, 1) Considérons le type naturel clos: ent » vx.X => ((X => X) *> X), Ce type est sémantisable dans C si, et seulement si, C admet un "objet des entiers naturels", Si C admet de plus des sommes finies, l'objet N a ent satisfait l'équation N S 1+N . Pour ces raisons, ent est appelé "type des entiers naturels" (on donne parfois ce nom au type ent* a VX.CX => X) => (X »> X) qui a la même géométrie), 2) Considérons le type naturel clos nil = VX.X , Ce type est sémantisable dans C si, et seulement si, C admet un objet initial 0 , On a alors nil s 0 et nil s'interprète comme "type vide". 3) Considérons le type naturel clos: PA 2 9 PART. II! SEMANTIQUE GEOMETRIQUE DU 8YSTI bOOl a VX.X a> (X a>X) , Ce type est sémantisable dans C si, et seulement si, la somme 1 + ] existe , On a alors booL S 1 + 1 et bool s'interprète comme "type des booléens". 4) Considérons le type naturel à deux variables libres: somme(Y,Z) a VX.(Y =* X) => ((Z =* X) =* X) . Ce type est sémantisable dans C si, et seulement si, C a les sommes de deux objets, On a alors, pour Y et Z e O b ( C ) , Sûmffl£ ( ( X => C X => X)) => X) . Si C en est une sémantique et admet les sommes finies, arbrebin est solution de X s 1 + Xa . Et arbrebin s'interprète comme "type des arbres binaires". 6) Considérons le type naturel à une variable libre: list(Y) » vx.X => ((X => (Y => X)) «> X). Si C en est une sémantique et admet les sommes finies, et si Y e Ob(C) , Usl(Y) est solution de X s 1 + YxX . Et list(Y) s'interprète comme "type des listes d'entités de type Y ". 7) Considérons le type naturel à trois variables libres: arbre (S,fi,V) » VX. (V => X) => ((fi => ((S => X) => X)) => X) Si C en est une sémantique et admet les sommes finies et si S, fi, V € Ob(C), alors arbres. fif V) est solution de X S V + fixX3. Et arbre(S, fi, V) s'interprète comme "type des arbres à embranchements de type S , à sommets internes de type fi et à sommets externes de type V ", 8) Considérons le type naturel clos: PA 3© PART. II: S E M A N T I Q U E GEOMETRIQUE OU SYSTEME P on a vx.X => ((X =* X) =» (((ent *> X) => X) =* X)) . Si C en est une sémantique et admet les sommes finies, on est solution de X S 1+X+X" , N étant un objet des entiers naturels, Dans [Coquand-Huet87], on est interprété comme "type des ordinaux", ou plus précisément "type des ordinaux dénombrables présentés comme limites de suites fondamentales de Cantor", 9) Considérons le type naturel clos: arbrefini a vX.dist(X) =* X) => X, Si C en est une sémantique, l'objet arbrofini est solution de X s lisi(X) et arbrefini s'interprète comme "type des arbres abstraits à embranchements finis", 10) et 11), Le cas des types: un » VX.X =* X prod(Y,Z) a VX,(Y => (Z => X)) s> X est un peu particulier. Ces types sont sémantisables dans toute catégorie cartésienne fermée, avec un = 1 et PLOJKY, Z) a y*Z pour Y, Z e 0 b ( C ) . Il est clair que ces types sont, "profondément", des types projectifs et non inductifs. Hais une "astuce" (inspirée, paraitil, de Russe1) consistant à leur ajouter un étage projectif "artificiel" permet de les intégrer au système F. 5. termes. Préliminaires, Voici quelle est l'interprétation informatique (algorithmique) des types de la forme VX.A(X) : le fait que VX,A(X) soit sémantisable dans C exprime que les algorithmes uniformes de type A(X) (j'entends par là les algorithmes qui PART. II: SEMANTIQUE GEOMETRIQUE OU SYSTEME P existent "à coup sûr", quel que soit l'objet X de C ) peuvent être décrits au moyen de certains algorithmes d'un certain type clos, Ceux-ci peuvent être vus comme des substrats opératoires abstraits, mais implantables dans le langage de C , Dans le système F , les algorithmes sont représentés par les termes: voir leur syntaxe dans [Girard 88], Nous allons donc dire un mot de la sémantique des termes du système F : nous nous bornerons ici à l'interprétation (dans un cas particulier suffisamment générique) des schémas d'extraction et d* abstraction universelle. Extraction, Soient A un type du système F ayant au plus la variable libre X et C une sémantique catégorique pour A et VX.A . On suppose que 1 est générateur dans C . Alors on a la règle d'extraction: u : 1 -» vx A X € Ob(C) c((u,X) : 1 -» &(X) Cette opération correspond à la construction suivante Soit u : 1 -*• v x A , Considérons l'application: £L. : ModCG(VX.A), C ) -» FKC) N H» fâ£jL(VX.A)(M).u Pour tout objet X de C G(VX,A), une application: , £L induit, par définition de £,,* : TT Hom ( TT â J t(X) , â 0 ± (X)) -* Hom (1, â°0(X)) Uiîn C Ujtkt C donc, par bijection de Curry, une application: EL.x~ : Hom (1 , TT a ± (X)) -* Hom (1 , Û.°0(X>) . PART. II: SEMANTIQUE GEOMETRIQUE OU SYSTEME P Comme on suppose que 1 est générateur, celle-ci détermine à son tour une unique flèche de C : c~(u,X) : TT &±(X) -* û°o (X =* list(X)). - Théorème, Le type L^ n'est pas ensembliste, - Preuve, Il est clair que list(-) est un constructeur de type ensembliste, c'est à dire que pour tout ensemble X , il existe dans E n s un "objet des listes d'entités de type X ": i X ( ) -* De plus, chaque 1 € déterminée, telle que: append lial(X) ^ * listm X iis±(X)xx a une longueur L0NG(1) € N X X L0N6(( ) ) a o et LONG (append (Ç,x)> a LQN6(«)+1 . (Remarquons en passant que le terme AX,appendx est précisément de type Li , tandis que AX, ( )* est de type U a VX.list(X) qui, lui, est ensembliste.) Supposons que Li soit un type ensembliste, ce qui revient à dire que la trame G(Li) admet un modèle initial dans E n s , Alors il existe (A , a e A , ce e Usi(A)) tel que pour tout (X , x € x , ç e JJLâi(X)) il existe un et un seul triplet d'applications ( h j k A -P X , Uai(A) -P U s K X ) , Usi(A)xA -» iiai(X)xx ) tel que PA 3 * PART. II: S E M A N T I Q U E GEOMETRIQUE OU SYSTEME P A X j(( ) ) a ( ) j o appendA a appendx o k j o pr1 u,tt . A a praiimtcx>, x o k h(a) » x j(«) = %. Nous allons montrer par récurrence que ces conditions impliquent: VX e Hst(A) , LONG(j(X)) a LONG(X), Si X = ( >A f c . e s t ciaip, Si X a appendA(X0i a 0 ) , où on suppose L0NG(j(Xo)) • L0NG(Xo) # alors: j(X) a j(append*(X0, a 0 )) a appendx(k(X0i a 0 >) a appendx(j(pr1(X0i a 0 ) , h(pr*(X0, a0))) a appendx(j(X0) # h(a0)) et donc L0N6(j(X)) a L0NG(j(X0))+1 » L0NG(Xo>+1 = LONQ(X). En particulier, on doit donc avoir LONG(a) a LÛNG(Ç) , liais S peut avoir n'importe quelle longueur, d'où la contradiction. Fin de la preuve. On a cependant le résultat plus faible suivant: - soit (X,x,Ç) avec LONG(Ç) = q et supposons (A,a, (X => list(X)) ne peuvent être décrits sans recourir à une notion extérieure, à savoir la longueur de la liste prise en argument. REFERENCES [Ageron-Even] BIBLIOGRAPHIQUES Pierre Ageron et Christian Even: Etude de la catégorie des catégories cartésiennes fermées, à paraître. [Barendregt84] Hendrik Pieter Barendregt; The lambda calculus, deuxième édition, North-Holland, 1984. [BurroniSI] Albert Burroni: Algèbres graphiques, Cahiers de Topologie et Géométrie Différentielle, vol. XXI1-3, Amiens, 1981. [Coppey84] Laurent Coppey: Catégories de Peano, catégories algorithmiques, récursivité, Diagrammes 12, Paris, 1984. [Coppey-Lair85] Laurent Coppey et Christian Lair: Algébricité, monadicité, esquissabilité et non-algébricitê, Diagrammes 13, Paris, 1985, [Coquand-Huet87] Thierry Coquand et Gérard Huet: Concepts mathématiques et informatiques formalisés dans le calcul des constructions, in Logic Colloquium 85, edited by Paris Logic Group, NorthHolland, 1987. [Coquand-Ehrhard87] Thierry Coquand et Thomas Ehrhard: An equational présentation of higher order logic, in Proceedings of Category Theory and Computer Science, edited by D, H. Pitt, A\ Poigne, D. E.Rydeheard, Leet. Notes in Corap. Sci. 283, Springer, 1987, [Coquand] Thierry Coquand: Catégories of embeddings, à paraître, PA 37 REPERENCES BI SI-1OGRAPHIQUES [Curien86] Pierre-Louis Curien: Categorical combinators, Sequential Algorithms and Functional Programming, Pitman, 1986. [Dubuc-Kelly83] Eduardo Dubuc et Max G, Kelly: A présentation of topoï as algebraic relative to catégories or graphs, Journal of Algèbre, vol. 81-2, 19®3. [Ehresmann68] Charles Ehresmann: Esquisses et types des structures algébriques, Bul. Znstit, Polit. Iasi, voITXIV, 1968. [Freyd-Girard-Scedrov-Scott] Peter J, Freyd, Jean-Yves Girard, André Scedov et Philip J, Scott: Semantic parametricity in polymorphic X-calculus, à paraître. [Girard7l] Jean-Yves Girard: Une extension de l'interprétation fonctionnelle de Godel à l'analyse et son application à l'élimination des coupures dans l'analyse et la théorie des types, in Proceedings of the second Scandmavian Logic Symposium, Oslo, 1970, edited by J.E Fenstad, NorthHolland, 1971, [Girard86] Jean-Yves Girard: The System F of variable types, fifteen years later, Theoretical Computer Science, vol. 45, 1986. [Girard] Jean-Yves Girard: Typed X-calculus, Cambridge Tracts in Theoretical Computer science, à paraître, [Guitart-Lair80] René Guitart et Christian Lair; Calcul syntaxique des modèles et calcul des formules internes, Diagrammes 4, Paris, 1980, PA 39 REPERENCES BI Bt_ IOGR APHIQUES [Huet] 6érard Huet: A uniform approach to type theory, à paraître. [Lair75] Christian Lair: Esquissabilité et triblabilité, 2 " colloque sur les catégories, Amiens 75, Cahiers de Topologie et Géométrie Différentielle, vol. XVI-3, Amiens, 1975. [Lair87] Christian lair: Trames et sémantiques catégoriques des systèmes de trames, Diagrammes 18, Paris, 1987. [Lair79] Christian Lair: Condition syntaxique de triplabilité d'un foncteur algébrique esquissé, Diagrammes 1, Paris, 1979, [Lambek-Scott86] Joachim Lambek et Philip J, Scott: Introduction categorical Press, 1986, to logic, higher Cambridge order Univ, [MacDonald-Stone84] John MacDonald et Arthur Stone: Topoî over graphe, Cahiers de Topologie et Géométrie Différentielle, vol. XXV-1, Amiens, 1984. [Pitts87] Andrew M. Pitts: Polymorphism is set-theoretic constructively, in Proceedings of nos Category Theory and Computer Se ii Science, edited b y D. H. Pitt, AV Poigne, D . E . Rydeheard, Lect, Notes in Comp. Sci. 283, Springer, 1987. [Reynolds84] John C. Reynolds: Polymorphism is not set-theoretic, in Semantics of Data Types, edited b y G, Kahn e t al, , Lect. N o t e s in Comp. Sci. 173, Springer, 1984, REPERENCES BIBLIOGRAPHIQUES [Seely87] R. A. G. Seely; Categorical senantics for higher order olynorphic X- calculus, The journal of ymfaolic Logic, vol. 52-4, 1987 . S UNIVERSITE DE CAEN DEPARTEMENT DE MATHEMATIQUES ESPLANADE DE L.A PAIX 14032 CAEN CEDEX