D IAGRAMMES C. O RIAT Étude des spécifications modulaires : constructions de colimites finies, diagrammes, isomorphismes. Partie II Diagrammes, tome 40 (1998), p. 3-71 © Université Paris 7, UER math., 1998, 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/ DIAGRAMMES VOLUME 40,1998 ETUDE DES SPECIFICATIONS MODULAIRES CONSTRUCTIONS DE COLIMITES FINIES, DIAGRAMMES, ISOMORPHISMES (*> PARTIE II (**> C. Oriat RESUME La composition de spécifications modulaires peut être modélisée, dans le formalisme des catégories, par des colimites de diagrammes. La somme amalgamée permet en particulier d'assembler deux spécifications en précisant les parties communes. Notre travail poursuit cette idée classique selon trois axes D'un point de vue syntaxique, nous définissons un langage pour représenter les spécifications modulaires construites à partir d'une catégorie de spécifications et de morphismes de spécifications de base Ce langage est caractérisé formellement par une catégorie de termes Animent cocomplète. D'un point de vue sémantique, nous proposons d'associer à tout terme un diagramme. Cette interprétation permet de faire abstraction de certains choix effectués lors de la construction de la spécification modulaire. Pour cela, nous définissons une catégorie de diagrammes "concrète", c'est-à-dire dont les flèches peuvent être manipulées effectivement. En considérant le quotient par une certaine congruence, nous obtenons une complétion de la catégorie de base par colimites finies. Nous montrons que le calcul du diagramme associé à un terme définit une équivalence entre la catégorie des termes et la catégorie des diagrammes, ce qui prouve la correction de cette interprétation. Enfin, nous proposons un algorithme pour décider si deux diagrammes sont isomorphes, dans le cas particulier où la catégorie de base est finie et sans cycle. Cela permet de détecter des isomorphismes "de construction" entre spécifications modulaires, c'est-à-dire des isomorphismes qui ne dépendent pas des spécifications de base, mais seulement de la manière dont celles-ci sont assemblées. ABSTRACT. The composition of modular spécifications can be modeled, in a categoy theoretic framework, by means of colimits of diagrams. Pushouts in particular allow us to o Thèse d'Informatique, préparée et soutenue à l'Institut National Polytechnique de Grenoble (Laboratoire LSR-IMAG). ( ) La Partie I de ce travail est publiée dans Diagrammes 39 et la Partie III le sera dans Diagrammes 41. gather two spécifications sharing a common part. Our work extends this classic idea along three Unes. From a syntactic point of vdew, we define a language to represent modular spécifications built from a category of base spécifications and base spécification morphisms. This language is formally characterized by afinitelycocomplete category of terms. From a semantic point of view, we propose to associate with each term a diagram. This interprétation allows us to abstract some choices made while constructing a modular spécification. We thus define a "concrète" category of diagrams, in which arrows can actually be handled. Considering the quotient by a certain congruence relation, we get a completion of the base category with finite colimits. We prove that this calculus defines an équivalence between the category of terms and the category of diagrams, which shows the soundness of this interprétation. At last, we propose an algorithm to décide whether two diagrams are isomorphic, when the base category is finite and cycle free. This allows us to detect "construction isomorphisms" between modular spécifications, i.e. isomorphisms which do not dépend on the base spécifications, but only on their combination. Introduction Spécifier un problème consiste à le décrire sans décider prématurément de la façon dont il sera résolu. En informatique, une spécification de programme est une description des fonctionnalités attendues du programme indépendante des choix de mise en œuvre. Il existe plusieurs manières de spécifier un programme. On peut utiliser une langue naturelle, par exemple en écrivant un cahier des charges. Certaines activités, comme la validation de programme, la construction automatique d'un prototype, ou la production systématique de jeux de tests, nécessitent des spécifications formelles, qui possèdent une sémantique précise, en particulier non ambiguë. Nous nous intéressons ici aux spécifications algébriques, qui font partie des spécifications orientées propriétés1. Les spécifications orientées propriétés sont basées sur un système logique, qui définit l'ensemble des propriétés que doit satisfaire tout modèle de la spécification. 1 Spécifications algébriques Une spécification algébrique est composée d'une signature et d'un ensemble d'axiomes. La signature contient les symboles utilisés pour former des expressions, et les axiomes définissent certaines propriétés de ces expressions. La logique sousjacente décrit l'ensemble des théorèmes que l'on peut déduire des axiomes. De plus, la sémantique des spécifications algébriques associe à toute spécification une classe de modèles, c'est-à-dire une classe d'algèbres multi-sortes qui satisfont les axiomes. Historiquement, les spécifications algébriques sont issues de deux courants distincts : l'algèbre universelle en mathématiques [Coh65] et les types abstraits en génie logiciel. L'origine des types abstraits figure dans le concept de classe du langage de programmation Simula [DN66, BDMN73]. Un type abstrait, composé d'un ensemble de domaines de valeurs accompagné d'un ensemble d'opérations sur ces domaines de valeurs, permet de structurer les données. L'idée de base en spécification algébrique consiste à modéliser un type abstrait par une algèbre. Cette idée est motivée par l'analogie entre un type abstrait et une algèbre multi-sortes sur une signature. L'interprétation des sortes de la signature correspond en effet aux domaines de valeurs, et l'interprétation des opérateurs de la signature correspond aux opérations sur ces domaines de valeurs. Les premiers travaux sur les spécifications algébriques datent du milieu des années 1970, avec les travaux de B. Liskov et S. Zilles [LZ74], de J. Guttag [Gut75, 1. En cinglais, property-oriented. INTRODUCTION Gut77] et du groupe ADJ (composé de J. Goguen, J. Thatcher, E. Wagner et J. Wright) [GTWW75, GTWW77, GTW78]. Au départ, les spécifications algébriques étaient basées sur la logique équationnelle. Puis ont été introduites d'autres logiques, comme les clauses de Horn, la logique du premier ordre ou encore les spécifications avec contraintes [EM90]. D'autres extensions ont permis de prendre en compte la notion d'erreur [BBC86, BL93]. J. Goguen et R. Burstall ont proposé la théorie des institutions, qui offre un cadre général pour étudier les différents formalismes de spécification algébrique [GB84, GB90]. Il existe beaucoup de références sur les spécifications algébriques, parmi les bonnes synthèses, citons [EM85, MG85, Wir90]. Ces travaux ont donné naissance à de nombreux langages de spécification algébrique, comme Clear [BG77, BG80], ACT ONE et ACT TWO [EM85, EM90], ASL [SW83, Wir86], OBJ2 et OBJ3 [FGJM85, GKK+87], PLUSS [Gau84, Bid89], LPG [Ber83, BE86, B+90], GLIDER [Huf92]. On trouve un bon panorama des différents langages de spécification algébrique existants dans [Wir94]. 2 Théorie des catégories La théorie des catégories repose sur deux notions: l'objet et la flèche, contrairement à la théorie des ensembles qui repose sur le seul concept d'ensemble. En théorie des ensembles, un ensemble est caractérisé de façon interne par ses éléments, alors qu'en théorie des catégories, un objet est caractérisé de façon externe par les relations entretenues par l'intermédiaire des flèches avec les autres objets. Pour cette raison, un grand nombre de concepts de théorie des catégories sont définis à un isomorphisme près. La théorie des catégories a été inventée au début des années 1940 par S. Mac Lane et S. Eilenberg. Bien que certains mathématiciens aient douté de l'intérêt des catégories, ce formalisme a joué un rôle unificateur en mathématiques, en particulier en algèbre et en topologie. Cette théorie définit les différents concepts de façon générale et abstraite, indépendamment de tout modèle. (C'est pour cette raison que ses détracteurs l'on surnommée "non-sens abstrait2".) La théorie des catégories a commencé à intéresser les informaticiens au début des années 1970. Par exemple, la découverte de l'équivalence entre le À-calcul typé et les catégories cartésiennes fermées a permis de donner des solutions élégantes au problème des modèles du Àcalcul, lié à celui de la résolution des équations de domaines [SP77, Wan79, LS86]. Il existe de façon générale des liens très étroits entre la théorie des types et la théorie des catégories (cf. par exemple [See84, Poi92]). L'ouvrage de référence sur les catégories est le livre de S. Mac Lane [McL71], plutôt destiné aux mathématiciens. Pour les informaticiens, le livre de M. Barr et C. Wells [BW90] est plus accessible, car les différents concepts sont présentés de façon assez élémentaire et les exemples sont tirés de l'informatique. Il existe beaucoup d'autres ouvrages qui traitent des catégories, par exemple [MB70, AM75, Gol79, AL91]. Le formalisme des spécifications algébriques s'appuie largement sur la théorie 2. En cinglais, abstract nonsense. INTRODUCTION des catégories. Historiquement, le développement des spécifications algébriques (en particulier les travaux du groupe ADJ) a été influencé par les théories algébriques de Lawvere. Les théories algébriques de Lawvere permettent de modéliser les catégories d'algèbres en faisant abstraction de la syntaxe, c'est-à-dire indépendamment de la notion de signature [Law63, BW85, WBT85]. D'autre part, d'un point de vue pratique, on peut justifier l'utilisation des catégories par l'importance des morphismes de spécifications, qui jouent un rôle essentiel en spécification algébrique. Intuitivement, un morphisme de spécifications exprime une relation entre deux spécifications. Pour prendre un exemple mathématique, tout anneau peut être considéré comme un groupe, ce qui signifie qu'il existe un morphisme de spécifications entre la spécification des groupes et la spécification des anneaux. Il peut exister plusieurs morphismes de spécifications entre deux spécifications. Par exemple, on peut considérer tout anneau comme un monoïde de deux façons différentes, en considérant soit l'opérateur additif, soit l'opérateur multiplicatif de Panneau comme l'opérateur du monoïde. Préciser quel opérateur de l'anneau sera l'opérateur du monoïde consiste exactement à définir un morphisme de spécifications entre la spécification des monoïdes et la spécification des anneaux. 3 Modularité Le développement de spécifications de grande taille nécessite un découpage des spécifications en plusieurs spécifications plus simples, appelées modules. Chaque module correspond à un problème plus simple à résoudre. Cette méthode, qui consiste à "diviser pour mieux régner"' est classique en génie logiciel [LCW85]. De façon générale, la modularité permet d'une part le développement indépendant des différents modules, et d'autre part une meilleure compréhension de chaque module, ce qui facilite la maintenance. Cette vision de la modularité correspond à une approche descendante de résolution de problème, puisque l'accent est mis sur la décomposition du problème en plusieurs sous-problèmes plus simples. Dans notre travail, notre conception de la modularité est au contraire ascendante. Nous nous intéressons en effet à la composition des modules, c'est-à-dire à l'assemblage de modules élémentaires permettant de construire des modules plus complexes. Ces modules élémentaires sont regroupés dans une bibliothèque, la bibliothèque des modules de base. L'intérêt de la composition est de permettre la réutilisation des modules de base, préconisée en génie logiciel pour réduire les erreurs et les coûts de développement (cf. par exemple [Ber90]). Un aspect de la modularité est la possibilité de définir des spécifications génériques, c'est-à-dire paramétrées [SST92]. En effet, une spécification paramétrée peut être instanciée de différentes manières par d'autres spécifications, ce qui évite de réécrire une nouvelle spécification pour chaque variation d'un même problème. Le but est alors de définir des spécifications génériques suffisamment générales pour permettre de spécifier le maximum de problèmes par une simple instanciation [Mar95]. Le développement modulaire des spécifications est assisté dans les langages de spécification algébrique par des opérateurs de construction^ comme le renommage, 3. En anglais, spécification-building opérations. INTRODUCTION Venrichissement ou Yabstraction [ST88, Wir90]. Ces primitives permettent de construire de nouvelles spécifications à partir de spécifications déjà définies. La composition de modules est un cas particulier d'opérateur de construction de spécifications, qui peut être modélisé par des colimites de diagrammes. Intuitivement, en théorie des catégories, un diagramme permet de décrire un assemblage de plusieurs objets en précisant des partages entre certains objets à l'aide de flèches. La colimite du diagramme permet de considérer le résultat de cette composition. Cette utilisation générale des colimites pour modéliser l'interconnexion de systèmes a été proposée par J. Goguen [Gog73, Gog92]. Un cas particulier de colimite est la somme amalgamée*, qui correspond à l'assemblage de deux objets B et C, en spécifiant une partie commune entre ces deux objets par un objet partagé A et deux flèches / : A —> B et g : A —> C. En spécification algébrique, la somme amalgamée peut modéliser d'une part la composition de deux spécifications qui ont une partie commune, et d'autre part Yinstanciation d'une spécification générique. 4 Notre travail Nous étudions la composition des spécifications algébriques modulaires. Nous supposons que nous disposons d'une bibliothèque de spécifications et de morphismes de spécifications de base, qui forment une catégorie de base, en général appelée CQ dans ce mémoire. Les spécifications de base sont monolithiques, c'est-à-dire non décomposées. Notre travail repose sur une idée classique en spécification algébrique : la composition des spécifications peut être modélisée par des colimites de diagrammes finis. Nous proposons donc de considérer une spécification modulaire comme une spécification obtenue à partir de spécifications et morphismes de spécifications de base par une suite de constructions de colimites. Notre travail est indépendant de la logique sous-jacente du langage de spécification algébrique. Nous pouvons donc nous placer dans le cadre général des institutions. Nous devons uniquement supposer que la catégorie des spécifications est finiment cocomplète, c'est-à-dire que tout diagramme fini a une colimite. D'un point de vue syntaxique, c'est-à-dire en ce qui concerne le langage utilisé pour décrire ces constructions, nous ne considérons pas toutes les colimites finies, mais uniquement les sommes amalgamées. En effet, avec la spécification vide, objet initial de la catégorie des spécifications, les sommes amalgamées permettent de simuler la construction de toute colimite finie. Nous proposons la construction d'une catégorie de termes, appelée Terme(Cn), pour représenter la composition de spécifications modulaires en utilisant les sommes amalgamées. En théorie des catégories, on travaille le plus souvent à un isomorphisme près. C'est une conséquence de la caractérisation externe des objets dans ce formalisme. Les colimites, par exemple, sont définies au départ à un isomorphisme près. La définition d'une syntaxe est au contraire un problème typiquement informatique, qui nécessite de faire des choix de représentation. C'est la raison pour laquelle nous devons utiliser des sommes amalgamées choisies au moment de la définition du langage 4. En anglais, pushout. Les catégoriciens utilisent également le terme de coproduit fibre. INTRODUCTION d'expression pour les spécifications modulaires. Ces choix de sommes amalgamées correspondent à des choix de codage. Un terme correspond donc à une spécification modulaire construite par une succession de sommes amalgamées. Dans une seconde étape, nous proposons d'interpréter un terme par un diagramme dont la colimite est la spécification modulaire dénotées par ce terme. Nous considérons les diagrammes comme une sémantique pour les spécifications modulaires, par opposition aux termes qui constituent la syntaxe. L'interprétation des termes par des diagrammes nécessite de définir une catégorie de diagrammes puisqu'il faut non seulement associer à toute spécification modulaire un diagramme, mais aussi associer à tout morphisme de spécifications modulaires un morphisme de diagrammes. La définition d'un diagramme est relativement standard en théorie des catégories, bien qu'il existe quelques nuances. La définition de morphisme de diagrammes est moins connue, en particulier dans la littérature informatique où sont utilisées des définitions moins générales que celle dont nous nous servons ici. Nous présentons deux catégories de diagrammes, DIAGR(Co) et diagr(Co)- Les objets de DIAGR(Co) sont des diagrammes, et les flèches de DIAGR(Cn) des morphismes de diagrammes. La catégorie diagr(Co) est obtenue à partir de DIAGR(Co) par un quotient par une relation de congruence sur les flèches de DIAGR(Cn)- C'est la catégorie diagr(Co) qui possède les propriétés théoriques intéressantes. Il s'agit en effet d'une catégorie finiment cocomplète, c'est-à-dire que tout diagramme fini sur diagr(Co) a une colimite finie dans diagr(Co). D'autre part, diagr(Co) est une complétion par colimites finies de la catégorie C$. Sur le plan pratique, comme les flèches de diagr(Co) sont des classes d'équivalence de morphismes de diagrammes, on travaille en réalité avec des représentants, c'est-à-dire avec des flèches de DIAGR(Co). La catégorie DIAGR(Co) permet donc la manipulation effective des flèches de diagr(Co). La représentation des termes par des diagrammes est définie par un foncteur V : Terme(Co) -> diagr(C0) entre les catégories Terme(Co) et diagr(Co). Nous montrons que ce foncteur définit une équivalence de catégories entre Terme(Co) et diagr(Co), ce qui signifie que bien qu'elles ne soient pas isomorphes, ces catégories ont néanmoins essentiellement la même structure. Après avoir représenté les spécifications modulaires par des diagrammes, nous nous intéressons au problème de Y équivalence entre deux spécifications modulaires. Deux spécifications modulaires sont considérées comme équivalentes lorsque cellesci sont isomorphes en tant que colimites de diagramme. Détecter cet isomorphisme consiste en fait à détecter un isomorphisme entre deux diagrammes dans la catégorie diagr(Cn). Nous appelons cet isomorphisme un isomorphisme de construction, parce qu'il ne dépend pas de la définition effective des spécifications de base, mais seulement de la manière dont celles-ci sont combinées pour construire les spécifications modulaires. Dans l'hypothèse où la catégorie Cn est finie et ne comporte pas de cycle, nous proposons un algorithme pour détecter si deux diagrammes sont isomorphes. Des résultats partiels concernant l'interprétation des termes par des diagrammes et la détection d'isomorphismes de construction ont été présentés dans [Ori94, Ori95]. 10 5 INTRODUCTION Comparaisons avec d'autres travaux Catégories de diagrammes La définition de diagramme est, à quelques nuances près, standard. Chez S. Mac Lane [McL71], un diagramme sur une catégorie C est un foncteur d'une catégorie J vers C. La définition de M. Barr et C. Wells [BW90], est moins générale, puisqu'un diagramme est un morphisme de graphes d'un graphe vers le graphe sous-jacent de C. Nous utilisons une définition "intermédiaire" : pour nous, un diagramme est un foncteur d'une catégorie librement engendrée sur un graphe vers C. Partir d'un graphe nous permet de rester proche de l'informatique. Par contre, nous ne souhaitons pas nous restreindre à une petite catégorie C. La définition de morphisme de diagrammes est beaucoup moins standard. Par exemple dans Clear, un morphisme de diagrammes, appelé morphisme basé, correspond uniquement à une inclusion entre deux diagrammes. La définition proposée par A. Tarlecki, R. Burstall et J. Goguen dans [TBG91], bien que plus générale que celle utilisée dans la sémantique du langage Clear, n'est pas encore suffisamment générale pour notre travail. En effet, cette définition ne permet pas de représenter tout morphisme de spécifications modulaires par un morphisme de diagrammes. La définition de morphisme de diagrammes que nous utilisons n'est pas nouvelle en théorie des catégories. Une version duale de la catégorie diagr(Co) est par exemple utilisée par M. Barr et C. Wells dans [BW94]. Néanmoins, la reformulation de la définition de catégorie de diagrammes que nous proposons dans le chapitre 2 présente un intérêt en informatique, d'une part parce que la catégorie DIAGR(Co) permet de manipuler effectivement les morphismes de diagrammes, et d'autre part parce que les catégories DIAGR(Co) et diagr(Co) sont peu connues dans cette discipline. Calculs de colimites R. Burstall et D. Rydeheard proposent des algorithmes pour calculer certains concepts de théorie des catégories [Bur80, BR86], en particulier les colimites de diagrammes. Le calcul général de colimite est paramétré par certaines colimites, en l'occurrence un objet initial, des sommes et des coégalisateurs, qui permettent d'évaluer la colimite d'un diagramme quelconque. Ainsi, ayant défini l'objet initial, la somme et le coégalisateur par exemple dans la catégorie des ensembles Set, on en déduit un moyen de calculer la colimite d'un diagramme quelconque dans Set. Cet algorithme est en fait basé sur une preuve du résultat suivant : si une catégorie a un objet initial, des sommes et des coégalisateurs, alors celle-ci est Animent cocomplète. Notre travail est basé sur un théorème similaire : si une catégorie a un objet initial et des sommes amalgamées alors celle-ci est finiment cocomplète. Notre travail est différent, dans la mesure où nous ne cherchons pas à calculer des colimites dans une catégorie fixée. En particulier, nous nous intéressons au problème général de l'isomorphisme entre deux diagrammes, qui correspond à un isomorphisme entre leurs colimites respectives. Cet isomorphisme est indépendant de la catégorie sur laquelle ces diagrammes sont construits. INTRODUCTION 11 Utilisation des colimites en spécification algébrique L'utilisation des colimites pour représenter l'assemblage de spécifications est loin d'être nouvelle. R. Burstall et J. Goguen ont présenté cette idée dans la sémantique du langage de spécification Clear [BG80]. Dans Clear, la composition de plusieurs spécifications qui partagent un environnement commun, appelées théories basées, est en effet formalisée par la colimite d'un diagramme. Les colimites ont ensuite été assez intensivement utilisées en spécification algébrique. La somme amalgamée en particulier permet de modéliser l'instanciation de spécifications génériques [TWW82, EM85]. H. Ehrig, R. Jimenez et F. Orejas [EJ093] ont également présenté une forme plus générale d'instanciation à l'aide de sommes amalgamées multiples5, nouvel exemple de colimite. Syntaxe pour les constructions modulaires J. Bergstra, J. Heering et R. Klint [BHK90] d'une part, et G. Renardel de Lavalette [Ren91] d'autre part, ont proposé de structurer les opérateurs de construction de spécifications sous forme d'algèbres de modules. Une algèbre de modules est un langage permettant d'écrire des expressions de composition des spécifications algébriques. Cette approche est voisine de notre travail sur le langage Terme(Cn)> puisque le problème de la composition des spécifications algébriques est abordé d'un point de vue syntaxique, et permet de comparer différentes spécifications modulaires. Par contre, nous ne nous intéressons pas aux mêmes opérateurs de constructions de spécifications, puisque nous ne considérons que les constructions de colimites. Notre syntaxe pour représenter les spécifications algébriques modulaires est largement inspirée des travaux de J.-C. Reynaud, qui a proposé un système de types pour représenter les constructions de colimites [Rey90a, Rey90b, Rey93]. Ce système est fondé sur les théories algébriques généralisées de Cartmell [Car86] qui permettent de spécifier des types dépendants, c'est-à-dire des types paramétrés par des termes. Les types dépendants ont été également utilisés par T. Streicher et M. Wirsing [SW91] pour modéliser la composition de spécifications algébriques modulaires. D'autre part, H. Ehrig, R. Jimenez et F. Orejas ont également proposé une syntaxe pour les spécifications algébriques modulaires dans [EJ093]. Cette syntaxe est en partie basée sur des constructions de sommes amalgamées. La principale difficulté en ce qui concerne la définition d'une syntaxe pour les constructions de colimites est le problème de circularité entre la définition d'une part des objets et des flèches de Terme(Co) et d'autre part de l'égalité entre deux flèches de Terme(Cn). En effet, il existe une flèche, que nous appelons up dans ce mémoire, entre une somme amalgamée et un objet à condition qu'une égalité entre deux flèches de Terme(Cn) soit vérifiée. La définition des flèches up dépend donc de la définition de l'égalité des flèches dans Terme(Cn), qui elle-même présuppose que les flèches ont été définies. J.-C. Reynaud contourne le problème en proposant une définition concrète, c'està-dire sémantique, d'une catégorie librement engendrée par objet initial choisi et sommes amalgamées choisies [Rey93]. H. Ehrig, R. Jimenez et F. Orejas [EJ093] ne 5. En anglais, multiple pushout. 12 INTRODUCTION définissent pas de syntaxe pour les flèches up. La syntaxe qu'ils proposent ne permet donc pas d'obtenir une catégorie finiment cocomplète. Une solution pour spécifier une catégorie finiment cocomplète sans utiliser d'égalités pour définir les flèches a été présentée par F. Cury dans [Cur91]. F. Cury propose de dédoubler les flèches up en deux flèches dont la définition ne dépend pas d'une égalité. Ces deux flèches, qui sont des exemples particuliers de flèches up, permettent de reconstruire a posteriori toutes les flèches up. La solution que nous proposons consiste à stratifier la construction de Terme(Co) en une suite de catégories C,. L'existence d'une flèche up dans la catégorie C, dépend uniquement d'égalités dans la catégorie C%-\. Nous évitons ainsi le problème de circularité entre la définition des flèches et la définition des égalités. Notre catégorie Terme(Co) peut être comparée au type d'une esquisse, introduit par C. Ehresmann [Ehr68]. Dans les travaux de D. Duval et J.-C. Reynaud [DR94a, DR94b], le type d'une esquisse est une catégorie librement engendrée à partir d'un graphe par sommes et produits. Par conséquent, la construction du type d'une esquisse est basée sur les catégories à sommes et produits alors que la construction de Terme(Cn) est basée sur les catégories à colimites finies. D'autre part, une esquisse contient des cônes et cocônes distingués, qui spécifient certaines limites ou colimites. Par contre, dans la construction de Terme(Co) que nous proposons, il n'est pas possible de spécifier des sommes amalgamées distinguées dans la catégorie de base CQ. 6 Plan de ce mémoire Ce mémoire est divisé en trois parties, chaque partie faisant l'objet d'un volume de Diagrammes. Dans la première partie, qui comprend les chapitres 1 et 2, nous avons présenté le cadre général de notre travail (les spécifications modulaires), ainsi que les bases théoriques (les catégories de diagrammes). Ce volume contient la deuxième partie de notre thèse, qui correspond au chapitre 3. Ce chapitre est consacré à la syntaxe des spécifications modulaires. Nous proposons une construction stratifiée de la catégorie de termes Terme(Co), qui fournit un langage pour représenter les spécifications et morphismes de spécifications modulaires. Nous montrons d'une part que Terme(Cn) est une catégorie finiment cocomplète, et d'autre part que Terme(Co) est une extension conservatrice de CQ. Enfin, nous construisons, à partir de Terme(Co), une catégorie C(CQ) librement engendrée par objet initial choisi et sommes amalgamées choisies sur CQ. La troisième partie, qui fait l'objet d'un troisième volume de Diagrammes, sera consacrée à l'interprétation des termes par des diagrammes (chapitre 4) et à la présentation d'un algorithme permettant de détecter si deux diagrammes sont isomorphes, dans le cas où la catégorie de base est finie et sans cycle (chapitre 5). Chapitre 3 Syntaxe : catégorie des termes "Nous sommes certain que la, syntaxe est indispensable mais nous voulons soutenir qu'elle ne saurait être syntaxe que dans la mesure où elle envisage non pas des relations entre objets quelconques, mais des relations entre des "signes" ou des "expressions'7. Or ce n'est que comme concept pragmatique que nous pourrons aborder la notion de "signe" ou dy "expression", car un événement n'est un signe que s'il est émis ou reçu comme tel." — Léo Apostel, Logique et connaissance scientifique Dans ce chapitre, nous considérons une catégorie CQ de base dont les objets sont considérés comme "atomiques", c'est-à-dire ne peuvent pas être divisés. Nous supposons que cette catégorie CQ est petite. Nous souhaitons pouvoir construire des objets composites en réunissant ces objets élémentaires, en fusionnant éventuellement certaines parties communes. L'assemblage de plusieurs objets est modélisé à l'aide de constructions de colimites. Par exemple, dans la catégorie des ensembles, la somme permet de modéliser l'union disjointe de deux ensembles. La somme amalgamée permet de réunir deux ensembles en fusionnant certains éléments. Dans le cadre des spécifications algébriques, la somme amalgamée permet également de combiner deux spécifications en précisant les parties fusionnées. Le but de ce chapitre est de présenter une syntaxe, c'est-à-dire un langage de description des constructions de colimites. Ces constructions de colimites font partie d'une catégorie, parce qu'à partir des objets et flèches de CQ, on peut non seulement construire des objets colimites, mais également des flèches entre objets colimites. En effet, d'un point de vue formel, la fonction qui à tout diagramme associe sa colimite peut s'appliquer sur les flèches et être ainsi étendue en un foncteur. Dans ce chapitre, nous construisons donc une catégorie de termes, appelée Terme(Cn), dont les objets représentent des constructions de colimites. Notre objectif n'est pas d'avoir une syntaxe pour toutes les constructions de coli13 14 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES mites finies, mais de sélectionner quelques constructions qui permettent d'obtenir un objet isomorphe à n'importe quelle colimite finie. Il s'agit donc de pouvoir décrire une catégorie finiment cocomplète. Ici, nous choisissons d'avoir une représentation pour un objet initial, et pour des sommes amalgamées. Ce choix est purement arbitraire, on aurait pu prendre d'autres colimites, comme des sommes ou des coégalisateurs. Nous avons donc besoin de constructions syntaxiques pour l'objet initial et les sommes amalgamées. Nous utilisons le terme 0 pour représenter l'objet initial, et le terme push (.4, B,C, / , g) pour représenter la somme amalgamée construite sur le diagramme qui comporte trois nœuds étiquetés par A, B, et C, et deux flèches étiquetées par / : A —> B et g : A —> C. Comme nos constructions sont purement syntaxiques, la seule égalité dont nous disposons, au départ, est Videntité syntaxique. Nous définissons donc des relations entre les flèches pour décrire les propriétés de l'objet initial et des sommes amalgamées. Techniquement, nous définissons donc une précatégorie, c'est-à-dire une catégorie dans laquelle certaines égalités sont remplacées par des équivalences sur les flèches. La catégorie correspondante est le quotient de cette précatégorie par la relation d'équivalence. Comme l'existence de certains termes est conditionnée par une relation entre deux autres termes (cf. règle (10)), on ne peut pas définir successivement les termes, puis la relation sur les termes. Pour résoudre ce problème, nous proposons une construction stratifiée de la syntaxe. Nous définissons une suite de précatégories de termes d, telles que, dans la précatégorie Cx\, l'introduction de termes n'est conditionnée que par des relations entre termes de C,_i. Finalement, la précatégorie des termes TERME(Co) est la "limite" de la suite de précatégories C,. S y n t a x e , s é m a n t i q u e , c a t é g o r i e s et choix En informatique, les problèmes ont souvent deux aspects: un aspect syntaxique. qui correspond au langage qui décrit les objets manipulés (par exemple un programme) ; et un aspect sémantique, qui correspond au sens des objets manipulés (par exemple le résultat de l'exécution d'un programme). Du point de vue syntaxique, on fait des choix de représentation, qui correspondent à la définition du langage utilisé. Du point de vue sémantique, on travaille indépendamment du choix de représentation, "à un codage près". L'intérêt des catégories réside dans le fait que l'on travaille le plus souvent "à un isomorphisme près", ce qui correspond à travailler "à un codage près" en informatique. Par exemple, en théorie des catégories, on définit les colimites à un isomorphisme près : un diagramme peut avoir plusieurs colimites, qui sont alors isomorphes. Lorsque Ton parle de "la" colimite d'un diagramme, il s'agit en fait souvent d'"une" colimite quelconque d'un diagramme, sachant que tant que l'on travaille à un isomorphisme près, on peut en choisir une quelconque. L'ensemble ({1} x A)U({2} x B) est un exemple de choix de colimite pour A + B dans la catégorie des ensembles. Ce degré de liberté est trop important lorsque l'on parle de syntaxe. On a en effet besoin de faire des choix de représentation ou de codage. Si on veut décrire une syntaxe pour des constructions de colimites, on ne peut plus parler des colimites à un isomorphisme près. En effet le fait d'avoir une représentation syntaxique par exemple pour une somme impose que Ton ait fait un choix particulier de somme. 3.1. PRÉCATEGORIES, PREFONCTEURS ET PRE-COLIMITES 15 Cela explique pourquoi dans toute la suite, nous parlons d'"objet initial choisi", ou de usomme amalgamée choisie". Techniquement, on doit faire des choix afin d'avoir une construction libre. L'introduction de colimites choisies dans une catégorie, due à C. Ehresmann [Ehr65, Ehr68], permet de donner un statut algébrique à cette catégorie. 3.1 Précatégories, préfoncteurs et pré-colimites Nous commençons par définir la notion de précatégorie, similaire à celle de catégorie. Dans une précatégorie, il n'y a, a priori, pas d'égalité entre flèches, mais seulement des équivalences. Chaque ensemble de flèches est donc muni d'une relation de d'équivalence. Définition 3.1 (Précatégorie) Une précatégorie C est définie par • une classe d'objets Obj(C), (si A est un objet de Obj(C), on notera AGObj(C), même si Obj(C) n'est pas un ensemble) ; • une famille Arr(C) indicée par Obj(C) x Obj(C) de flèches — autrement dit, VA, B G Obj(C), on a un ensemble de flèches Arr(C)(A, B) ; • une famille U(C) indicée par Obj(C) x Obj(C) de relations sur Arr(C) — autrement dit, VA,B G Obj(C), on a une relation TZ(C)(A,B) sur l'ensemble Arr(C)(-4,fl); • VA, B,C G Obj(C), on a une opération de composition o : Arv(C){B,C) X AVT{C)(A,B) -> Arr(C)(A,C) ; • VA G Obj(C), on a une flèche identité idA G ATT(C)(A, A) ; • VA, B G Obj(C), V/ G Arr(C){A, B), (foidA,f)en(C)(A,B) (idBof,f)en(C)(A,B); • \JA,B,C,D£Ob]{C), V/ G Avv{C){A, B), Vp G Avv{C){B, C), Vh G Arr(C)(C, D), ((hog)of,ho(gof))en(C)(A,D); • TZ(C) est une congruence, c'est-à-dire - VA, B G Obj(C), U{C){A, B) est une relation d'équivalence ; - \/A,B,Ce Obj(C), V / , / ' G Arr(C)(A,B), Vg,g'£ ATT(C)(B,C), 16 CHAPITRE 3. SYNTAXE : CATEGORIE DES TERMES Lemme 3.1 On peut associer à toute précatégorie C une catégorie, qu'on notera également, par abus de langage, C. Cette catégorie est définie de la façon suivante. • Les objets de la catégorie C sont les objets de la précatégorie C. • Comme 1Z(C)(A.B) est une relation d'équivalence sur ATT(C)(A,B), on peut définir Vensemble des flèches de A vers B de la catégorie C comme l'ensemble quotient homc{A,B) = Arr{C){A,B)/n{C){A,B). On notera [f] : A -> B la classe d'équivalence de f G Arv(C)(A, B). • Etant donné un objet A de C, l'identité sur A est [idA] : A —> A. • La composition de deux flèches [f] : A —» B et [g] : B —> C est la classe [g o f] : A —> C. Cette définition est indépendante des représentants f et g choisis carlZ(C) est une congruence. Preuve. On vérifie immédiatement que • les flèches [idA] : A —• A sont bien des identités ; • la composition est associative. Réciproquement, on peut considérer toute catégorie comme une précatégorie, en prenant pour relation d'équivalence la relation d'égalité sur les flèches. Définition 3.2 (Identité syntaxique) Soit une précatégorie C. L'égalité dans C (à ne pas confondre avec l'équivalence 1Z(C)) est appelée identité syntaxique. En effet, dans une précatégorie de termes, deux termes sont égaux lorsqu'ils sont syntaxiquement identiques, c'est-à-dire composés des mêmes symboles. Notations • L'identité syntaxique sera notée =. • Pour plus de lisibilité, et comme deux flèches équivalentes dans la précatégorie C sont égales dans la catégorie C associée, (/, / ' ) G TZ(C)(A, B) sera noté / = /,GArr(C)(A,B). Nous rappelons le plus souvent possible l'ensemble auquel les flèches appartiennent, parce que nous manipulons plusieurs précatégories, et certaines flèches appartiennent à plusieurs ensembles de flèches dans des précatégories différentes. Définition 3.3 (Petite précatégorie) Une précatégorie C est petite si et seulement si la catégorie associée est petite, c'est-à-dire si et seulement si Obj(C) est un ensemble. 3.1. PRÉCATÉGORIES, PRÉFONCTEURS ET PRE-COLIMITES 17 L'analogue d'un foncteur entre deux catégories est un préjoncteur entre deux précatégories. Définition 3.4 (Préfoncteur) Soit deux précatégories C et V. Un préjoncteur F de C vers V, noté F : C —> V est une application qui à tout objet A de C associe un objet F{A) de î>, et à toute flèche / € Arr(C)(.4, B) associe une flèche F(j) € Arr(D)(F(.4), F(B)), et telle que . V/,/'€Arr(C)(A,B), j = j'eArr(C)(A,B) => F(j) = F(j') € Atv(V)(F(A),F(B)) ; • V.4 € Obj(C), F(Jrf^) = idF(A) e Arr(ï>)(F(/i), F(.4)) ; • V/ € Arr(C)(.4, B) et V5 G Arr(C)(5,C), F(9 o / ) = F(<7) o F ( / ) € Arr(P)(F(.4), F(C)). A tout préfoncteur entre deux précatégories on peut associer un foncteur entre les catégories correspondantes. Le m m e 3.2 Soit deux précatégories CetVet un préfoncteur F : C —» V. Alors on a un foncteur, noté également F : C -» V entre les catégories C et X>, défini par F : C A -> H* [f] * V A [F(f)] La définition de F([f]) est bien indépendante du représentant f choisi car j = j'eArr(C)(A,B) => F ( / ) = F(/'))(F(/t),F(B)). Deux préfoncteurs F,G :C - 4 P sont syntaxiquement identiques lorsque • WlGObj(C), F(A) = G(A); • Vj€Arr(C)(A,B), F(j) = G(j). On note F = G. On peut reformuler de nombreuses notions de théorie des catégories en les adaptant aux précatégories. Il suffit de remplacer les égalités entre flèches dans chaque catégorie par des équivalences dans la précatégorie correspondante. Définition 3.5 (Isomorphisme) Soit une précatégorie C. La flèche / G Arr(C)(A, B) est un isomorphisme (dans la précatégorie C) si et seulement si il existe une flèche g G An{C)(B, A) telle que g o f = idA G Arr(C)(A, A) et / og = idB G Arr(C)(fl, B). 18 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES On vérifie facilement qu'une flèche / dans une précatégorie C est un isomorphisme si et seulement si [/] est un isomorphisme dans la catégorie associée. Définition 3.6 (Préfoncteur plein) Soit deux précatégories C et V, et un préfoncteur F : C —• V. Le préfoncteur F est plein si et seulement si pour toute flèche g G Arr(P)(F(A), F{B)). il existe une flèche / G Arr(C)(A, B) telle que g= F(f)£Arr(V)(F(A),F(B)). Définition 3.7 (Préfoncteur fidèle) Soit deux précatégories C et V, et un préfoncteur F : C -+ V. Le préfoncteur F est jidèle si et seulement si pour toutes flèches /,/'€Arr(C)(/t,fl), F ( / ) = F ( / ' ) G A r r ( P ) ( F ( , 4 ) , F ( B ) ) => / = / ' G Arr(C)(.4, B). On vérifie facilement qu'un préfoncteur F est plein (respectivement fidèle) si et seulement si le foncteur associé est plein (respectivement fidèle). On peut enfin reformuler la notion de colimite d'un diagramme pour une précatégorie. Nous définissons ici uniquement les notions d'objet pré-initialet de pré-sommes amalgamées. Définition 3.8 (Objet pré-initial) Soit une précatégorie C. Un objet 0 de C est pré-initial si et seulement si 1. VAe Obj(C), il existe une flèche j A G Arr(C)(0, A) ; 2. V/GArr(C)(0,A), / = j A G Arr(C)(0, A). Lemme 3.3 Un objet 0 est pré-initial dans une précatégorie C si et seulement si 0 est initial dans la catégorie associée C. Définition 3.9 (Pré-somme amalgamée) Soit une précatégorie C. Soit trois objets .4, B et C de C, ainsi que deux flèches / G Arr(C)(,4,£) et g G Arr{C)(A,C). Le triplet (F, & l t & 2 ), où F e O b j ( C ) , &i G ATT{C){B,P) et &2 € Arr(C)(C,F),est une pré-somme amalgamée de B et C par rapport aux flèches / et g si et seulement si 1. kloj = k2ogeAtr(C)(A,P); 2. si D € Obj(C), / ' G ATT{C)(B,D), Arr(C)(A,D), alors, g' G Arr(C)(C,D) et / ' o / = g' o g G (a) il existe une flèche u G Arr(C)(F, D) telle que u o & ! = / ' G Arr(C)(£,£>) uok2=g'eATT(C)(C,D); (b) pour toute flèche v G Arr(C)(F, Z>) telle que voSd = / ' G A r r ( C ) ( B , D ) u o & 2 = (/ / GArr(C)(C,D), on a u = oGArr(C)(P,£>). 3.1. PRÉCATÉGORIES, PRÉFONCTEURS ET PRÉ-COLIMITES 19 L e m m e 3.4 Le triplet (P, &i, &2) est une pré-somme amalgamée de B et C par rapport aux flèches f et g dans la précatégorie C si et seulement si le triplet (F, [&i], [&2D est un€ somme amalgamée de B et C par rapport aux flèches [f] et [g] dans la catégorie associée C. On peut définir, de façon similaire, la pré-colimite d'un diagramme sur une précatégorie. Une précatégorie est finiment pré-cocomplète lorsque tout diagramme fini a une pré-colimite. De façon générale, une pré-colimite dans une précatégorie correspond à une colimite dans la catégorie associée. Par conséquent, une précatégorie est finiment précocomplète si et seulement si la catégorie associée est finiment cocomplète. De plus, une précatégorie est finiment pré-cocomplète si et seulement si elle a un objet préinitial et des pré-sommes amalgamées. Précatégorie DIAGR(C) Étant donné une catégorie C, la catégorie DIAGR(C), avec la relation de congruence %, est une précatégorie. Plus précisément, • l'identité syntaxique dans la précatégorie DIAGR(C) est l'égalité dans la catégorie DIAGR(C) : - si cï et [3 sont deux objets de DIAGR(C), a = /3 (dans la précatégorie) <=> â = f3 (dans la catégorie) ; - si W, T : â -> /3 sont deux flèches de DIAGR(Co), â = T (dans la précatégorie) & â = r (dans la catégorie) ; • la relation d'équivalence dans la précatégorie DIAGR(C) est la congruence « sur les flèches de la catégorie DIAGR(C) : si a, r : â -» /3 sont deux flèches de DIAGR(Co), â = r G A r r ( D I A G R ( C ) ) ( â , / 3 ) <* a % r. La catégorie associée à la précatégorie DIAGR(C) est diagr(C). De plus, le foncteur le :C -> DIAGR(C) peut être considéré comme un préfoncteur dont le foncteur associé est [-]c o Ic : C -» diagr(C). D'autre part, la précatégorie DIAGR(C) est finiment pré-cocomplète, d'après les lemmes 2.17 (partie I, page 100) et 2.19 (partie I, page 101). Remarquons que ce sont justement ces deux lemmes qui nous ont permis de montrer que la catégorie diagr(C) est finiment cocomplète. L'aplatissement Apl c : DIAGR 2 (C) -+ DIAGR(C) donne un choix de pré-colimites dans DIAGR(C). En particulier, la précatégorie DIAGR(C) a un objet pré-initial choisi (le diagramme vide) et des pré-sommes amalgamées choisies (obtenues par aplatissement). 20 3.2 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES Problème de circularité termes - congruences Soit Co une petite catégorie. Nous cherchons à définir une catégorie qui contient Co. qui a un objet initial et des sommes amalgamées. Nous allons en fait définir une précatégorie avec un objet pré-initial et des pré-sommes amalgamées. Objet pré-initial Pour l'objet pré-initial, il nous suffit d'introduire un nouvel objet 0 , et pour tout objet A, une flèchej^ de 0 vers A. De plus, pour chaque couple de flèches (/, g) de 0 vers A, on introduit la relation / = g. Pré-sommes amalgamées Etant donné trois objets A, B et C, ainsi que deux flèches / : A —> B et g : A -+ C, nous introduisons un nouvel objet push (A,B,C,f,g) deux flèches Sn(A,B,C,f,g): B^ push (A, B,C,f, g) b2(A, B, C, f, g) :C-> push (A, B,C,f, g) et la relation &l(A,B,C,j,g)oj = 8c2(A,B,C,j,g)og. Il y a donc une circularité entre la définition des objets et la définition des flèches, puisque l'introduction d'une nouvelle flèche permet d'introduire ensuite des nouveaux objets. Cette circularité ne pose, a priori, pas de problème car il s'agit d'une circularité au niveau des termes. De plus, étant donné un objet D et deux flèches f':B—>Detg':C—>D telles que f'oj = g'og on introduit une flèche up (A, B, C, D, f, g, /', g') : push (A, B, C, f, g) -> D et deux relations up (4, B, C, D, j , g, / ' , D dans C,+i. Dans chaque d, nous définissons donc d'abord les objets — l'ensemble Obj(Cî) —> ensuite les flèches — la famille d'ensembles Arr(Cj) —, et enfin les équivalences entre flèches — la famille de relations 72(Ct). 3.3 Précatégories Ci Soit CQ une petite catégorie. On considère la précatégorie associée CQ. On a donc un ensemble d'objets Obj(Cn), une famille de flèches Arr(Co) et une famille de relations 1Z(CQ). Si A et B sont des objets de CQ, la relation 1Z(CQ)(A,B) sur l'ensemble Arr(Cn)(A, B) est l'égalité dans la catégorie CQ. Dans ce paragraphe, nous définissons, pour tout entier naturel i, une petite précatégorieC,-+i, en définissant successivement les ensembles et familles d'ensembles Obj(C,-+i), Arr(C,+i) et U{Ci+i), à partir de Obj(C,), Arr(Ct) et lZ(d). Chaque ensemble est caractérisé par des règles de la forme xeX ; z(x,y)£Z yeY 22 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES Cette règle définit partiellement l'ensemble Z, et signifie: bt Si le terme x appartient à À', et si le terme y appartient à Y, alors le terme z(x, y) appartient à Z." Ensuite, on considère le plus petit ensemble Z qui satisfait toutes les règles qui le définissent. Règles qui définissent l'ensemble Obj(C2+i) Les objets de C,+i sont les objets de CQ (règle (1)), et les objets que l'on peut construire à partir d'objets et de flèches de C;, c'est-à-dire objet pré-initial (règle (2)) et pré-somme amalgamée (règle (3)). ^eObj(Co) AeObj(Ci+l) (2) 0€Obj(C,-+i) . 4 , f l . C € O b j ( Ç ) ; j £ Arr(d)(A, B) ; g G Arr(C,)(.4,C) push (.4, B,C,j,g)eObj(Ci+l) (3) Règles qui définissent la famille d'ensembles Arr(C,+i) Les flèches de d+i sont les flèches de Co (règle (4)), les compositions de flèches de Cl+i (règle (5)), les identités entre objets de C,+i (règle (6)), les flèches de cône colimite (règles (8), (9)), et les uniques flèches d'un objet colimite vers le sommet d'un cône (règles (7), (10)). .4,£çObj(C0) ; /eArr(C0)(.4;fl) /GArr(C,- + i)(^,B) A,B,CeOb)(Ci+l) (4) ; / € A r r ( C , - + 1 ) ( ^ , B ) ; g G Arr(C,- +1 )(B,C) gofeAn(Ci+l)(A,C) (5) .4€Obj(C,.n) \dA6ArT(Ci+l)(A,A) (6) AçObj(Ci+1) iAeArr(Ci+l)(0,A) (7) .4,fl,C€Obj(C,-) ; /6Arr(C t -)(i4,B) ; g G Arr(C,)(A,C) in(A, B,C,j,g) eArr(Ci+l)(B, push (A, B,C,j,g)) (8) . 4 , g , C 6 0bj(C,-) ; f€An{Ci)(A,B) ; g G An(d)(A,C) &2(.4, B, C, / , g) G Arr(C,-+1 ) (C, push (A, B, C, j , g)) (9) A,B,C,DeObj(Ci) ; / G An(Ci)(A,B) ; g € An(&)(A,C) f'eArr(Ci)(B,D) ; g' G Arr(C,)(C,P) ; / ' o / = g'og G An(b)(A, up (A, B,C, D, /,g, j',g') G Arr(C,-+i)(push {A, B, C, j,g), D) D) (10) 3.3. PRÉCATÉGORIES d 23 Remarquons que l'existence de la flèche up de C;+i dépend d'une relation entre deux flèches de C;. L'introduction d'un terme dans une précatégorie ne dépend jamais d'une relation dans cette précatégorie. Règles qui définissent la famille de relations 1Z(Ci+i) La relation U{Cl+\) contient la relation 1Z{C0) (règle (11)). fë(Ci+i) est une relation d'équivalence (règles (12)-(14)), et une congruence (règle (15)). Pour que C î+ i soit une précatégorie, il faut que la composition soit associative (règle (16)), et que les flèches id,4 soient des flèches identités (règles (17), (18)). Les règles (19)-(23) servent à assurer que 0 est pré-initial, et que push (A, B,C, f,g) est une pré-somme amalgamée. .4,BGObj(C 0 ) ; j,g€ATT(C0)(A,B) j = g G Avr(C0)(A, B) f = g€Arr(Ci+i)(A,B) A, B £ Obj(Ct+i) ; j e Arv(Ci+i)(A, f = f £ Atr{Ci+i)(A, B) (H) B) (12) .4,£GObj(C î + 1 ) ; j,g€AvT(Ci+l)(A,B) f = g € AiT(Ci+i)(A, B) g= f€An(Ci+i)(A,B) A,BeObj(Cî+1) ; f,g,h£Arr{Ci+i){A,B) j = g€An(Cl+l)(A,B) g = h G Arr(C,-+1 ){A, B) f= heATr(Ci+i)(A,B) (13) (14) A,B,CeObj(Ci+1) ; fJ'eATT{Ci+i)(A,B) ; g,g' G Arr(C,-+1)(B,C) f = f'eArr(Ci+l)(A,B) ; g = g' G Arr(C t+1 )(£,C) goj = g>oj'6Arr(Ci+1)(A,C) (15) A,B,C,D€Ob)(Ct+l) / G Arr(C i+1 )(.4,5) ; gGArr(C i + 1 )(B,C) ; h G Arr(C i+1 )(C, D) (hog)oj = ho(goj)e Arr(Ct+l)(A, D) (16) A,B€Ob)(Ci+l) jo\dA = ; f £ ATT(CJ+1)(A, jeArr(Ct+l)(A,B) B) (17) A,BeObj(Ci+1) ; jeArr(Ci+l)(A,B) i d B o / = /GArr(Ct+1)(A,B) (18) AeOb)(Ct+l) ; j,g£An(Ci+1)(0,A) j = g G Arr(C,-+i)(0, A) (19) A,B,C£Obj(Ci) ; /gArr(C,-)(^,B) ; g G ATT{CJ)(A,C) &! {A, B, C,j,g)oj = &2( A, B, C,j,g)og£ An(Ci+l)(A, push (A, B, C, j , g)) (20) 24 CHAPITRE 3. SYNTAXE: CATÉGORIE DES TERMES A, B,C, De Obi(Ci) ; f€Arr(Ci){A,B) ; g Z An{b)(A,C) f€An(Ci)(B,D) ; g'€ Arr(C,)(C,D) ; f o / = g'og G ATX{CJ){A,D) up {A, B,C,D,j,g,j',g') o&^A, B , C , / , g ) = / ' G Arr(C, +1 )(B, D) A,B,C,£>GObj(Ci) ; /GArr(C,)(A,B) ; 0 G Arr(C,)04,C) j ' GArr(C,)(B,P) ; g' G Arr(C,)(C, D) ; f o / = ^ o g G Arr(C;)(.4,D) up (A, B,C, £>,/,) 2 .4,B,C\£>GObj(C t ) ; / G Arr(C,)(A, B) ; ff G Arr(C,)(A,C) u, t; G Arr(Ci+i)(push (A, B,C, / , 5 ) , D) uo&l(A,B,C,j,g) uob2{A,B,C,j,g) = = vo&i(A,B,C,j,g)€AtT(Ci+l){B,D) vob2(A,B,C,j,g)£An(Ci+l)(C,D) u = t; G Arr(Ct+1)(push (.4, B , C , / , < / ) , £ ) Pour obtenir une suite de précatégories C,, il faut préciser les flèches identités et les compositions. Les flèches identités sont évidemment les termes id^ G Arr(C,)(A, .4) et les opérations de composition sont les fonctions o : Arr(C t )(B,C)x Arr(Ct)(.4, B) {9, j) -• -+ Arr(C,)(.4,C) 9oj . Lemme 3.5 Pour tout i > 0, on a: 1. Obj(C,)ÇObj(C 1+1 ): 2. V.4, B G Obj(C,-). Arr(C,)(.4, B) Ç Arr(C l+1 )(.4, B) ; 3. V.4, B G Obj(C,), K{Ci){A, B) Ç R(Ci+l)(A, B). Preuve. Par induction sur i. Pour i = 0, le point 1 provient de la règle (1), 1< point 2 provient de la règle (4), et le point 3 provient de la règle (11). Pour i + 1 on prouve les trois points en parallèle, par induction sur la structure des élément! de Obj(C, + i), Arr(C1+i) et ft(C,+i). Cela nécessite de considérer toutes les règle: (1)-(23). C Lemme 3.6 Pour tout i > 0, on a: 1. 1Z(Ci+\) est un€ congruence; 2. Ci+i est une précatégorie ; 3. l'objet 0 est pré-initial dans C,-+i. 3.3. PRECATÉGORIES d 25 Preuve. Toutes les propositions dérivent de façon évidente des règles qui définissent Obj(C,+i), Arr(C, + i) et 7£(C,+i). Plus précisément: 1. règles (12)-(15) ; 2. règles (5), (6) et (16)-(18) ; 3. règles (7) et (19). Exemple 3.1 Supposons que CQ contient trois objets A, B et C, et deux flèches / : .4 —» B et g : .4 —» C. On peut construire une pré-somme amalgamée de deux façons différentes : A, B.C G Obj(Co) ; / G Arr(C0)(A, B) ; g G Arr(C 0 )(A,C) , . P! = push (.4, B , C , / , 5 ) G O b j ( d ) W .4,C,B.GObj(C 0 ) ; g G Arr(C 0 )(A,C) ; / G Arr(C 0 )(.4, B) F 2 = push(.4,C,B, 5 ,/)GObj(C 1 ) m W On a également : .4,C,B, G Obj(Cp) ; g G Arr(C 0 )(.4,C) ; / G Arr(C 0 )(.4, B) , „ m &1(.4,C,B,ff,/)o(7 = &2(.4,C,B,5,/)o/GArr(C1)(.4,P2) ^ .4,B,CGObj(C 0 ) ; / G Arr(C 0 )(A,B) ; g G Arr(C 0 )(A.C) ,. >m 8il(A,B,C,j,g)oj = gi2(A.B,C,j,g)og G Arr(Ci)(.4, Px) l Z U ; Par la règle (10), on peut donc construire les termes « = up(A,B,C,P2,/,5,&i(A,C,B,ff,/),&2(.4,C,B, 1, V/l 6 Obj(Co), Arr(Cf-)(.4f 0 ) = 0 . Preuve. 3.4 Par induction sur la définition de Arv(Ct). D Simplification des flèches Dans cette section, nous définissons pour tout entier i > 0, un système de simplification des flèches de la précatégorie C,-+i. Il s'agit ici d'un outil technique qui nous permet de démontrer en section 3.5 que, pour tout i, la précatégorie C, est une extension conservatrice de CQ. Définition 3.10 (Flèche élémentaire) On dit qu'une flèche fj £ Arr(Ci){A, B) est élémentaire si et seulement si l'une des conditions suivantes est satisfaite. 1. / , G A r r ( C 0 ) ( A , B ) ; 2. / , = & f c ( . 4 , B , C , / , 5 ) ; 3. jj = up {A, B, C, D, / , g, / ' , g'); 4. / j S i d j r e t / ^ A r r f C b H X . J Q ; 5- fj =ix- Dans tout le reste de cette section, nous considérons les flèches de C, comme des compositions f = fn°jn-l°---°j\ avec, pour tout j G {l,..ra}, jj est une flèche élémentaire. L'entier n est appelé longueur du terme / . Cette présentation simplifiée est justifiée par la règle (16), c'est-à-dire l'associativité de la composition. 3A. SIMPLIFICATION DES FLECHES 27 Le système de simplification est composé de règles de simplification, qui définissent une relation —> sur les flèches de la précatégorie C%+\. On considère ensuite la fermeture réflexive et transitive, notée —>*, de la relation —>. Nous considérons des règles de simplification de Tune des deux formes suivantes. P (Axiome) P u —y u' => / —> / ' (Règle de contexte) où / , / ' , u et u' sont des flèches de la précatégorie C t +i, et P est l'ensemble des conditions qui assurent que les termes / , / ' , u et u1 sont bien formés. Intuitivement, si / —>* f1 (c'est-à-dire si la flèche / peut se simplifier en la flèche / ' ) , alors / et / ' sont équivalentes dans la précatégorie C,-+i. La réciproque n'est pas vraie. Autrement dit, le système de simplification est cohérent, mais pas complet, par rapport à l'équivalence dans Ci+i. On considère le système de simplification des flèches de Ci+i composé des règles suivantes. Axiomes .4, B G Obj(C,-+l) ; / G Arr(C, +1 )(.4, B) / o \AA —> j A,BeObi(Cl+1) (-•17) ; /€Arr(Ci+1)(.4,B) id B o / —> j A, B , C \ D G ObUC.) ; /GArr(Ci)(A,B) ; g G A r r ^ H ^ C ) / , €Arr(C,-)(B,D) ; g' G Arr(C,-)(C, D) ; f o f = g1 o g £ ATT(CJ)(A, up (A, B,C, D J, g, f, g1) o WA, B,C, f, g) ^>f H 18) D) .4, B,C,D G Obj(C-) ; / G Arr(C,)(A,B) ; g G Arr(C,)(A,C) f'eATr(Ci)(B,D) ; jf'€Arr(C,-)(C,£>) ; f o f = g'o g e ATT(CJ)(A, D) uP(A,B,C,D,j,gJ',g')ob2(A,B,C,j,g)-^g' ( [ ' 28 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES Règles de contexte .4, B,CG Obj(C i+1 ) ; / , / ' G Arr(C, +1 )(A,B) ; g G Arr(Ci+1)(B,C) ( f->r*gof-+gor A. B.C G Obj(C,-+1) ; / G Arr(C t+1 )(.4, B) ; g, g' G Arr(C, + 1 )(B,C) ; T ;—? g-^g'^goj^g'oj „.. ^ 15,) (-» 15 u) .4, B.C, D G Obj(C,) ; / G Arr(C,-)(^, B) ; g G Arr(C t )(.4,C) / ' € Arr(Ct-)(fl, D) ; up(A,B,C,D,j,g,j>,g>)-^up(A,B,C,D,j,g,j",g>) .4, B,C\£> G Obj(C) ; /GArr(C t )(A,B) ; g G Arr(C,)(A,C) /'€Arr(C,-)(B,I>) ; g' G Arr(C,-)(C, D) ; g" G Arr(C,-)(C, D) / / Q / = g / °flGArr(C 1 )(.4,D) ¢/ _ + g» ^ u p ( i 4 i 5 ) c , D, / , ff, /', g') —> up (.4, B, C, D, j , g, /', g") . ( [ ~"23l) ~* "j Remarque 3.2 Ce système de simplification ressemble à un système de réécriture (cf. par exemple [DJ90]). Il y a cependant deux différences avec les systèmes de réécriture classiques. 1. Nous avons besoin de prémisses pour assurer que les termes manipulés sont bien formés. 2. Nous n'autorisons pas toutes les règles de passage au contexte. Nous avons une règle de passage au contexte uniquement pour l'opérateur de composition (règles (-» 15i) et (—> 15ii)), et pour les deux derniers paramètres de l'opérateur up (règles (—y 23i) et (-> 23ii)). Lemme 3.8 Soit f G Arr(C;)(A, B). alors, ffeAvT(Ci)(A,B); 1. / — • / ' =» 2. / — • / ' = > Preuve. f = f'£AïT{Cl){A,B). Aucune difficulté. D Lemme 3.9 (Terminaison du système de simplification) Le système de simplification termine, c'est-à-dire qu'il n'existe pas de séquence infinie / i — > /2 — > • • • /n —> " • • • 3.4. SIMPLIFICATION Preuve. DES FLECHES 29 Pour chaque axiome / ' est un sous terme de / . Lemme 3.10 (Confluence du système de simplification) Le système de simplification est confluent, c'est-à-dire que si f —> f\ et f —> /2, alors il existe f1 tel que f\ —>M f1 et /2 —>* f. Preuve. Aucune difficulté. D Définition 3.11 (Forme normale) Soit une flèche / G Arr(C,+i)(.4, B). On dit que la flèche / est sous forme normale, ou irréductible, si il n'existe aucune simplification Proposition 3.1 Toute flèche f G Arr(C,)(.4, B) a une forme normale. Preuve. C'est une conséquence immédiate de la terminaison et confluence du système de simplification. D La forme normale de / sera notée N(f). Théorème 3.1 (Cohérence de la simplification) Soit f G Arr(C,-)(-4, B). On a / = ,V(/)GArr(C,)(A,B). Preuve. Par induction sur la longueur de la simplification / —•" Af(/). Pour une simplification de longueur 0, le résultat est évident. Supposons / —> / ' —>m jV(f'). D'après le lemme 3.8, / = / ' G Arr(C,)(.4, B). Ensuite, par hypothèse d'induction, on a / ' = N{f) € Avv{Ci){A,B), d'où / = jV(f')eArv(Ct)(A,B). D Le théorème suivant affirme que toute flèche pour laquelle le domaine et le codomaine sont dans CQ a pour forme normale une flèche de CQ. Théorème 3.2 (Forme normale (1)) Soit A,Be Obj(Co) et me Avr{Ci){A, B). On a M{m)eATv{C0){A,B). 30 CHAPITRE Preuve. 3. SYNTAXE: CATEGORIE DES TERMES Soit A, B e Obj(C0) et m G Arr(Ct-)(A, B). Soit Af(m) = mn o m n _i ---77120 m\, avec pour tout j G { 1 , . . . n } , mj est une flèche élémentaire. Pour tout j G { 1 , . . . n}, on a • Si m3 n'est pas une flèche de CQ, alors mj ^ id^, sinon nécessairement n > 2 et donc A/"(m) n'est pas irréductible. • m3 ^ j Y , car d'après le lemme 3.7, Arr(Cf)(A, 0 ) = 0 . Par conséquent, pour tout j G { 1 , . . .n}, l'une des conditions suivantes est vérifiée 1. m J GArr(C 0 )(A',y); 2. mj s &*(Ao, Ai, ^ 2 , / 1 , / 2 ) , avec fc€{l,2}; 3. mj = up (A 0 , Ai, A2, A3, /1,/2, /{, / 2 ) Par l'absurde, supposons qu'il existe j tel que mj ¢. ATT(CQ)(X,Y). Soit jo le plus r petit j qui satisfait cette propriété. On a donc mj 0 G Arr(C;) (X, Y ), avec À'GObj(Co). Par conséquent mjo = &k(A0, Ai, A 2 , /1,/2). Si m J 0 + i = up (.4o, Ai, A2, A3, / 1 , /2, /{, /2), alors AT(m) n'est pas irréductible, donc m jo+i = & ^ ( A 0 , A i , A , 2 , / i , , / 2 ) . Finalement, on obtient mn = Stk»{A0",Aï",A2"Jl",f2"). ce qui est en contradiction avec JBGObj(Co). Par conséquent, pour tout jG{1,.. mj est une flèche de CQ, et donc A^(m) G Arr(Co)(A, B). .n}, D Théorème 3.3 (Forme normale (2)) Soit A G Obj(Co), B = push (A 0 , Ai, A 2 ,/1,/2) G Obj(C), m G Arr(C,-)(A, B). Posons N(m) = m n o m n _i o - - -o m\, avec n > 1 etVj G { 1 , . . .n}, mj est une flèche élémentaire. Alors, 1. m n = &fc(A0, Ai, A 2 ,/1,/2), avec ke {1,2}; 2. ss n > 2, alors m n _i o • • -o m\ G Arr(Ci_i)(A, A^). 3.4. SIMPLIFICATION DES FLÈCHES 3i Preuve. Similaire à la preuve du théorème 3.2. La preuve complète est développée n en appendice A.l. Théorème 3.4 (Forme normale (3)) Soit A = push {A0, Ai, .4 2 , / i , / 2 )eObj(C,), BGObj(Co) et mGArr(Ci)(A, B). Posons Af(m) = mno m n _i o • • • o TOI, avec n > 1 et Vj G { 1 , . . .n}, mj est une jtèche élémentaire. Alors m, = up {AQ,A\,Ai, A3, / I , j2,gi,g2)- Preuve. Similaire à la preuve du théorème 3.2. La preuve complète est développée a en appendice A.2. La forme normale d'une flèche n'est pas unique relativement à l'équivalence dans C{. Dans le cas général, m = m'GArr(C i )(X,y) #> j\f{m) = Af{m'). Par exemple, on a &!(.4, B.C, j,g)oj = &2(.4, B , C , j , g ) o g £ Arr(C,-){A,push {A, B.C, j,g)). Ces deux flèches sont irréductibles et équivalentes dans C,, mais ne sont pas identiques. Par contre, on a VX,y'GObj(C 0 ), TO = TO'GArr(C)(A\Y) =• M (m) = Af(m') G ATT{C0){X,Y). Pour montrer ce résultat, nous démontrons le théorème suivant. Théorème 3.5 ( "Unicité* de la jorme normale) Soit m, m' G Arr(C,-)(A\ Y), tels que m = m' G Arr(Ct-)(A\ Y). 1. Si A', F GObj(Co), alors y (m) = yV(m') G Arr(C0)(A:, Y). 2. Si X G Obj(Co), V = push {A0, AUA2, /1,/2), a/ors VZ G Obj(Co), V/i G ATT{Ct){Y,Z), on a AT (h o m) = M {h oTO')G Arr(C 0 )(X, Z). 3. S/ A' = push (.40, Ai, A2, / 1 , /2), V G Obj(C 0 ), a/ors VW G Obj(Co), VpG Arr(C,-)(W^, X), on a M {m o p) = M {m'o p) G Arr(C0)(W, Y). 4. Si X = push (A 0 , Ai, A2, /1, /2), Y = push (A{„ A\,A'2, / ( , /£), a/ors VW, Z G Obj(Co), V/i G An{Ct)(Y, Z), Vp G Arr(C,-)(W, X ) , on a Af(homop)=Af(hom'op)e Arr(C0) (W, Z). 32 CHAPITRE 3. SYNTAXE : CATEGORIE DES TERMES Preuve. On prouve les points 1 à 4 par induction sur i. Pour i = 0, le point 1 est évident, et il n'y a rien à prouver pour les points 2 à 4. Pour i + 1, on doit faire une induction sur la longueur de Af(h) pour prouver les points 2 et 4. On prouve alors les points 1, 2, 3, 4 en parallèle, par induction sur la longueur de la preuve que m = m'£ Arr(Ci+i)(X,r). Cette preuve est détaillée en Appendice A.3. 3.5 • Extensions conservatrices La suite de précatégories C; satisfait deux propriétés importantes: on n'introduit pas de nouvelles flèches entre des objets de CQ, et on n'introduit pas de nouvelles équivalences entre des flèches de CQ. On dit que Ci est une extension conservatrice deC0. Pour tout i < j , on définit un préfoncteur Jij : Ci —> C3 par: / • • C • -> C A i-* .4 f ^ f Ji.j est bien un préfoncteur car d'après le lemme 3.5, • .4€Obj(C,)=>A€Obj(C,); • / G ATT(d)(A, B) => / G Arr(C J )(A, B) ; . / = / ' G Arr(C t )(.4, B) = • / = / ' G Arr(C})(A, B). Théorème 3.6 Pour tout entier j , la précatégorie Cj est une extension conservatrice de Co. Autrement dit, le préjoncteur Joj est plein et jidèle. Ce théorème est équivalent à: V / G N , Wl,BGObj(C 0 ), 1. M G Arr(Cj)(i4, B), 3h' G Arr(CQ)(A, B) ; /i = /i' G Arr(C J )(A, B) ; 2. V/i',/i"GArr(Co)(.4,B), /i' = /i"GArr(C J )(^,B) =j> h'= h" € An(C0)(A,B). 3.6. PRECATEGORIE Preuve. TERME(Cp) 33 C'est une conséquence immédiate des théorèmes 3.1, 3.2, et 3.5. 1. Il suffit de prendre h' = M{h). D'après le théorème 3.2, M (h) G Arr(C 0 )(A, B). 2. h' = h" G Arr(Cj)(A, B), donc d'après le théorème 3.5, M{ti) = N{h") e AU(CQ)(A,B). De plus, d'après le théorème 3.1, on a jV(h') = jV{h") = h'eArr{CQ){A,B) h"£ArT{C0){A,B) d'où le résultat. Remarque 3.3 En général, pour 1 < i < j , C3 n'est pas une extension conservatrice de C{. En effet : 1. Le préfoncteur J Z J n'est pas plein, car la règle (10) peut introduire dans la précatégorie Cx+\ des nouvelles flèches entre des objets de C{. Dans l'exemple 3.1, u est une flèche entre deux objets de C\ qui fait partie de C2, mais pas de C\. 2. Le préfoncteur J,-j n'est pas fidèle, car deux flèches de Ct peuvent être équivalentes à une troisième flèche de C;+i (et donc, par transitivité, équivalentes dans C;+i), sans être équivalentes dans C{. On peut donc introduire dans Cz+i des nouvelles équivalences entre flèches de C{. 3.6 P r é c a t é g o r i e TERME(C 0 ) Nous pouvons maintenant définir la précatégorie des termes, qui va nous servir de syntaxe pour les constructions de colimites. Les objets de cette précatégorie sont les éléments de Obj(C t ), pour i quelconque, et les flèches entre deux objets A et B sont les éléments de Arr(C,)(A, B), pour tous les j tels que A,B G Obj(Cj). De plus, deux flèches sont équivalentes si et seulement si elles sont équivalentes dans un des ensembles Arr(C,-)(A, B). On définit donc la précatégorie TERME(C 0 ) comme la "limite" de la suite de précatégories C{. Définition 3.12 (Précatégorie TERME(C0)) La précatégorie des termes TERME(C 0 ) est définie de la façon suivante. • L'ensemble des objets est 00 Obj(TERME(C0)) = (J 0b J( C «)i=0 34 CHAPITRE 3. SYNTAXE: CATEGORIE • Soit .4, B G Obj(TERME(C 0 )). Il existe A; G N tel que A,B€ L'ensemble des flèches de A vers B est DES TERMES Obj(Ck). oo Arr(TERME(C 0 ))(^, B) = \J Arr(C,)(4, B). i=k • Soit .4, B G Obj(TERME(C 0 )). Il existe k G M tel que A,BÇ La relation d'équivalence sur Arr(TERME(Co))(>l, B) est K(TERME{C0))(A, B) = ( J Obj(Cjt). K{d)(A,B). i=k D'après le lemme 3.5, ces ensembles sont bien définis. En particulier, la définition des ensembles Arr(TERME(C 0 ))(4, B) et 7e(TERME(C0))(>l, B) est indépendante de l'entier k choisi. Proposition 3.2 TERME(Co) est une précatégorie. Soit J : CQ -> TERME(Co) le préfoncteur défini par J : C0 -> TERME(Co) A H-> A j -* /• T h é o r è m e 3.7 La précatégorie TERME(Co) est une extension conservatrice de CQ. Autrement dit, le préfoncteur J : CQ —> TERME(Co) est plein et fidèle. Par conséquent, dans TERME(Co), on n'ajoute pas de flèche entre des objets de CQ, et on n'ajoute pas d'équivalence entre flèches de CQ. Cela montre la cohérence hiérarchique de la construction. Preuve. D'après le théorème 3.6, VA: G N, la précatégorie Ck est une extension conservatrice de CQ. 1. Soit A,Be Obj(Co), et h G Arr(TERME(C 0 ))(A, B). Il existe A: G N tel que h G Arr(Cfc)(A, B). Comme Ck est une extension conservatrice de CQ, il existe h' G Arr(C0)(A, B), tel que h = hf G Arr(C*)(A, B), et donc h = h' G Arr(TERME(C 0 ))(A, B). 2. Soit A, B G Obj(Co), et h', h!1 G Arr(C 0 )(A, B), tels que h! = h!1 G Arr(TERME(C 0 ))(A, B). Il existe A: G N tel que h1 = h11 G Arr(CA:)(A, B). Comme Ck est une extension conservatrice de CQ, /i , = A ,, GArr(C 0 )(A, J B). 3.6. PRECATEGORIE TERME(C 0 ) 35 Théorème 3.8 La précatégorie TERME(Co) est jîniment pré-cocomplète. Plus précisément, 1. l'objet 0 est un choix d'objet pré-initial dans TERME(Co) >' 2. «i A, B,C G Obj(TERME(C 0 )), / G Arr(TERME(Co))(4, B) et g Ç Arr(TERME(C 0 ))(A,C), alors le triplet (push (A, B,C,j, g), &!(.4,B,C,/,5), &2(A,B,C, j,g)) est un choix de pré-somme amalgamée de B et C par rapport à f et g dans TERME(Co)Preuve. 1. L'objet 0 est pré-initial. Soit AGObj(TERME(C 0 )). Il existe k > 1 tel que Ae Obj(Cjfc). Donc on a une flèche j 4 G Arr(C*)(0, A) Ç Arr(TERME(C o ))(0, A). Soit deux flèches M, y G Arr(TERME(C o ))(0, A). Il existe A:' > 1 tel que u, v G Arr(Cfc#)(0, A), donc d'après la règle (19), u = v G Arr(£V)(0, A) et donc u = v G Arr(TERME(C o ))(0, A). 2. La preuve est similaire. Considérons une précatégorie £ ayant un objet pré-initial choisi 0e et des présommes amalgamées choisies. Si A, B et C sont trois objets de £, et /GArr(£)(A, B), g G Arr(£)(A,C) deux flèches de £, on note (pushs(A,B), tel que / ' o / = g'og G Arr(£)(4, D), on a un choix de flèche up£(A, B,C, £>, / , 5 , /',g') G Arr(£)(p«s/» f (4, B, C , / , £. Alors il existe un unique préfoncteur G : TERME(Co) -> S tel que • G oJ = F; .G(gof)=G(g)oG(f); • G(id,4) = idG(A) » • G(0) = 0e ; • G('iA)=j^(A); . G(push (A, B, C, f, g)) = pushs(G(A), G(B), G(C), G(f), G (g)) ; .G(8il(A,B,CJ,g)) = ksl(G(A),G(B),G(C),G(f),G(g)); .G(b2(A,B,C,f,g)) = ke2(G(A),G(B),G(C),G(f),G(g)); . G(up(A,BX\DJ,g,f',g') = uPHG(A),G(B),G(C),G(D),G(f),G(g),G(f),G(g')). La précatégorie TERME(C0) est donc librement engendrée par objet pré-initial choisi et pré-sommes amalgamées choisies. Intuitivement cela signifie que la précatégorie TERME(Co) satisfait les propriétés suivantes. 1. Toutes les constructions (de pré-colimites sélectionnées, c'est-à-dire utilisant l'objet pré-initial et les pré-sommes amalgamées) sont distinctes. 2. TERME(Co) ne contient pas d'objets ou flèches autres que ceux de CQ et ceux obtenus par les constructions de pré-colimites sélectionnées. Ces deux propriétés correspondent respectivement à l'existence et l'unicité du préfoncteur G. Preuve. On construit un préfoncteur G : TERME(C 0 ) -* £ par induction sur la structure des objets et flèches de TERME(C 0 ). On montre ensuite que ce préfoncteur est unique. La preuve est détaillée en Appendice A.4. O Ce théorème permet d'interpréter, c'est-à-dire de donner une sémantique aux termes. Une précatégorie d'interprétation est une précatégorie avec un objet préinitial choisi et des pré-sommes amalgamées choisies. À partir d'une interprétation de CQ, c'est-à-dire un préfoncteur SQ : CQ —> £ on obtient une interprétation des termes, c'est-à-dire un préfoncteur S : TERME(Co) -> £. 3.7. CATEGORIE Terme{C0) Cette précatégorie £ peut par exemple être la catégorie Spec (considérée comme une précatégorie, et accompagnée d'un choix d'objet pré-initial et de choix de présommes amalgamées), ou une catégorie de classes d'algèbres permettant d'interpréter les spécifications de base. Dans le chapitre 4, la précatégorie d'interprétation considérée est DIAGR(Co). L'interprétation des objets et flèches de CQ est donnée par le préfoncteur Ic0 : CQ —> DIAGR(Co). D'après le théorème 3.9, cette interprétation peut être prolongée sur les termes en un préfoncteur V : TERME(Co) -> DIAGR(C0). C'est ce préfoncteur qui va nous permettre, dans le chapitre 4, d'associer à tout terme un diagramme. 3.7 Catégorie Terme(Co) La catégorie Terme(Co) est la catégorie associée à la précatégorie TERME(Co). Définition 3.13 (Catégorie des termes) La catégorie Terme(Co) est définie de la façon suivante. • Les objets de Terme(Co) sont les objets de TERME(Co). • Pour toute flèche / G Arr(TERME(C 0 ))(A, B), [f] : A -> B, classe d'équivalence de / modulo 1Z(TERME(CQ))(A, B), est une flèche de Terme(Co). On a un foncteur J : CQ —> Terme(Co) associé au préfoncteur J : CQ —> TERME(Co). Théorème 3.10 La catégorie Terme(Co) est une extension conservatrice de CQ. Autrement dit, le foncteur J : CQ —> Terme(Co) est plein et fidèle. Preuve. D'après le théorème 3.7, le préfoncteur J : CQ —> TERME(Co) est plein et fidèle, donc le foncteur associé J : CQ —> Terme(Co) est également plein et fidèle. D Théorème 3.11 Terme(Co) est une catégorie finiment cocomplète. Plus précisément, 1. l'objet 0 est initial dans Terme(Co) ; 2. si A, B et C sont des objets de Terme(Co), [/] : A -> B et [g] : A -> C sont des flèches de Terme(Co), alors le triplet (push (A. B,C,f, g), [&! (A, B,C,/,(?)], [&2(A, B,C,f,g)]) est une somme amalgamée de B et C par rapport à [f] et [g] dans Terme(Co). 38 CHAPITRE Preuve. 3. SYNTAXE: CATEGORIE DES TERMES Application des lemmes 3.3 et 3.4. D La catégorie Terme(Co), bien que finiment cocomplète, n'a pas de sommes amalgamées choisies. En effet, si / ' est un autre représentant de [/], et g' un autre représentant de [g], c'est-à-dire si [/] = [/;] et [g] = [g'] dans Terme(C0), alors les triplets (push (A, B,C,f, g), [&! (A, # , C \ / , ( / ) ] , [&2(A, (push (A, B,C, f',g'), [&i(A,B,C,f',g% [k2(A, B,C,f,g)]) B.C,f',g')]) sont deux choix différents de somme amalgamée de B et C par rapport aux flèches [/] et [g]. Par conséquent, la catégorie Terme(Co) n'est pas librement engendrée par objet initial choisi et sommes amalgamées choisies. Il y a en effet "trop de choix de sommes amalgamées" dans Terme(Co). Intuitivement, les constructeurs push, &i et &2 dépendent des représentants choisis pour [/] et [g], et donc les choix de pré-colimites de TERME(Co) ne sont pas conservés en passant au quotient. Par contre, on peut retrouver une catégorie librement engendrée par objet initial choisi et sommes amalgamées choisies en "fusionnant les choix multiples de sommes amalgamées". Cette construction est décrite dans le paragraphe suivant. 3.8 Catégorie libre C(CQ) Dans ce paragraphe, nous construisons, à partir de la précatégorie TERME(Co), une catégorie C(CQ) librement engendrée par objet initial choisi et sommes amalgamées choisies. L'idée est de définir une relation d'équivalence à la fois sur les objets et les flèches de TERME(Co), afin de fusionner les choix multiples de sommes amalgamées. La relation d'équivalence sur les flèches est plus forte que celle de TERME(Co), c'est-à-dire vérifie / = 0GArr(TERME(C o ))(A,fî) => f - g. Cette construction est inspirée de la "réécriture d'objets" proposée par F. Cury [Cur91]. Nous commençons par définir la relation d'équivalence ~ sur Obj(TERME(C 0 ))Deux objets équivalents sont isomorphes, mais deux objets isomorphes ne sont pas nécessairement équivalents. Nous définissons d'abord une sous-précatégorie Iso(Co) de TERME(Co). La précatégorie Iso(C0) a pour objets les objets de TERME(C 0 ), et pour flèches certains isomorphismes de TERME(Co). Ces isomorphismes vont correspondre aux équivalences entre objets de TERME(Co). Définition 3.14 (Précatégorie Iso(C0)) • L'ensemble des objets de Iso(C0) est l'ensemble des objets de TERME(Co). 3.8. CATEGORIE LIBRE C{C0) 39 • L'ensemble des flèches de Iso(Co) est défini inductivement de la façon suivante. - Pour tout objet A de TERME(C 0 ), id. 4 €Arr(Iso(C 0 ))(.4,^). - Soit / G Arr(Iso(C0))(.4, B) et g € Arr(Iso(C 0 ))(fl,C). Alors, gojeATT(lso(C0))(A,C). - Soit six objets Ai, Bi,Ci, A2, B2,C2 de TERME(Co), et trois flèches de Iso(Co) ^€Arr(Iso(C0))04i,A2), <£ B eArr(Iso(Co))(fli,fî2), ^ C € Arr(Iso(C 0 ))(C!,C 2 ). Soit quatre flèches de TERME(C 0 ) / i € Arr(TERME(C 0 ))(^i,fli), ^eArrCTERMEfCoM^d), / 2 e Arr(TERME(C 0 ))(.4 2) S 2 ), 5 2 €Arr(TERME(C 0 ))(/l 2 ,C 2 ), telles que 4>Boh=f2oct>Ae Arr(TERME(C 0 ))(A 1 , B2), 0cop1=^2o^GArr(TERME(Co))(A1,C2). Il existe alors une flèche up(.4 1 ,B 1 ,Ci,push(A 2 ,fi 2 ,C 2 ,/ 2 ,flf 2 ),/i,flfi, &i (A2, B2,C2, f2, g2) o 4>B, & 2 (A 2 , B2, C2, f2, g2) o 0 C ) de push (Ai,B\,C\, l'on note f\,g\) vers push (A2, B2,C2, f2,g2). iso(fi, Cette flèche, que g\,f2, g2, 4>A, B, Arr(Iso(C 0 ))(B, A)) La fonction inv, qui associe à toute flèche de Iso(Co) de A vers B une flèche de Iso(Co) de B vers A, est définie inductivement sur la structure des flèches de Iso(Co) de la façon suivante. • inv(idA) = id,4 ; 40 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES • inv(g o / ) = inv(f) o inv(g) ; • inv(iso(fi,gi, f2,g2,A,(i>B,c)) iso(f2,g2,fi.gi,inv(4)A),inv(4>B),inv(4)c))On vérifie sans difficulté que, pour toute flèche / G Arr(Iso(Co))(A, B), on a bien • inv(f) e ATV(\SO(CQ))(B, A); • inv(f) o / = id 4 € Arr(TERME(C 0 ))(A, A) ; • / o inv(f) = \àB G Arr(TERME(C 0 ))(5, B). Nous pouvons maintenant définir la relation d'équivalence sur les objets de TERME(Co). Définition 3.16 (Relation d'équivalence ~ sur les objets de TERME(Co)) Deux objets A et B de TERME(Co) sont équivalents si et seulement si il existe un isomorphisme de A vers B dans Iso(Co)Notation. Si A et B sont équivalents, on note A ~ B, ou, pour préciser l'isomorphisme (p de A vers S, 0 h A ~ fi. Intuitivement, on peut considérer la flèche

inv() h B ~ A ; • transitive car <£i h ,4 ~ B, 2 o 0! h A ~ C. D Soit un objet A de TERME(Co). On note [[A]] la classe d'équivalence de A modulo ~ . Autrement dit, [[A]] = {Be Obj(TERME(C 0 )) ; A - B}. À chaque preuve de A ~ B est associé un isomorphisme <£G Arr(TERME(Co))(A, B). La proposition suivante indique que l'isomorphisme (f> ne dépend pas de cette preuve. Proposition 3.3 Si è\ h A ~ B et (f>2 h A ~ B, alors 4>x=(t>2e Arr(TERME(C 0 ))(A, B). Esquisse de la preuve. On définit un système de réécriture sur les flèches de Iso(Co) de la façon suivante. (Les prémisses qui assurent que tous les termes sont bien formés sont, pour faciliter la lecture, omis.) 3.8. CATEGORIE LIBRE C(C0) £1 Axiomes • 3 o (2) o cf>i • 0 o id^ — > • id,4 o (j> — > (f> • iMf2,92j3,g3,iïA,*lyB,iïc)°iso(fli9l,f2,g2,$A,$B,$c) —• iso(fl,gl, /3,flf3, ll>A°A,ll>B° B, 0C o 0c) Règles de contexte • (j) > (f/, ift • 04 • &'AI B > if)1 O (j)1 > 0 ' => \\) O <\) • Bi 0 C • c => iso{f\,g\,f2,Q2,A,B,c) —• iso(fl,gï,f2,g2,(t>,A,^B,(l>,c) On montre alors successivement les points suivants. 1. Si 0 h A - B et 0 —>' ', alors 0' G Arr(Iso(C0))(A, B). 2. Le système de réécriture est cohérent. Si 0 h A ~ B et 0 —•* <£', alors 0 = ' G Arr(TERME(C 0 ))(A, B). 3. Le système de réécriture est confluent. 4. Le système de réécriture termine. 5. D'après 3 et 4, toute flèche (f> de Arr(Iso(Co))(A, B) a donc une forme normale notée V((j>). D'après 2, on a 0 = V(0) G Arr(TERME(C 0 ))(A, B). 6. On montre, par induction sur la structure de A et B, que 0i h A ~ B, 0 2 h A - B => V(0i) = V(0 2 ). 7. On déduit immédiatement de 5 et 6 que 0i h A - B, 0 2 h A ~ B =• 0i = 0 2 G Arr(TERME(C 0 ))(A, B). Remarque 3.4 Si 0 h A ~ B, l'isomorphisme 0 correspond à une preuve que A ~ B et V(0) correspond à la normalisation de cette preuve. 42 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES Notation. Si h- .4 ~ B, la flèche 0 : A -» B de Iso(C0) est notée (A, B) : A -» B. Cette notation est justifiée par la proposition 3.3. À partir de cette relation d'équivalence sur les objets de TERME(Co), nous définissons une relation d'équivalence sur les flèches de TERME(Co). Définition 3.17 (Relation d'équivalence ~ sur les flèches de TERME(Co)) Soit deux flèches / G Arr(TERME(C 0 ))(A, B) et / ' G Arr(TERME(C 0 ))(A', B'). Les flèches / et / ' sont équivalentes si et seulement si A ~ A', B^B1 et / ' o (A, A') = (B, B1) o f G Arr(TERME(C 0 ))(A, B1). On note / ~ / ' . Lemme 3.12 La relation ~ sur les flèches de TERME(Co) est une relation d'équivalence. Preuve. La relation ~ est • réflexive car (.4, A) = id,4 G Arr(TERME(C 0 ))(A, A) ; • symétrique car inv(A, B) = (B, A) G Arr(TERME(C 0 ))(B, A) ; • transitive car (B.C)o(A,B) = (A,C) G Arr(TERME(C 0 ))(A,C). D Soit /G Arr(TERME(C 0 ))(A, B). On note [[/]] la classe d'équivalence de / modulo ~ . Autrement dit, [[/]] = {/' € Arr(TERME(C 0 )M4', B') ; j ~ / ' } . Lemme 3.13 V/, / ' € Arr(TERME(C 0 ))(.4, B), / = /'€Arr(TERME(C 0 ))(A,B) => / ~ / ' . Preuve. O n a / ' o (.4, A) = (B,B)oje Arr(TERME(C 0 ))(4i B) car (A, A) = \dA e Arr(TERME(C 0 ))(A, A) (B, B) = \dB € Arr(TERME(C 0 ))(fl, B). Nous définissons maintenant la catégorie C{CQ). Intuitivement, C(Co) a pour objets les classes d'équivalence modulo ~ d'objets de TERME(Co) et pour flèches les classes d'équivalence modulo ~ de flèches de TERME(Co). 3.8. CATÉGORIE LIBRE C(C0) 43 Définition 3.18 (Catégorie C{C0)) • Objets. Soit un objet A de TERME(C 0 ). Alors, [[A]] est un objet de £{C0). • Flèches. Soit / e Arr(TERME(C 0 ))(.4, B). Alors, [[/]] : [[A]] -> [[B]] est une flèche de C(C0). Cette définition est correcte car si jeArr(7ERME(C0))(A,B), j'eArr{TERME(C0))(A',B') et / ~ / ' , alors, on a .4 ~ A' et B ~ B'. • Composition. Soit /eArr(TERME(C 0 ))(.4, B) et 0€Arr(TERME(C o ))(C, D), avec B ~ C. On pose [[«?]] o [[/]] = [[5 o (B, C) o / ] ] . Cette définition est indépendante des représentants j et g choisis. En effet, soit / ' e Arr(TERME(C 0 ))(.4', B') et g' € Arr(TERME(C 0 ))(C, D') tels que / ~ / ' et g ~ 5'. On a les égalités suivantes dans Arr(TERME(C 0 ))(-4, D') : (D,D')ogo(B,C)oj = g'o(C,C)o(BX')oj = g'o(B.C")oj = g'o(B',C')o(B,B')oj = (car g ~ g') ( c a r ( C , C > o ( £ J , C ) = (fî,C'» (car <5',C> o ( 5 , B') = {B,C")) g'o(B',C')oj'o(A,A') (car/~/') Par conséquent, g o (B, C) o j ~ g' o (B1, C") o j ' , et donc [[go(BX')oj]] = [[g'o(B',C')oj')]. La composition est évidemment associative. • Identités. Soit [[.4]] un objet de C(C0). Alors [[id^]] : [[A]] -+ [[A]] est une flèche identité. Remarque 3.5 Si A ~ B, alors id^ ~ (.4, B). Par conséquent, les flèches (.4, B) de Iso(Co) correspondent à des identités [[{A, B)}] = [[id^]] = [[idB]] dans C{C0). On a un préfoncteur [[-]] : TERME(C 0 ) -+ £{C0) défini de la façon suivante: [[-]] : TERME(Co) - • C{C0) A - • [[A]] f H. [[/]]. C'est bien un préfoncteur d'après le lemme 3.13. Ce préfoncteur est associé à un foncteur [[-]] : Terme(C0) -»• C(C0), défini par: [[-]] : Terme(Co) - • C(C0) A _• [[A]] [f] -• [[/]]• Proposition 3.4 La catégorie C(CQ) est une extension conservatrice de CQ. Autrement dit, le foncteur [[-]] o J : C 0 - > C(CQ) est plein et fidèle. 44 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES Preuve. On utilise le fait que le foncteur J : CQ —• Terme(Co) est plein et fidèle (théorème 3.10). On remarque également que la classe d'équivalence d'un objet de CQ ne contient que cet objet. Autrement dit, pour tout objet A de CQ, [[J(A)]\ = {J(A)}. En effet, dans la définition 3.14, on n'introduit pas d'équivalence entre objets de CQ autres que les identités. Le foncteur [[-]] o J est plein. Soit deux objets A et B de C0, et une flèche h : [[J(A)]\ -+ [[J{B)]] de C(C0). Par définition de [[-]], il existe une flèche g de TERME(Co) telle que [[g]] = h, qui a pour domaine J(A) et pour codomaine J(B). Comme le foncteur J est plein, il existe donc une flèche / : A -» B de CQ telle que J(f) = g, ce qui implique que [[J(f)]\ = [[g]) = h. Le joncteur [[-]] o J est fidèle. Soit deux flèches / . g : A ->• B de C0 telles que [[ J(f)~J(g) => (J(B), J(B)) o J(j) = J(g) o {J(A),J(A)) => ./(/) = J(g) e Arr(TERME(C0))(A, B) => j = g G Arr(TERME(C 0 ))(A, B) (car J est fidèle) Théorème 3.12 La catégorie C(CQ) est jiniment cocomplète. Plus précisément, 1. l'objet [[0]] est un objet initial choisi dans C(CQ) ; 2. si [[A]], [[B]] et [[C]) sont des objets de C(CQ), [[/]] : [[A]] -+ [[B]] et [[g]] : [[A]] -> [[C]] sont des flèches de C(Co), alors le triplet ([[push(.4,B,C,/, 5 )]], [[&!(/!,£,C,/,s)]], [[&2(A,B,CJ,g)]]) est un choix de somme amalgamée de [[B]] et [[C]] par rapport à [[/]] et [[g]] dans C(CQ). On vérifie facilement que le choix de somme amalgamée ne dépend pas des représentants A, B, C, f et g respectivement choisis pour [[A]], [[B]], [[C]], [[/]] et [[g]]. Le triplet ([[push (.4, B,C,/,(/)]], \[*ti(A,B,CJ,g)]), [[& 2 (A,B,C,/, £ qui conserve fortement l'objet initial choisi, les sommes amalgamées choisies, et tel que H o [[-]] o J = F. Esquisse de la preuve. On considère le foncteur G : Terme(Co) —• £ associé au préfoncteur G : TERME(Co) -» £ du théorème 3.9. Existence. On montre que ÏY- A~* A' => G (A) = G (A') et G (à) = idG(A), par induction sur la longueur de la preuve que h A ~ A7. On en déduit que / - / ' = > • G(f) = G(f). Par conséquent, il existe un unique foncteur H : C(CQ) —• £ tel que H o [[—]] = G. On a donc H o [[-]] o J = G o J = F. On vérifie que le foncteur H conserve fortement l'objet initial choisi et les sommes amalgamées choisies. Unicité. Soit Hf : C(CQ) —> £ un foncteur qui conserve fortement l'objet initial choisi, les sommes amalgamées choisies, et tel que H' o [[-]] o J = F. D'après le théorème 3.9, on a donc H o [[-]] = H' o [[—]]. Comme [[-]] est surjectif sur les flèches et les objets, on en déduit que H = H'. a 3.9 Conclusion Nous avons proposé la construction d'une précatégorie TERME(Co) à objet préinitial choisi et pré-sommes amalgamées choisies pour décrire des constructions de colimites sur une petite catégorie de base CQ. Cette précatégorie de termes constitue une syntaxe pour les constructions modulaires. Nous avons montré que TERME(Co) est une extension conservatrice de CQ (théorème 3.10), c'est-à-dire que le préfoncteur d'inclusion J de CQ dans TERME(Co) est plein et fidèle. Cela signifie d'une part que TERME(Co) ne contient pas de flèches entre des objets de CQ autres que celles contenues dans CQ, et d'autre part que 46 CHAPITRE 3. SYNTAXE: CATEGORIE DES TERMES TERME(Co) ne contient pas d'égalités entre flèches de CQ autres que celles qui proviennent de CQ. Nous avons montré que la précatégorie TERME(Co) est librement engendrée par objet pré-initial choisi et pré-sommes amalgamées choisies (théorème 3.9). En passant au quotient, on obtient une catégorie finiment cocomplète Terme(Co), qui est également une extension conservatrice de CQ (théorèmes 3.10 et 3.11). Enfin, nous avons montré comment construire, à partir de TERME(Co), une catégorie C(CQ) librement engendrée par objet initial choisi et sommes amalgamées choisies sur CQ (théorème 3.13). Annexe A Preuves sur la syntaxe A.l Preuve du théorème de forme normale (2) Nous montrons le théorème 3.3, page 30. Théorème 3.3 (Forme normale (2)) Soit A G Obj(Co), B = push (A0, Au A2, / i , / 2 ) G Obj(d), m G Arr(C,)(A, B). Posons Af(m) = mn o m n _i o • • • o m\, avec n > 1 et V/ G { 1 , . . . ra}, m3 est une flèche élémentaire. Alors, 1. mn = &k(A0, Ai, A 2 , / i , / 2 ) , avec A: G {1,2}; 2. 5/ rc > 2, a/ors ran_i o • • • o m\ G Arr(C;_i)(A, A*). Preuve. Nous montrons successivement les points 1 et 2. 1. On a • mn i Arr(C 0 )(B', B), car B £ Obj(C 0 ). • ran ^ idx, sinon nécessairement w > 2 et donc M (m) n'est pas irréductible. • mn ^ j x , car Arr(C^)(A,0) = 0 . On fait une induction sur n. Si n = 1, alors comme A G Obj(Co), on a mi = & j t ( A 0 , A i , A 2 , / ! , / 2 ) . Pas d'induction : par l'absurde, si mn ^ &À:(AO, A I , A 2 , / I , / 2 ) , alors mn = u p ( A ^ A ; , A ' 2 , B , / i ^ , ^ ^ Par hypothèse d'induction, m n _! = &jt'(Ao, Ai, A 2 , /{, / 2 ) , ce qui est en contradiction avec M(m) irréductible. On a donc mn = &k(AQ, Ai, A 2 , / 1 , / 2 ) . 47 48 ANNEXE A. PREUVES SUR LA SYNTAXE 2. Par induction sur n. Si n = 2, alors AT (m) = &fc(A0, Ai, A2, / i , / 2 ) o mx. D'après le lemme 3.7, A* ^ 0 . Si Ak G Obj(Co), alors mi G Arr(C0)(A, Afc). Sinon, A/t = push (A'0, A^, A2, /{, / 2 ) G Obj(C,-«i), et donc m i S ^ ^ M U i J Î J i ) € Arr(C,_i)(A,A*). Pas d'induction : Af(m) = &*(A0, Ai, A2, /1,/2) o m n . ! o • •. o mx G Arr(C,-)(A, B). D'après le lemme 3.7, A* ^ 0 . Si A^ G Obj(Co), alors d'après le théorème 3.2, m n _i o •. • o rai G Arr(C 0 )(A, A*) Si Afe = push (A'Q, A;, A'2, / ( , /J) G Obj(CVi), alors ran_! = &k,(A'0, A[, A'2, /{, /J) G Arr(C 1 _ 1 )(A^, A,) et, par hypothèse d'induction, ran_2 o . . . o rai G Obj(C î _ 2 )(A, A'k>), d'où ran_i o . . . o r a ! G Arr(C e _i)(A, Ak). A.2 Preuve du théorème de forme normale (3) Nous montrons le théorème 3.4, page 31. Théorème 3.4 (Forme normale (3)) Soit A = push (A0, A I , A2, / i , / 2 )GObj(C î ), BGObj(C 0 ) et m€Arr(C,-)(A, B). Posons M (m) = ran o ran_i o • • • o rai, avec n > 1 et V/ G { 1 , . . .rc}, m7 es£ une flèche élémentaire. Alors mi = up(A 0 ,Ai,A 2 ,A 3 ,/i,/ 2 ,5i,5f 2 ). A.3. PREUVE DU THÉORÈME Preuve. D'UUNICITÉ" 49 D'abord, on a • rai £ Arr(C0)(A, A') car A ¢ Obj(C 0 ). • rai ^ idx, sinon nécessairement, n > 2 et donc Af(m) n'est pas irréductible. • rai ^ j A - , car A^0. Par conséquent, on a soit rai = up(A 0 , Ai, A 2 , B , / i , / 2 , 0 i , 0 2 ) , soit ral = &^(AÎ ) ,A , 1 ,A , 2 ,/ 1 , ,/^). On montre par induction sur n que c'est la première condition qui est satisfaite. Si /i = l, alors comme B G Obj(Co), on a rai = up(A 0 , Ai, A2, B , / i , / 2 , 0 i , s r 2 ) . Pas d'induction : par l'absurde, si rai ¢: up (AQ, A I , A2, A3, / i , / 2 ,fin,g 2 ), alors mx^^K,^,^,/!,/^). Par hypothèse d'induction, m2 = up (A'0, A\,A'2, A'3, / [ , /^, g[, g'2), ce qui est en contradiction avec Af{m) irréductible. Par conséquent, ml = up (A0, AUA2, -43, /1,/2,51,02)D A.3 Preuve du théorème d'"unicité" de la forme normale Nous montrons le théorème 3.5, page 31. Théorème 3.5 ("Unicité" de la forme normale) Soit m, m' 6 Arr(C,)(À', Y), tels que m = m'e Arr(Ct)(A', Y). 1. SiX,YeObj(Co), alors AT (m) = M{m') € Arr(C0)(A-, Y). 50 ANNEXE A. PREUVES SUR LA 2. Si X £ Obj(Co), Y = push (A0, Ai, A2, / i , f2), VZ G Obj(Co), VA 6 Arr(C,)(V, Z), on a SYNTAXE alors M{h o m) = N{h o m') G Arr(C 0 )(X, Z). 3. Si X = push {A0, Ax, A2, A, f2),Y <= Obj(C 0 ). alors VW e Obj(Co), Vp € Arr(C,)(W, X), on a M{mop)=N{m'op)£AvT{C0){W,Y). 4. Si .Y = push (A0, ^ 1 , ^ 2 , / i , /2), V' = push (A'0, A'v A'2, f[, f2), alors VW, Z e Obj(Co), M e Arr(C,)(y, Z), Vp G Arr(C,)(W, .Y), on a Af(homop)=jV(hom'op)e Arr(C0) (W^, Z). Preuve. Nous montrons les points 1 à 4 par induction sur i. Pour i = 0, le point 1 est évident, et il n'y a rien à prouver pour les points 2 à 4. Pour i + 1, on prouve les points 2 et 4 par induction sur la longueur de Al'(h). Nous prouvons alors les points 1 à 4 en parallèle, par induction sur la longueur de la preuve que m = m'<= Arr(C t + i)(AW). Il faut considérer les règles (11) à (23). En réalité, nous avons besoin de l'hypothèse d'induction sur la longueur de ^V(/i) uniquement pour la règle (20). Dans tous les autres cas, il est inutile de prouver le cas de base, puis le pas d'induction. Les points 2 et 4 sont donc montrés directement, pour toutes les règles sauf la règle (20), et par induction sur la longueur de Af(h) pour la règle (20). Règle (11) m = m' € Arr(C 0 )(A\ Y). 1. D'après le théorème 3.1, on a m = AT(m)eArr(Co)(A:,y) m/ = ^ ( m ' ) G A r r ( C 0 ) ( A , F ) et donc M {m) = M {m') € Arr(C0)(A", Y). Il n'y a rien à démontrer pour les points 2 à 4. Règle (12) Les 4 points sont évidents. Règle (13) Les 4 points sont évidents, par symétrie de l'égalité dans CQ. Règle (14) Les 4 points sont évidents, par transitivité de l'égalité dans CQ. Règle (15) m = g o f, m' = g' o / ' , avec / = / ' G Arr(C !+ i)(A, B) et g = g' € Arr(C,+,)(fl,C). 1. A,C eObj{Co). • B 6 Obj(Co). Par hypothèse d'induction, on a JV(/)=W)€Arr(Co)04,fl) (*) A.3. PREUVE DU THEOREME D'UUNICITÉ" 51 Af(g)=M(g')eATT(C0)(B,C) (ii) Af(gof) = .\f(jV(g)oAr(f))eATv(C0)(A,C) = = = A/,(g)oAf(f)£An(C0)(A,C) AT (g') oAf(f') € Arr(C 0 )(A,C) M(rt(g')oAf(f')) G An(Co)(A,C) = W°/')€Arr(C0)M,C) (théorème 3.1) (d'après (i) et (ii)) (théorème 3.1) • B = push (A0, Ai, A2, /1,/2). Par hypothèse d'induction, on a : VZ G Obj(Co), V/i G Arr(C 1+ i)(C, Z), AT (h o / ) = AT (h o /') G An(CQ)(A, Z) (i) VW G Obj(Co), Vp G Arr(C,-+i)(W, A), jV(g o p) = A/*(s' o p) G Arr(C,-+i)(W, C) (ii) Par conséquent, A'(W) = .\f(gof')çArr(C0)(A,C) = X(g'of')€Arr(C0)(A,C) ((i), avec A = g) ((»), avec p = / ' ) • 6 = 0 : impossible d'après le lemme 3.7. 2. .4 G Obj(Co), C = push ( ^ , A'lt .4'2, f[, f2). VZ G Obj(Co), M G Arr(Ci+i)(C,Z), Il faut montrer que M (h 0 5 0 / ) = ,V(A o g' o / ' ) G Arr(C0)(-4, Z). • fi G Obj(Co). Par hypothèse d'induction, on a Mf)=^(f')eArt(C0)(A,B) (i) VZ G Obj(Co), V/i G Arr(C t + 1 )(C,Z), ,V(/i o j ) = ,V(/i o g') G Arr(C 0 )(B. Z) Par conséquent, JV(/»O0O/) = Af(Af(hog)ojV(f)) = M(hog)oM(f)€AïT(C0)(A,Z) = Af(hog') oAT(f') G An(C0)(A,Z) = N(M(hog')oM(f')) = jV(hog'of') (ii) (théorème 3.1) (d'après (i) et (M)) (théorème 3.1) • B = push (A 0 , /li, A 2 , /1,/2)- Par hypothèse d'induction, on a VZ G Obj(Co), VV G Arr(C,- + ,)(B, Z), ,V(fc' o / ) = M (h' o / ' ) G Arr(C0)(.4, Z) (i) VW, Z G Obj(Co), Vp' G Arr(C 1 + i)(^, 6 ) , V/» G Arr(C t+1 )(C, Z), A'(/i o 0 o p') = M (h og'o p') G Arr(C0)(H^, Z) (n) Par conséquent, :V(Ao 5 o/) = A^o^o/OGArr^oM^Z) = JV(hog'of')eATT(C0)(A,Z) ((i), avec V = ho g) ((n),avecp' = / ' ) 52 ANNEXE A. PREUVES SUR LA SYNTAXE • B = 0 : impossible d'après le lemme 3.7. 3. .4 = push (.40, .4i, A2, /1,/2), C G Obj(Co). On doit montrer que VW G Obj(Co), Vp G Art(Ci+i)(W, A), M(g o / o p) = AT (g1 o f o p) G An(C0)(W, C). • B G Obj(Co). Par hypothèse d'induction, on a VW G Obj(Co), Vp G Arr(C,+i)(W, A), Ar(fop)=Af(fop)eATt(Co)(W,B) et JV(<7) = A / V ) € Arr(Co)(^,C) Par conséquent, ,V'(5 o / o p) = N(M(g)oM(fop)) = Af(g)oAf(fop)çAn(Co)(W,C) = M(g') o jV(f o p) G Arr(C0)(W, C) = .VXV(<7') o ^(/ / o P))eArr(C 0 )(VF,C) = M(g'of'op) (i) (ii) (théorème 3.1) (cf. (i) et (ii)) (théorème 3.1) • B = push (.4(,, .4p /1 2 , f[, f2). Par hypothèse d'induction, on a VW\ Z G Obj(Co), Vp G ATT(Ci+i)(W, A), Vfc G Arr(C 1+ ,)(B, Z), ,V(fc o / o p) = AT(/i o / ' o p) G Arr(C0)(W, Z) (i) et VW G Obj(Co), Vp' G Arr(C,-+1)(W, B), A'(<7 o P') = W o P') € Arr(C0)(VV', C) (ii) Par conséquent, j\f(g o / o p) = = A % o / ' o p ) G A r r ( C o ) ( W , C ) ((i), avec A = (7) M (g' o f o p) G Arr(Co) (W, C) ( (ii), avec p' = / ' o p) • B = 0 . Il n'existe pas de flèche p£ Arr(C,-+i)(W, .4), sinon, on aurait une flèche /opGArr(C t + i)(W, 0 ) , avec WGObj(Co). Par conséquent, on a le résultat. 4. .4 = push (.4 0 ,.4i, A2,fuf2) doit montrer que et C = push (A0", Ai", A2", h", f2"). VW.ZÇ Obj(C 0 ), VpG Arr(Ci+i)(W,A), A/"(/i ogofop)= On V/i G Arr(C,+i )(C,Z), Af(h og'of'op)€ Arr(C0)(W, Z). • B G Obj(Co). Par hypothèse d'induction, on a VW G Obj(Co), Vp G Arr(C t+ i)(W, A), Af(f o p) = M(f o p) G Arr(C 0 )(^, B) VZ G Obj(Co), VA G Arr(C I+ i)(C, Z), Af (A o 5 ) = Af (A o g') G Arr(Co) (B, Z) (i) (ii) A.3. PREUVE DU THÉORÈME D,UUNICITÉ" 53 Par conséquent, Af(h o g o / o p) = N(N(hog)oN(fop)) = jV(hog)ojV(fop)eArT(C0)(W,Z) = Af(hog') oM(f'op) G Arr(C0)(W,Z) = Af(M(hog')oAf(fop)) = (théorème 3.1) (d'après (i) et (ii)) (théorème 3.1) N(hog'of'op) • B = push (A'0, A\, A'2, f[, f2). Par hypothèse d'induction, on a VW, Z G Obj(Co), Vp G Arr(C,+i)(^, A), VA' G Arr(C 1+ ,)(B, Z), Af(A' o / o p) = A/"(A' o / ' o p) G Arr(C0)(W, Z) (i) VW, Z G Obj(Co), Vp' G Arr(Ct+i)(W, B), VA G Arr(C,+i)(C, Z), A^(Ao«/op')=A^(Ao fi r'op')GArr(C 0 )(Vy,Z) (ii) Par conséquent, M (h ogo f op) = Ar(hogof'op)£ArT(Co)(W,Z) ((i), avec A' = A o g) = ;V(A o 5 ' o / ' o p) G Arr(Co)( W, Z) ((ii), avec p' = / ' o p) • B = 0 . Il n'existe pas de flèche p€Arr(d+i)(W, A), sinon, on aurait une flèche/opGArr(Ct+i)(VT, 0 ) , avec lyGObj(Co). Par conséquent, on a le résultat. Règle (16) m = (h o g) o / et m' = Ao (go f). 1. X((hog)of)=jV(ho(gof)). Les points 2 à 4 sont aussi évidents. Règle (17) m = / o id^ et m' = / , avec / G Arr(C,)(A, B). 1. On a Af(m)=Af(m'). 2. VZ G Obj(Co), VA G Arr(C,+i)(B, Z), A/"(Aom)=Af(Aom'). 3. VW G Obj(Co), Vp G Arr(C1+,)(W, A), M(mop) = Af(m' op). 4. VW, Z G Obj(Co), Vp G Arr(Ct-+i)(W, A), VA G Arr(C J+ i)(B, Z), M (h o m o p) = A/"(A om' op). Règle (18) Cas similaire au précédent. Règle (19) Il n'y a rien à démontrer. 54 ANNEXE A. PREUVES SUR LA SYNTAXE Règle (20) m = &i(A 0 , Ai, A 2 , / i , / 2 ) o fx et ra7 = & 2 (A 0 , Ai, A2, / i , / 2 ) o / 2 . 1. Il n'y a rien à démontrer. 2. A' = A0 G Obj(Co) et Y = push (A 0 , Ai, A 2 , / i , / 2 ) . Il faut montrer que VZ € Obj(Co), V/* G Arr(C l+1 )(y, Z), Af(/iora)=Af(/iora'). Induction sur la longueur de Af(h). Cas de base : Af(h) est de longueur 1. D'après le théorème 3.4, j\f(h) = up(A 0 , Ai,A 2 ,Z,/i,/ 2 ,flfi,5 2 ) Af(hom) = Af(up(AQ,...gi,g2)o8Li(AQ,...f2)ofl) j\f(homf) = = j\f(up(AQ<...gi,g2)o&2(A0,...f2)of2) Af(# 2 o/ 2 ) Or, on a ^ i o / i = gr 2 o/ 2 6 Arr(C t )(X, Z), donc par hypothèse d'induction sur i, A'(<7i o / i ) = Af(<72 ° /2) € Arr(C 0 )(X, Z). Par conséquent, .V(h om)= M(h o ra7) G Arr(C 0 )(A\ Z). Pas d'induction: on suppose le résultat démontré pour Af(h) de longueur n, et on le montre pour N(h) de longueur n + 1. D'après le théorème 3.4, Af(h) = h'oup (A0, A I , A 2 , A 3 , /1,/2,ffi,02). Af(/i o ra) = = 7 M (h o ra ) = = Âr(/i7 o up ( A 0 , . . .51 ^ 92) ° &i (A 0 , . . . / 2 ) 0 / 1 ) ^(h'og.oh) A r (/i / o up ( A 0 , . . -0i, 52) o &2(A0, . . - / 2 ) 0 /2) N(h'og2of2) Or, on a 51 o /1 = 0 2 o / 2 G Arr(C,)(AT, K), et /i7 est une forme normale de longueur n, donc par hypothèse d'induction sur n, M(h'ogi o /1) = M(ti og2 o f2) G Arr(C 0 )(X, Z). Par conséquent, Af(h o ra) = Af(A o ra7) G Arr(C0)(-Y, Z). 3. Il n'y a rien à démontrer. A.3. PREUVE DU THÉORÈME D,UUNICITÉ" 55 4. A' = .40 SE push (A'0, A\, A'2, f[, f2) et Y = push (A0, Ai, A2, h, f2). Il faut montrer que VW, Z G Obj(Co), Vp G Arr(Ci+l)(W, X), VA G Arr(C t+ ,)(F, Z), A'(hom op) = Af(ho m' op). Remarquons d'abord que X G Obj(C,), donc d'après le théorème 3.3-2, Af(p) G Arr(C,)(W, .Y). Cas de base sur la longueur de Af(h) : N(A) = up (A0, AUA2, Z, /1, / 2 , gi,g2). = Ar(up(A0,...gl,g2)oSil(Ao,...f2)of1op) = tf(giofioAr(p)) jV(hom'op) = Af(up(A0,...gi,g2)o8i2(A0,...f2)of2op) = A r (52o/ 2 oA/'(p)) A'(p) G Arr(C,), 51 ° /1 = 02 o / 2 G Arr(C,)(A,Z), donc par hypothèse d'induction sur i, on a Af(homop) M(gi o h oAf(p)) = Af(g2 o f2 oAf(p)) G Arr(Co)(W, Z) d'où Af(A o m o p) = AT (h o m'o p) G ATT(C0)(W, Z). Pas d'induction : on suppose le résultat démontré pour .V(A) de longueur n, et on le montre pour Af(h) de longueur n + 1. j\f(h) = N(homop) Af(hom'op) = = = = h'oup(A0,Ai,A2,A3,fi,f2,gi,g2) AA(A'oup(ylo,--.5i,ff2)o&i(-4o,---/2)o/iop) M(h' ogiofxop) A/"(A'oup (^0,.--171,52) 0 ^ 2 ( ^ 0 , - - - / 2 ) 0 / 2 op) M (h' o g2 o / 2 o p) On a j i o / ] = g2 o / 2 G Arr(C,)(A, Z), A' est une forme normale de longueur n, donc par hypothèse d'induction sur n, on a N(h' o gx o fi o p) = A/"(A' og2o f2op), d'où AT (A o m o p) = Af (A o m'o p) G Arr(C0)(W, Z). Règle (21) m = up(A,B,C,D,f,g,f',g')oki(A,B,C,f,g),m' 1. On a N(m)=N(m'). = f'. 56 ANNEXE A. PREUVES SUR LA 2. VZ G Obj(Co), VA G Arv(Ci+1)(B, Z), Af(hom) = 3. VW G Obj(Co), Vp G An(Ci+i)(W, SYNTAXE Af(hom'). A), Af(m o p) = M (m' o p). 4. \/W, Z G Obj(Co), Vp G Arr(C t+1 )(W, A), VA G Arr(C )+ i)(fl, Z), Af( h o m o p) = A/*( A o m' o p). /ïèg/e (22) Cas similaire au cas précédent. Règle (23) m = m' parce que mobl(A0,Al,A2,f1,f2) m o & 2 (.4 0 , Ai, A2, fi,f2) = Tn'oài1(A0,Ai,A2,fi,f2)€Air(Ci+l)(Ai,Y), = m'o & 2 (,4 0 , .4,, A2, / , , / 2 ) G Arr(C 1+1 )(,4 2 , F ) . 1. Il n'y a rien à démontrer. 2. Il n'y a rien à démontrer. 3. A' = push (.40, -4i, .4 2 , /1,/2) et Y G Obj(C 0 ). Il faut montrer que VW G Obj(Co), \/peAvr(Ct+i)(W,X), AT (m o p) = M (m'o p) G Arr(C0)(W, Y). Soit Af(p) = pn°Pn-i o • • -opi, avec n > 1. D'après le théorème 3.3, p„ = &k(A0, Ai,A2,fi,f2). Si n = 1, on a par hypothèse d'induction j\f(m o iik(A0, Au A2, /1,/2)) = AT (m! o bk(A0, Ai, A2, / 1 , f2)) G An(C0)(W, Y) d'où A/"(mop) = Af(m'op) G Arr(C0)(Vy,Y). Si n > 2, on a par hypothèse d'induction M (m o &.k(A0, Ai, A2, fx, f2) o p n _j o • • • o pj) = Ar(m'o&fc(Ao,Ai,A2,/i,/2)opn_io...op1)GArr(Co)(^,Y) d'où Af(jnop) = ATfm'op) G Arr(C0)(W, V')- A.4. PREUVE DU THEOREME 3.9 57 4. X = push (AQ, A I , A 2 , / i , / 2 ) et Y = push (AQ, A 7 P A ^ / J , / 7 , ) . Il faut montrer que VVy,ZGObj(Co),VpGArr(^ + i)(V^,X),V/iGArr(C î + i)(y,Z), Af(h omop) = AT (h o ra7 o p) G Arr(C0)(W, Z). Soit Af(p) = pn ° P n - i o • • -opi, avec n > 1. D'après le théorème 3.3, p n = &jk(A 0 , A i , A 2 , / i , / 2 ) . Si n = 1, on a par hypothèse d'induction j\f(h o ra o 8ik(A0, Ai, A2, / i , / 2 )) = -V(/iora7o&,(A0,Ai,A2,/i,/2))GArr(C0)(^,Z) d'où AT (h o ra op) = AT(/i o ra7 op) G Arr(C0)(W, Z). Si n > 2, on a par hypothèse d'induction Af(h o ra o &k(AQ, Ai, A2, /1,/2) o Pn-i o • • • o pi) = Af(h o ra7 o &ib(Ao, Ai, A 2 , / 1 , / 2 ) o p n _i o .. - o pi) G ATT(C0)(W,Z) d'où AT (h o ra o p) = Af(h A.4 o ra7 o p) G AVÏ(CQ)(W, Z). Preuve du théorème 3.9 Nous montrons le théorème 3.9 page 36. Théorème 3.9 (La précatégorie TERME(Co) est librement engendrée par objet préinitial choisi et pré-sommes amalgamées choisies) Considérons une précatégorie £ ayant un objet pré-initial choisi 0 et des présommes amalgamées choisies. Si A, B, C sont trois objets de £, et / G Arr(£)(A, B), g G Arr(£)(A,C) deux flèches de £, on note (push£(A,B,C,f,g), & f ( A , f l , C , / , 5 ) , &f (A, B, C,f,g)) la pré-somme amalgamée choisie de B et C par rapport à f et g dans S. On suppose de plus que, pour tout objet A de £, on a un choix de flèche j£A£Arv(E)(0£,A). De même, si A,B,C,De Obj(£), / G An(€)(A, B), g G Arr(£)(A,C), / ' G Atx(S)(B, D), g'eArr(€)(C, D), tel que / ' o / = g' og G An(£)(A, D), on a un choix de flèche up£(A, B, C, D, f,g, /',g') G An(£)(push£(A, B, C,f, g), D) 58 ANNEXE A. PREUVES SUR LA SYNTAXE telle que up£(A,B,C,D,f,g,f',g')ok£(A,B,C,f,g) up£(A,B,C,D,f,g,f',g')ok£(A,B,C,f,g) = = f'eArr(£)(B,D) g'eArr(£)(C,D). Soit un préfoncteur F : CQ —» €. Alors il existe un unique préfoncteur G : TERME(Co) -> S tel que Go.J = F; G(gof) = G(g)oG(f); G(\dA) = idG(A) ; G(0) = 0£ ; G (ÏA) = JG(A) ' G(push (A, B, C, f,g)) = push£ (G(A), G(B), G(C), G(f), G (g)) ; G(bi(A,B,C,f,g)) = k£(G(A),G(B),G(C),G(f),G(g)); G(b2(A,B,C,f,g)) = k£(G(A),G(B),G(C),G(f),G(g)); G(op(A,B.C,D,f,g,f',g') = uP£(G(A),G(B),G(C),G(D),G(f),G(g),G(f),G(g')). Nous commençons par montrer l'existence du préfoncteur G : TERME(Co) - • £. Pour cela, nous définissons pour tout entier i un préfoncteur G; : Ci -> £, par induction sur i. Nous posons Go = F, et définissons le préfoncteur G,-+i : C,-+i -» £ à partir du préfoncteur G{ : d —> £. Hypothèses d'induction Pour i G IN, on fait les hypothèses d'induction suivantes. 1. Si i > 1, (a) VAeObj(C,-_i), Gî(A) = Gî.l(A); (b) VA,fleObj(C t -_i), V / G A r r ( C ^ i ) ( A , B ) , Gt(f) =Gt^(f) 2. h = h'£Arr(Cî)(A,B) =» Gx(h) = G%(ti) G An(£)(Gî(A),Gl(B)) ; ; 3. Gi : Ci —> £ est un préfoncteur. Pour i = 0, on pose GQ = F :CQ —¥ £. Les hypothèses d'induction sont bien vérifiées. Nous définissons maintenant le préfoncteur G;+i : Ci+\ —»• £, en supposant que les hypothèses d'induction sont satisfaites au rang i. A.4. PREUVE DU THEOREME 3.9 59 Définition du préfoncteur G,+i : C,+i —• S Le préfoncteur G,+i est défini à partir de G,, par induction sur la structure des objets et des flèches de C,+i. • Action sur les objets : Règle (1) Gi+Ï(A) = G0(A), pour A G Obj(C0) ; Règle (2) Gi+i(0) = 0£; Règle (3) G t+ i(push (.4, B,C,f,g)) = push£(Gi(A), G,(B), Gi(C), d(f), G,(g)). • Action sur les flèches: Règle (4) Gt+i(f) = G 0 (/), pour / G An(C0)(A, B) ; Règle (5) G,+i (gof) = Gi+i (g) o Gi+Ï (f) ; Règle (6) G t + i(id^) = idGt+1(A), identité de £ ; Règle (7) G,+i(j. 4 ) = Ja,+l(A) ? Règle (S) Gi+i(8n(A,B,C, f,g)) = &f (Gi(A),G,(B),Gi(C),Gi(f),Gi(g)); £ Règle (9) G I + ,(& 2 04,#,C,/,i : Cj+i -> £ est un préfoncteur. Preuve. PomJ 7. On montre le point 1 (a) par induction sur la structure des objets de C,+i, le point 1 (b) par induction sur la structure des flèches de C,-+i. 60 ANNEXE A. PREUVES SUR LA SYNTAXE Point 2. On montre le point 2 par induction sur la longueur de la preuve que h= h'€Arr(Ct+l)(A,B). Règle (11) Si h = h' G Arr(C0)(A, B), alors G0(h) = G0(h'), et donc, par définition de G 1+ i, Gi+i(h) =G 1 + i(/i'). Règle (12) Si h = h', alors on a évidemment G{+i(h) = G,+i (/&'), d'où le résultat. Règle (13) Si h' = /i G Arr(C,+i)(/l, B), alors par hypothèse d'induction, Gi+i(h') = Gt+i(h),d'oùGi+i(h)=Gi+i(h'). Règle (14) Si h = g G Arr(C î+ i)(/l, £ ) et g = h' € Arr(Ci+i)(A, B), alors, par hypothèse d'induction, on a G,+i(/i) = G,+i(<7) et G,+i( 5 est bien un préfoncteur. D Nous avons donc montré le résultat suivant. Lemme A . l Pour tout entier i, 1. (a) Vi4 G Obj(C,-). Gi+i(A) = G,(A) ; (b) VA, fî G Obj(C,-). V/ G Arr(C,-)M, B), G,+i(/) = £ par son action sur les objets et les flèches de TERME(C 0 ). • Action sur les objets. Pour tout .4 G Obj(TERME(C 0 )), il existe k G N tel que A G Obj(Ck). On pose G(A) = Gk(A). D'après le lemme A.l (a), cette définition est indépendante de l'entier k choisi. • Action sur les flèches. Pour tout / G Arr(TERME(C 0 )), il existe A; G N tel que / € Arr(Ck)(A, B). On pose G(f) = Gk(f). D'après le lemme A.l (b), cette définition est indépendante de l'entier k choisi. • Compatibilité avec les équivalences. Si h = h' G Arr(TERME(C 0 ))(.4,£), alors il existe A; G IN tel que h = h' G Arr(Cfc)(-4, B). Comme Gk est un préfoncteur, Gk(h) = Gk(h'). Par conséquent. G (h) = G(h'). On vérifie que G est bien un préfoncteur tel que • G o./ = F ; • G(gof) = G(g)oG(f); • G(idA) = idG{A); • G ( 0 ) = 0£ ; • GfjA) = j £ G ( A ) ; • G(pusb(A,B,C,f,g)) = puSh£(G(A),G(B),G(C),G(f),G(g)); • G(Li(A,B.C,f,g)) = k£(G(A),G(B),G(C),G(f),G(g)); • G(L2(A,B,C,f,g)) = k£2(G(A),G(B),G(C),G(f),G(g)); • G(up(A,B,C,D,f,g,f',g') = up£(G(A),G(B),G(C),G(D),G(f),G(g),G(f'),G(g')). Unicité du préfoncteur G Soit un préfoncteur G' : TERME(Co) -> £ tel que • G'oJ = F; • G'(gof)=G'(g)oG'(f); A.4. PREUVE DU THEOREME 3.9 63 G'(\dA) = idG,(A) ; • G'(0) = 0£ : • G'(iA) = iG,(A) ; • G'(push (.4, B,C, f,g)) = push£(G'(A),G'(B),G'(C),G'(f),G'(g)) • G'(ki(A,B,C,f,g)) = k£(G'(A),G'(B),G'(C),G'(f),G'(g)); • G'(k2(A,B,C.f,g)) = k£(G'(A),G'(B),G'(C),Gy),G'(g)); • ; G'(up(A,B,C,D,f,g,f',g') = up£(G'(A),G'(B),G'(C),G'(D),G'(f),G'(g),G'(f'),G'(g')). Par induction sur la structure des objets etflèchesde TERME(CQ), on a bien G = G7. Références bibliographiques [AL91] A. Asperti and G. Longo. Catégories, Types and Structures, An Introduction to Category Theory for the Working Computer Scientist. Foundations of Computing Science, MIT Press, 1991. [AM75] M. A. Arbib and E. G. Mânes. Arrows, Structures and Functors: The Categorical Imperative. Académie Press, 1975. [B+90] D. Bert et al. Référence manual of the spécification language LPG. Technical Report 59, LIFIA, Mars 1990. Anonymous ftp at imag.fr, in /pub/SC0P/LPG/NewSun4/man_lpg.dvi. [BBCH6] G. Bernot, M. Bidoit, and C. Choppy. Abstract data types with exception handling: An initial approach based on a distinction between exception and errors. Theoretical Computer Science, 46(1):13-45, 1986. [BDMN73] G. Birtwistle, O.-J. Dahl, B. Myrhaug, and K. Nygaard. Simula Begin. Auerbach Pub., New York, 1973. [BE86] D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proceedings of ESOP'86, number 213 in LNCS, pages 119-132. Springer-Verlag, 1986. [Ber83] D. Bert. Refinements of generic spécifications with algebraic tools. In Proceedings of IFIP'83, Paris, pages 815-820, 1983. [Ber90] D. Bert. Spécification de logiciels réutilisables. Technical Report RR828-I-IMAG-116, LIFIA, Octobre 1990. [BG77] R. M. Burstall and J. A. Goguen. Putting théories together to make spécifications. In Proceedings of the 5th International Joint Conférence on Artificial Intelligence, pages 1045-1058, 1977. [BG80] R. M. Burstall and J. A. Goguen. The semantics of CLEAR, a spécification language. In Proceedings of Advanced Course on Abstract Software Spécification, number 86 in LNCS, pages 292-332. SpringerVerlag, 1980. [BHK90] J. A. Bergstra, J. Heering, and R. Klint. Module algebra. J. ACM, 37(2):335-372, Apr. 1990. 65 66 REFERENCES BIBLIOGRAPHIQUES [Bid89] M. Bidoit. PLUSS, un langage pour le développement de spécifications algébriques modulaires, Mai 1989. Thèse d'Etat, Université de ParisSud. [BL93] G. Bernot and P. Le Gall. Exception handling and term labelling. In Proceedings of TAPSOFT93, number 668 in LNCS, pages 421-436. Springer-Verlag, 1993. [BR86] R. M. Burstall and D. Rydeheard. Computing with catégories. Technical Report ECS-LFCS-86-9, University of Edinburgh, September 1986. [Bur80] R. M. Burstall. Electronic category theory. In Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, 1980. [BVV85] S. L. Bloom and E. G. Wagner. Many-sorted théories and their algebras with some applications to data types. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 4, pages 133-168. Cambridge University Press, 1985. [BW90] M. Barr and C. Wells. Category Theory for Computing Prentice-Hall International, 1990. [BW94] M. Barr and C. Wells. The categorical theory generated by a limit sketch, Nov. 1994. [Car86] J. Cartmell. Generalized algebraic théories and contextual catégories. Annals of Pure and Applied Logic, 32:209-243, 1986. [Coh65] P. M. Cohn. Universal Algebra. Harper and Row, 1965. Revised version 1980. [Cur91] F. Cury. Catégories lax-localement-cartésiennes et catégories localement cartésiennes: un exemple de suffisante complétude connexe de sémantiques initiales. In diagrammes, volume 25, pages 1-155, Université Paris 7, Juillet 1991. [DJ90] N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In Handbook of Theoretical Computer Science, chapter 15. Elsevier Science Publishers B.V., 1990. [DN66] O.-J. Dahl and K. Nygaard. Simula - an Algol-based simulation language. Communications of the ACM, 9:671-678, Sept. 1966. [DR94a] D. Duval and J.-C. Reynaud. Sketches and computation (part 1): Basic définitions and static évaluation. Mathematical Structures in Computer Science, 4:185-238, 1994. [DR94b] D. Duval and J.-C. Reynaud. Sketches and computation (part 2): Dynamic évaluation and applications. Mathematical Structures in Computer Science, 4:239-271, 1994. Science. REFERENCES BIBLIOGRAPHIQ UES 67 [Ehr65] C. Ehresmann. Catégories et structures. Dunod, Paris, 1965. [Ehr68] C. Ehresmann. Esquisses et types de structures algébriques. Bulletin de llnstitut Polytechnique, Iasi 14, 1968. [EJ093] H. Ehrig, R. M. Jimenez, and F. Orejas. Compositionality results for différent types of parameterization and parameter passing in spécification languages. In Proceedings of the 4th International Joint Conférence CAAP/FASE, number 668 in LNCS, pages 31-45. Springer-Verlag, 1993. [EM85] H. Ehrig and B. Mahr. Fundamentals of Algebraic Spécification 1. Equations and Initial Semantics, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985. [EM90] H. Ehrig and B. Mahr. Fundamentals of Algebraic Spécification 2. Module Spécifications and Constraints, volume 21 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1990. [FGJM85] K. Futatsugi, J. A. Goguen, J.-P. Jouannaud, and J. Meseguer. Principes of OBJ2. In Proceedings of Principles of Programming Languages, pages 52-66, 1985. [Gau84] M.-C. Gaudel. A first introduction to PLUSS. Technical report, Université d'Orsay, France, 1984. [GB84] J. A. Goguen and R. M. Burstall. Introducing institutions. In Proceedings of the Workshop on Logic of Programming, number 164 in LNCS, pages 221-256. Springer-Verlag, 1984. [GB90] J. A. Goguen and R. M. Burstall. Institutions: Abstract model theory for spécification and programming. Research Report ECS-LFCS-90106, University of Edinburgh, January 1990. [GKK+87] J. A. Goguen, C. Kirchner, H. Kirchner, A. Mégrelis, J. Meseguer, and T. Winkler. An introduction to OBJ3. In Proceedings of the lst International Workshop on Conditional Term Rewriting Systems, number 308 in LNCS, pages 258-263. Springer-Verlag, 1987. [Gog73] J. A. Goguen. Categorical foundations for gênerai Systems theory. In Advances in Cybernetics and System Research, pages 121-130. Transcripta Books, 1973. [Gog92] J. A. Goguen. Sheaf semantics for concurrent interacting objects. Mathematical Structures in Computer Science, 2:159-191, 1992. [Gol79] R. Goldblatt. Topoi: The Categorial Analysis of Logic, volume 98 of Studies in Logic and the Foundations of Mathematics. North Holland, 1979. 68 [GTW78] REFERENCES BIBLIOGRAPHIQUES J. A. Goguen, J. W. Thatcher, and E. G. Wagner. An initial algebra approach to the spécification, correctness, and implementation of abstract data types. In R. T. Yeh, editor, Current Trends in Programming Methodology, volume 4: Data Structuring, pages 80-149. Prentice-Hall, 1978. [GTWW75] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Abstract data types as initial algebras and the correctness of data représentation. In Computer Graphics, Pattern Récognition and Data Structure, pages 89-93, 1975. [GTWW77] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebra. J. ACM, 24:68-95, 1977. [Gut75] J. V. Guttag. The spécification and application to programming of abstract data types. PhD thesis, University of Toronto, 1975. [Gut77] J. V. Guttag. Abstract data types and the development of data structures. Communication of the ACM, 6:396-404, 1977. [Huf92] J.-M. Hufflen. Proposai for GLIDER version 1.0: Principles and main features. ICARUS Technical Report, INRIA-LORRAINE & CRIN, 1992. [Law63] W. Lawvere. Functorial semantics of algebraic théories. Proc. Nat. Acad. Sel, 50:869-873, 1963. [LCW85] D. Lorge Parnas, P. C. Cléments, and D. M. Weiss. The modular structure of complex Systems. IEEE Transactions on Software Engineering, SE-11(3) :259-266, March 1985. [LS86] J. Lambek and P. J. Scott. Introduction to higher order categorical logic. Cambridge studies in advanced mathematics, 1986. [LZ74] B. Liskov and S. Zilles. Programming with abstract data types. ACM SIGPLAN Notices, 9(4):50-59, 1974. [Mar95] A. Martins. La généralisation: un outil pour la réutilisation. thesis, INPG, Grenoble, Mars 1995. [MB70] S. Mac Lane and G. Birkhoff. Algèbre. 1. Structures Gauthier-Villars, 1970. [McL71] S. Mac Lane. Catégories for the Working Mathematician. Verlag, 1971. [MG85] J. Meseguer and J. A. Goguen. Initiality, induction, and computability. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 14, pages 459-541. Cambridge University Press, 1985. PhD fondamentales. Springer- REFERENCES BIBLIOGRAPHIQUES 69 [Ori94] C. Oriat. Representing modular spécifications as diagrams. In Compte Rendu des Journées du GDR Programmation, Lille, pages 53-68, Septembre 1994. [Ori95] C. Oriat. Detecting isomorphisms of modular spécifications with diagrams. In Proceedings of AMAST'95, number 936 in LNCS, pages 184-198. Springer-Verlag, 1995. [Poi92] A. Poigne. Basic category theory. In Handbook of Logic in Computer Science, Volume 1. Background: Mathematical Structures, pages 413640. Oxford Science Publication, 1992. [Ren91] G. Renardel de Lavalette. Logical semantics of modularisation. In Proceedings of CSL *91, number 626 in LNCS, pages 306-315. SpringerVerlag, 1991. [Rey90a] J.-C. Reynaud. Putting algebraic components together: A dépendent type approach. Research Report 810 I IMAG, LIFIA, Avril 1990. Extended version. [Rey90b] J.-C. Reynaud. Putting algebraic components together: A dépendent type approach. In Proceedings of DISCO'90, number 429 in LNCS. Springer-Verlag, 1990. [Rey93] J.-C. Reynaud. Isomorphism of typed algebraic spécifications. Internai Report, LGI-IMAG, Avril 1993. [See84] R. A. G. Seely. Locally cartesian closed catégories and type theory. Math. Proc. Camb. Phil. Soc., 95(33):33-48, 1984. [SP77] M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain équations. In Proceedings of the I8th IEEE Symposium on Foundations of Computer Science, pages 13-17, 1977. [SST92] D. Sannella, S. Sokolowski, and A. Tarlecki. Toward formai development of programs from algebraic spécifications: Parameterisation revisited. Acta Informatica, 29:689-736, 1992. [ST88] D. Sannella and A. Tarlecki. Spécifications in an arbitrary institution. Information and Computation, 76:165-210, 1988. [SW83] D. Sannella and M. Wirsing. A kernal language for algebraic spécification and implementation. In Proceedings of the llth Colloquium on Foundations of Computation Theory, number 158 in LNCS, pages 413-427. Springer-Verlag, 1983. [SW91] T. Streicher and M. Wirsing. Dépendent types considered necessary for spécification languages. In Proceedings of the 7th Workshop on Spécification of Abstract Data Types, number 534 in LNCS, pages 323339, 1991. 70 REFERENCES BIBLIOGRAPHIQUES [TBG91] A. Tarlecki, R. M. Burstall, and J. A. Goguen. Some fundamental algebraic tools for the semantics of computation: Part 3. Indexed catégories. Theoretical Computer Science, 91:239-264, 1991. [TWW82] J. W. Thatcher, E. G. Wagner, and J. B. Wright. Data type spécification: Parameterization and the power of spécification techniques. ACM Trans. Prog. Lang. Syst., 4:711-773, 1982. [Wan79] M. Wand. Fixed-point constructions in order-enriched catégories. Theoretical Computer Science, 8:13-30, 1979. [WBT85] E. G. Wagner, S. L. Bloom, and J. W. Thatcher. Why algebraic théories? In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 17, pages 607-634. Cambridge University Press, 1985. [Wir86] M. Wirsing. Structured algebraic spécifications: A kernel language. Theoretical Computer Science, 42:123-249, 1986. [Wir90] M. Wirsing. Algebraic spécification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 13, pages 677-788. Elsevier Science Publishers B.V., 1990. [Wir94] M. Wirsing. Algebraic spécification languages: An overview. In Récent Trends in Data Type Spécification, 10th Workshop on Spécification of Abstract Data Types, number 906 in LNCS, 1994. Table de la deuxième partie Introduction 1 Spécifications algébriques 2 Théorie des catégories 3 Modularité 4 Notre travail 5 Comparaisons avec d'autres travaux 6 Plan de ce mémoire 5 5 6 7 8 10 12 3 Syntaxe : catégorie des termes 3.1 Précatégories, préfoncteurs et pré-colimites 3.2 Problème de circularité termes - congruences 3.3 Précatégories C; 3.4 Simplification des flèches 3.5 Extensions conservatrices 3.6 Précatégorie TERME(Co) 3.7 Catégorie Terme(Co) 3.8 Catégorie libre C(C0) 3.9 Conclusion 13 15 20 21 26 32 33 37 38 45 A Preuves sur la syntaxe A.l Preuve du théorème de forme normale (2) A.2 Preuve du théorème de forme normale (3) A.3 Preuve du théorème d'"unicité" de la forme normale A.4 Preuve du théorème 3.9 47 47 48 49 57 Références bibliographiques 65 Laboratoire LSR (Logiciels, Systèmes, Réseaux) Institut IMAG (Institut d'Informatique et de Mathématiques Appliquées de Grenoble) 681, rue de la Passerelle B.P. 72 38402 Saint Martin d'Hères Cedex 71