D IAGRAMMES C. O RIAT Étude des spécifications modulaires : constructions de colimites finies, diagrammes, isomorphismes. Partie III Diagrammes, tome 41 (1999), p. 3-76 © Université Paris 7, UER math., 1999, 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 41,1999 ETUDE DES SPECIFICATIONS MODULAIRES CONSTRUCTIONS DE COLIMITES FINIES, DIAGRAMMES, ISOMORPHISMES (*> PARTIE III (**> 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 finiment 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 ( ** 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 II dans Diagrammes 40. gather two spécifications sharing a common part. Our work extends this classic idea along three Unes. From a syntactic point of view, 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: Vobjet 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 abstrait 2 ".) 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 anglais, 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 l'anneau 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 construction3 comme le renommage, 3. En anglais, spécification-building opérations. INTRODUCTION Venrichissement ou Vabstraction [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 Vinstanciation 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 Co 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(Co), 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(Cn) et diagr(Co). Les objets de DIAGR(Cn) sont des diagrammes, et les flèches de DIAGR(Cn) des morphismes de diagrammes. La catégorie diagr(Cn) est obtenue à partir de DIAGR(Cn) par un quotient par une relation de congruence sur les flèches de DIAGR(Co). C'est la catégorie diagr(Cn) 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(Cn). D'autre part, diagr(Co) est une complétion par colimites finies de la catégorie CQ. 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(Cn). 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(Cn). Nous montrons que ce foncteur définit une équivalence de catégories entre Terme(Cn) et diagr(Cn), 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 Animent 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. S y n t a x e 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(Co), 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(Co). 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(Co), 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,_i. 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(Cn) 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(Co) 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 les deux premières parties, comprenant les chapitres 1, 2 et 3, nous avons présenté le cadre général de notre travail (les spécifications modulaires), les bases théoriques (les catégories de diagrammes) et la syntaxe des spécifications modulaires. Ce volume contient la troisième partie de notre thèse, c'est-à-dire les chapitres 4 et 5, consacrés respectivement à la traduction des spécifications modulaires en diagrammes et à la détection d'isomorphismes entre diagrammes. Dans le chapitre 4, nous interprétons les termes dénotant des spécifications modulaires par des diagrammes. Cette interprétation permet d'obtenir une représentation plus abstraite des spécifications modulaires que celle donnée par les termes, parce que certaines étapes spécifiques de la construction sont éliminées. Nous montrons que l'interprétation des termes par les diagrammes définit une équivalence entre les catégories Terme(Co) et diagr(Co). Ce résultat nous permet de déduire que toute spécification modulaire est isomorphe à la colimite du diagramme qui la représente. Le chapitre 5 est une application de cette représentation des spécifications modulaires par des diagrammes. Nous proposons de détecter un isomorphisme de construction entre deux spécifications modulaires en détectant un isomorphisme entre leurs diagrammes correspondants. Nous présentons un algorithme qui permet, dans l'hypothèse où la catégorie de base CQ est finie et ne comporte pas de cycle, de détecter si deux diagrammes sont isomorphes. Chapitre 4 Sémantique : des termes aux diagrammes Le but de ce chapitre est d'associer à toute spécification modulaire un diagramme, et à tout morphisme de spécifications modulaires un morphisme de diagrammes. On appelle CQ la catégorie des spécifications et morphismes de spécifications de base, et on décrit cette association par un préfoncteur V : TERME(Co) -> DIAGR(C 0 ). Intuitivement, étant donné un objet A de TERME(C 0 ) qui représente une spécification modulaire, V(A) est un diagramme dont la colimite est isomorphe à cette spécification. Le foncteur V décrit une interprétation des termes par des diagrammes, il s'agit donc d'une sémantique pour les spécifications algébriques modulaires, par opposition aux termes qui constituent la syntaxe. Après avoir défini le préfoncteur V : TERME(C 0 ) - • DIAGR(C 0 ), nous détaillons les calculs de diagrammes associés aux spécifications modulaires A2, A'2, A3 et A4 des anneaux présentées dans le chapitre 1 (partie I). Dans la dernière partie, nous montrons que les précatégories TERME(C 0 ) et DIAGR(Cn) sont équivalentes, ce qui implique par passage au quotient que les catégories associées Terme(C0) et diagr(Co) sont équivalentes. Intuitivement, cela signifie que ces deux catégories ont "la même structure", "aux isomorphismes entre objets près". Nous en déduisons que deux objets de Terme(C0) sont isomorphes si et seulement si leurs diagrammes associés sont isomorphes dans la catégorie diagr(Cn). Enfin, nous montrons que le calcul de diagrammes est correct, c'est-à-dire qu'une spécification est isomorphe à la colimite du diagramme qui la représente. 4.1 Sémantique 4.1.1 P r é c a t é g o r i e DIAGR(C 0 ) Dans tout ce chapitre, Cn est une petite catégorie. Rappelons que la catégorie DIAGR(Cn) peut être considérée comme une précatégorie de la façon suivante (cf. 13 14 CHAPITRE 4. SEMANTIQUE : DES TERMES AUX DIAGRAMMES chapitre 3, partie II, page 19) : • l'identité syntaxique dans la précatégorie DIAGR(Co) est l'égalité dans la catégorie DIAGR(Co) ; • l'équivalence dans la précatégorie DIAGR(Co) est définie par la congruence « sur les flèches de la catégorie DIAGR(Co). Par conséquent, la catégorie associée à la précatégorie DIAGR(Co) est diagr(Cn). La précatégorie DIAGR(Co) est finiment pré-cocomplète. Plus précisément, la précatégorie DIAGR(Cn) a un objet pré-initial choisi et des pré-sommes amalgamées choisies. Objet pré-initial Rappelons que le diagramme vide, noté O , est le diagramme dont le graphe sousjacent ne contient aucun nœud et aucun arc. L e m m e 4.1 Le diagramme vide est pré-initial dans la précatégorie DIAGR(Cn). Autrement dit, 1. pour tout diagramme a de DIAGR(Co), H existe une flèche 7Ô : O -> ô dans DIAGR(Co) ; 2. pour toute flèche 7r : Ç) —ta, on a Jâ~&- Remarquons qu'en réalité le diagramme vide est initial dans DIAGR(Co). En effet, pour toute flèche a : O -> â, on a j ^ = a. Pré-sommes a m a l g a m é e s Soit trois diagrammes a, fi et 7, et deux morphismes de diagrammes a : a —» (3 et r : Q —> 7 de DIAGR(Cn)- On considère le diagramme de somme amalgamée ïï= (n*, n : n* -> DIAGR(C0)) où 11(0) = 3 ; 11(1) = 0; n(2) = f; ïl(a) = â; n(6) = T. 4.1. 15 SEMANTIQUE Ce diagramme sera noté Il = VushT>iagr(â, fi, 7, a, r). Le diagramme II est un objet de DIAGR2(Cn), construit sur le graphe II*. (r • -•- 1 a 0 -*-• b 2 graphe U^ %, diagramme II = VushViagr[pt, fi, 7, a, r) En aplatissant le diagramme II, on obtient un diagramme 6 de DIAGR(Co) (cf. définition 2.29, partie I, page 84) : * = Apl Co (II). On a également deux flèches J\ : fi —> 6 et J 2 : 7 définition 2.30, partie I, page 85) qui seront notées 6 dans DIAGR(C0) (cf. J± = Ji[â, fi,7, cr,T) : fi -+ ~6 J2 = J 2 ( â , / 3 , 7 , â , r ) :î->6. L e m m e 4.2 Le triplet (AplCo (VushTHagr (â, /3, 7, â, r)), Ji"(â, /3,7, â, r), J 2 (â, /3,7, â, r)) est une pré-somme amalgamée de fi et 7 par rapport aux flèches W et T. Cela signifie qu'on a les propriétés suivantes. 1. J[(Q, / 3 , 7 , â , r ) o â « J 2 (â,/3,7,â, r) o r . 2. SoiJ arc diagramme 6' et deux flèches 7^:/3-^ A"2 : 7 - • £' de DIAGR(Co) telles que / \ 1 o cr % A' 2 ° 7\ Alors. (a) en posant 6 = Ap\Co (VushTHagr(a, fi, 7, a, r ) , i/ existe une flèche Û(â, p, ^,0,7,1^,7^):6^61 de DIAGR(Co) telle que U[a,/3,7,#,^,r,Ki,K2) o Ji(a,/3,7,a,r) « Kj_ U{â, /3,7, £', â, r, K\, K2) o J 2 ( â , /3, 7,â, r) « /f2 ; 16 CHAPITRE 4. SÉMANTIQUE : DES TERMES A UX DIAGRAMMES (b) pour toute flèche TF-.S^W de DIAGR(C0) telle que f ^0^(5,5,7,^,7) » 3 ^ \ U'oJ2{â,f3,î,w,T)xK2 on a U{â,p,y,6>,â,T,KuK2)*U'. Preuve. 1. Il s'agit d'une reformulation du lemme 2.17, partie I, page 100. 2. Il s'agit d'une reformulation du lemme 2.19, partie I, page 101. Remarquons que la preuve de ce lemme est constructive, c'est-à-dire construit explicitement un choix de flèche U(â, 0,7, S7, à, Y, 7?7, K2) : S -»• S7. 4.1.2 P r é f o n c t e u r V : TERME(C 0 ) -> DIAGR(C 0 ) Rappelons qu'on a un préfoncteur ICo : C0 -> DIAGR(C0). D'après les lemmes 4.1 et 4.2, on peut appliquer le théorème 3.9, partie II, page 36. Il existe donc un unique préfoncteur V : TERME(Co) -> DIAGR(C0) tel que 1. Wl€Obj(Co), V(A) = ICo(A); 2. 2)(0) = O ; 3. 2>(push (A,B,C, f,g)) = AplCo(VushViagr{V{A),V(B),V{C),V(f),V{g))); 4. V/€Arr(C 0 )(4,5), 2?(/) s / C o ( / ) ; 5. V(gof)=V(g)oV(f); 6. V{\dA) = idV(A) ; 7- P(iA)sJ;p ( > 1 ) ; 8. P(&!(A,B,C, f,g)) = 9. 1>(^2(A,B,C,f,g)) = TyiViA),V(B),V(C),Z>(/),V(g)); MV(A),V(B),V(C),V(f),V(g)); 10.V(up(A,B,C,D,f,g,f',g')) = U(V(A),V(B),V(C),V(D),V(f),V(g),V(f),V(g')). 4.2. EXEMPLE DES ANNEAUX 17 Ces règles donnent une procédure de calcul du diagramme ou morphisme de diagrammes associé à un terme. Remarquons que nous avons remplacé la condition V o J = Ic0 du théorème 3.9 par les points 1 et 4, qui sont évidemment équivalents. Enfin, au préfoncteur V : TERME(Cn) -> DIAGR(Co) est évidemment associé à un foncteur V : Terme(Co) -> diagr(C 0 ). 4.2 Exemple des anneaux Dans cette section, nous calculons les diagrammes associés aux spécifications modulaires des anneaux A2, A!2, .4 3 et A4 présentées dans le chapitre 1. Pour chaque spécification modulaire A, nous calculons donc V(A), en utilisant les règles de calcul du préfoncteur V : TERME(Co) -> DIAGR(C0) décrites dans le paragraphe 4.1.2. 4.2.1 D i a g r a m m e a s s o c i é à la spécification A2 Dans le chapitre 1, nous avons défini une spécification modulaire des anneaux A2 de la façon suivante (cf. partie I, page 41). Nous commençons par construire une spécification MD en combinant la spécification M des monoïdes avec la spécification D qui contient deux opérateurs distributifs, et en partageant la spécification de l'opérateur binaire multiplicatif. Puis on obtient une spécification des anneaux en combinant MD avec la spécification G des groupes, et en partageant l'opérateur additif. MD = push (B, M, D, b, m*) A2 = push {B, MD, G, &L2{MD) O m+, m o b) Nous calculons d'abord le diagramme associé à MD. V{MD) = = V{push{B,M,D,b,m*)) Ap\Co{VushT>i,agr{V{B),V{M),V{D),V{b),V{m*))) V(B) = ICo{B) = ÇT) V{M) = ICO(M) ÇM) V(D) = = ICO(D)=ÇTD) P(6) = /Co(6)= ( F ^ - ^ J M ) V{mm) = ICo(m.) = (B^}^^F) 18 CHAPITRE 4. SÉMANTIQUE: DES TERMES AUX DIAGRAMMES V(MD) = Api. Nous calculons maintenant le diagramme associé à A2. V(A2) = = V(G) = V{p\ish{B,MD,G,&2{MD)om+,mob)) AplCo{VushTHagr{V(B),V{MD),V(G),V(ë<.2(MD)om+),V{mob))) Ic0{G)=(*G) V(&.2(MD) o m+) = V{&.2{MD)) o V{m+) V(b2(MD)) 2>(m+) = = T2{V{B),V{M),V{D),V(b),V{m„)) (Bjy^^D) V{&2(MD) o m+) = V(mob)= ( B » ) ^ ^ G ) 19 4.2. EXEMPLE DES ANNEAUX V(A2) = AplCo = S-2 Finalement, le diagramme associé à la spécification A2 est le diagramme 62 que nous avions donné partie I, page 43. 4.2.2 D i a g r a m m e associé à la spécification A'2 Nous calculons maintenant le diagramme associé à la spécification ,42 des anneaux. La spécification A'2 a été construite en commençant par combiner les spécifications D et G, puis en ajoutant M (cf. partie I, page 42). DG = push (B, D, G, m+, m o b) A'2 = push {B, M, DG, b, &i{DG) o m«) V{DG) = Apl Co {Vush7>iagr(V(B),V{D),V{G),V{m+),V{m) = A V{b1{DG)om») o V{b))) ?k0 = = V[8n{DG))oV(mm)) Jl{V{B),V{D),V{G),V{m+),V{m) o V{b)) o V{mm) CHAPITRE 4. SÉMANTIQUE: DES TERMES AUX DIAGRAMMES 20 V{A'2) = = AplCo(VushT>iagr(V{B),V(M),V{DG),V(^i(DG))oV(mm))) = AplCo 60 Le diagramme associé à la spécification A'2 est donc, comme pour la spécification A2, le diagramme 52. 4.2.3 D i a g r a m m e a s s o c i é à la spécification A3 Pour la spécification A3 des anneaux, nous avons utilisé deux spécifications intermédiaires : la spécification B2 qui regroupe deux opérateurs binaires, et la spécification P des pseudo-anneaux (cf. partie I, page 43). Rappelons qu'un pseudo-anneau est un anneau sans la propriété de distributivité entre les deux opérateurs. B2 = push{0,B,B,}B,}B) u2 = up ( 0 , B, B, D,iB,iB, m», m+) : B2 -+ D P = push (S,M,G,bos,mobo s) ui = u p ( 0 , B , f î , F , j s , j B , & i ( F ) o 6 , & 2 ( F ) o m o 6 ) : 5 2 - > F A3 = push (B2, F, D, «1, u2) Commençons par calculer le diagramme associé à la spécification B2. V(B2) = AplCo (VushTHagr(V(0),V(B),V(B),VQB),V()B))) V(0) = O V{B) = ÇJ) VHB) = 0^(VB) B» V(B2) = AplCo B* 21 4.2. EXEMPLE DES ANNEAUX Calculons le morphisme de diagrammes associé au morphisme de spécifications u2 : B2^D. V{u2) = V(up(0,B,B,D,jB,}B,m„,m+)) = U(V(0),V(B)MB),V(D),VijB), VQB),V(mm),V(m+)) V(D) = ÇD) V{m.) = ( 5 ^ 4 ^ ) P(m+) = (Ë^^D) V{u2) = Calculons le diagramme associé à la spécification P des pseudo-anneaux. V{P) = AplCo = a (cf. partie I, page 44) Pour calculer le morphisme de diagrammes associé au morphisme de spécifications ui : B2 -» P, nous devons d'abord calculer P(&i(P) o 6) et V(&.2(P) omob). P(&!(P)) = Tl(V{S),V{M),V{G),V{bos),V{mobos)) 22 CHAPITRE 4. SÉMANTIQUE: DES TERMES AUX DIAGRAMMES V(Sci{P)ob) = 2>(& 2 (F)omo6) = J2{V{S),V{M),T>{G),V(bos),V{mobos))oV{m)oV(b) Nous calculons maintenant le morphisme de diagrammes associé à u\ : B2 -> F. X>(ui) = = P(up(0,B,B,F,jB,jB,&1(F)o6,&2(F)omo6)) U(V(0),V(B),V(B),V(P), V{iB),V{jB),V{Si1(P)ob)1V(&2(P)omob)) Nous calculons enfin le diagramme associé à la spécification ^3. 4.2. EXEMPLE DES ANNEAUX V{A3) = = V{pusb = AplCo 23 (B2,P,D,Ul,u2)) Ap\Co(Vush-Diagr(V(B2),V(P)MD)Mui),V(u2))) Le diagramme associé à la spécification A3 est donc le diagramme S3 donné partie I, page 45. 4.2.4 D i a g r a m m e associé à la spécification A4 Rappelons la définition de la spécification A4 des anneaux. Cette spécification utilise la spécification B2 que nous avons déjà vue dans le paragraphe précédent, ainsi qu'une autre spécification F ' des pseudo-anneaux. B2 = p u s h ( 0 , B , B , j B , j B ) u2 = up ( 0 , B, B, D, j B , j B , m „ m + ) : B2 D Qi = push (S, B, B, s, s) Q 2 = push(F,M,Q 1 ,6,& 1 (Q 1 )) F ' = push (B, Q2, G, &2(Q2) o & 2 ( Q , ) , m o b) u3 = u p ( 0 , B , f l , F ' , j B , j B , ^ 1 ( ^ ) 0 ^ 2 ( ^ 2 ) 0 ^ ( ^ ) , &i(F') o& 2 (Q 2 )o& 2 (Qi)) : F 2 -> P' A4 = push {B2, F', D, u3, u2) Nous avons vu dans le paragraphe précédent le diagramme associé à la spécification B2, ainsi que le morphisme de diagrammes associé au morphisme de spécifications «2 : B2 —¥ D. V{B2) = V{u2) = 24 CHAPITRE 4. SÉMANTIQUE: DES TERMES AUX DIAGRAMMES Calculons maintenant les diagrammes associés aux spécifications Q\, Q2 et F 7 . V(Ql) = AplCo V(Q2) = AplCo V(P') = AplCo 25 4.2. EXEMPLE DES ANNEAUX Si un diagramme 6 contient un arc a : n —>• n' étiqueté par la flèche identité (c'est-à-dire tel que S(n) = S(n') et S(a) = id a („)), alors on obtient un diagramme isomorphe en en fusionnant les nœuds n et n' et en supprimant l'arc a : n —> n'. Ce résultat sera démontré dans le chapitre 5. Dans notre exemple, le diagramme Z>(F') est donc isomorphe au diagramme a1 ci-dessous. •M B» A \idB • B P(F') = S» A = a' \ • B B /idB \rnob •G Revenons au calcul de V(A4). Il reste à calculer le morphisme de diagrammes associé au morphisme de spécifications u$ : B2 —> Pf. V(u3) = On en déduit enfin le diagramme associé à la spécification A4. 26 V(A4) CHAPITRE 4. SÉMANTIQUE: = P(push DES TERMES AUX DIAGRAMMES {B2,P',D,u3,u2)) = AplCo En supprimant les quatre arcs étiquetés par des flèches identités, on obtient un diagramme S4, isomorphe à V(A4). •M A >M A B» VB B»/s V{A4) = S» • \ idB B /* B \m* »D S B» /ida B» idB S» *D A- VA* B B = 64 v \mob • G \mob • G 4.3 Équivalence entre les catégories Terme(Co) et diagr(Co) Dans cette partie, nous montrons que les catégories Terme(Co) et diagr(Co) sont équivalentes. Pour cela nous montrons en fait que les précatégories TERME(Co) et DIAGR(Co) sont équivalentes. 4.3. ÉQUIVALENCE 4.3.1 ENTRE Terme{C0) ET diagr(C0) 27 Équivalence entre catégories, équivalence entre précatégories Nous commençons par définir la notion de transformation naturelle entre préJoncteurs. Définition 4.1 (Transformation naturelle entre deux préfoncteurs) Soit deux précatégories C et C Soit deux préfoncteurs F, G :C -*C\ Une transformation naturelle a de F vers G, notée a : F -1» G, est une application qui à tout objet A de C associe une flèche aA G ATT(C')(F{A),G{A)), telle que pour toute flèche / G Arr(C)(4, £ ) , G(f) oaA = crBo F(f) G ATT(C')(F(A),G(B)). Par conséquent, a est une transformation naturelle entre les deux préfoncteurs F et G si et seulement si a est une transformation naturelle entre les foncteurs F et G. Définition 4.2 (Isomorphisme naturel entre deux préfoncteurs) Une transformation naturelle a : F -^ G entre deux préfoncteurs F, G :C -* C est un isomorphisme naturels et seulement si pour tout objet A de C, aA G Arr(C'){F{A),G{A)) e s t u n isomorphisme. Si a : F -^ G est un isomorphisme naturel, on dit que les préfoncteurs F et G sont naturellement isomorphes, et on note F = G. On vérifie facilement que deux préfoncteurs sont naturellement isomorphes si et seulement si les foncteurs associés sont naturellement isomorphes. Rappelons la définition d'équivalence entre deux catégories. Définition 4.3 (Équivalence) Deux catégories C et C sont équivalentes si et seulement si il existe deux foncteurs F : C -» C et G : C ->• C tels qu'on ait deux isomorphismes naturels G o F = Idc et F o G = Idc> On en déduit une définition d'équivalence entre deux précatégories. Définition 4.4 Deux précatégories C et C1 sont équivalentes si et seulement si il existe deux préfoncteurs F : C -> C et G :C ->• C tels qu'on ait deux isomorphismes naturels G o F 2 Idc et F o G S Afc,. Deux précatégories sont équivalentes si et seulement si les catégories associées sont équivalentes. 4.3.2 Équivalence e n t r e les p r é c a t é g o r i e s DIAGR(C 0 ) et TERME(C 0 ) Dans ce paragraphe, nous montrons qu'il existe une équivalence entre les précatégories DIAGR(Co) et TERME(C 0 ). Intuitivement, cela signifie que ces deux précatégories ont "la même structure", "aux isomorphismes entre objets près". Nous commençons par reformuler le théorème 2.7 (partie I, page 109) en utilisant des précatégories. Théorème 4.1 La précatégorie DIAGR(Cn) est une complétion de CQ par pré-colimites finies. Autrement dit, pour toute précatégorie S finiment pré-cocomplète, et tout préfoncteur F : CQ —> £, il existe un préfoncteur H : DIAGR(Co) -> S, 28 CHAPITRE 4. SÉMANTIQUE: DES TERMES AUX DIAGRAMMES unique à un isomorphisme naturel près, qui conserve les pré-colimites finies, tel que HoICo*F. Comme la précatégorie TERME(Co) est finiment pré-cocomplète, et comme on a un préfoncteur J : CQ —• TERME(Cn), il existe un préfoncteur T : DIAGR(Cn) -> TERME(Co), qui conserve les pré-colimites finies, tel que ToICo*J. D'autre part, nous avons vu au paragraphe 4.1.2 que le préfoncteur V : TERME(Co) -» DIAGR(C0) conserve l'objet pré-initial et les pré-sommes amalgamées. Le préfoncteur V conserve donc les pré-colimites finies. De plus, on a VoJ = ICo. Lemme 4.3 On a les isomorphismes naturels suivants: 1. VoToICo^ICo; 2. ToVoJ^J. Preuve. C'est une conséquence immédiate de T o Ic0 ^ J et V o J = Ic0. D Proposition 4.1 On a un isomorphisme naturel V o T = WDIAGR(CO)- Preuve. D'après le lemme 4.3-1, on &V oTo Ic0 — Ic0- De plus, les préfoncteurs VoT : DIAGR(Co) -> DIAGR(C0) et IdDlAGR(Co) : DIAGR(C 0 ) ->• DIAGR(C 0 ) conservent les pré-colimites finies. Par conséquent, d'après le théorème 4.1, VoT= W D I A G R ( C o ). L e m m e 4.4 Soit A,B,Cç. Obj(TERME(C 0 )), / € Arr(TERME(C 0 ))(A, B) et g G Arr(TERME(C 0 ))(,4,C). Alors, le triplet ( (ToV)(push(A,B,CJ,g)), (ToV)(b2(A,B,C,f,g)) est une présomme amalgamée de (ToV)(B) (ToV)(f)et(ToV)(g). ) et (ToV)(C) par rapport aux flèches 4.3. ÉQUIVALENCE ENTRE Terme{C0) ET diagr{C0) 29 Preuve. Comme les préfoncteurs V et T conservent les pré-sommes amalgamées, le préfoncteur ToV conserve également les pré-sommes amalgamées. • Proposition 4.2 On a un isomorphisme naturel # : T o V -^ IdTERME(C0)' Preuve. Comme T o P et WTERME(C 0 ) s o n t des préfoncteurs de la précatégorie TERME(Co) vers TERME(C 0 ), il faut donner, pour tout objet U de TERME(C 0 ), un isomorphisme Vu'(ToV){U)-±U dans TERME(Co). On définit cet isomorphisme par induction sur la structure des objets de TERME(Cn)> et on vérifie qu'il s'agit bien d'une transformation naturelle par induction sur la structure des flèches de TERME(Co). Soit un objet U de TERME(Cn). On définit Vu par induction sur la structure des objets de TERME(C 0 ) (cf. partie II, règles 1 à 10, page 22). Règle (1) U = J{A), où A est un objet de C0. D'après le lemme 4.3-2, T o V o J = J. Par conséquent, il existe un isomorphisme Vu'-{ToV){U)->U. Règle (2) U = 0 . ( T o X>)(0) = T ( O ) = 0 car T conserve l'objet pré-initial. Soit #0 : ( T o D ) ( 0 ) - + 0 cet isomorphisme. Règle {3) U = push {A, B , C , /,A VB:{ToV)(B)^B *c:(To£>)(C)->C tels que fo9A = goVA = VBo(ToV)(f) qco{ToV){g). D'après le lemme 4.4, le triplet ( (ToV)(push(A,B,C,f,g)), (ToV)(^(A,B,C,f,g)), (ToV)(b2(A,B,C,f,g)) ) 30 CHAPITRE 4. SÉMANTIQUE: DES TERMES AUX DIAGRAMMES est une pré-somme amalgamée de (ToV)(B) flèches {ToV){f) et ( T o V){g). et (7~oZ>)(C) par rapport aux D'autre part, le triplet (push (,4,5,(7,/, s), &i(4,B,C,/,0), &i(i4,J3,C,/,flF)) est évidemment une pré-somme amalgamée de B et C par rapport aux flèches / et g dans TERME(C0). Par conséquent, il existe un unique isomorphisme * l / = *push(A,B,c,/,3) : (ToP)(push (A, B,C,/, push (A,J5,C,/, 5 ) tel que « y o (To 2>)(&i(A, B, C, / , 5 ) ) = &!(A, B, C, / , 5 ) o * B yuo(ToV)(b2(A,B,C,f,g)) = iL2(A,B,C,f1g)oVc. On vérifie maintenant qu'on définit bien une transformation naturelle * : T o P ^ WTERME(C0)» par induction sur la structure des flèches de TERME(Co). Règle (4) Soit / : A -> B une flèche de CQ. Comme ¢,4 et $ B sont les isomorphismes correspondant à Fisomorphisme naturel T o P o J = J , o n a donc VBo{ToV){f) = fo9A. Règle (5) Soit deux flèches / : A -+ B et )Gyi) = ÏA ° * 0 c a r c e s deux flèches ont pour domaine un objet pré-initial de TERME (CQ). Règle (8) Par définition de *push(vi,B,c,/,s)> o n a Règle (9) Par définition de * pus h( J 4,B,c,/, a )' o n a *push(^B,C,/,fl)° ( T o P J ^ A . B . C / . j ^ t î ^ B . C / . j J o ï c 4.3. EQUIVALENCE ENTRE Terme{C0) ET diagr{C0) 3i Règle (10) Posons &2 = & 2 ( A , B , C , / , 5 ) up = up {A, B,C, D,f,g,f',g') *push — *push (A,B£,f,g) Il faut montrer que *Do(ToP)(up) = upo*push. Pour cela, il suffit de montrer * D o ( T o P)(up) o ( T o ©)(&!) = up o * p u s h o ( T o V){8n) *Do(ToP)(up)o(To2?)(&2) = upo*pusho(ToP)(&2). # D o ( T o 2?)(up) o ( T o P ) ( t i ) = * D °(ToX>)(upo& 1 ) = * D o (T o V) (/') = /' o ¢^ = upo&!0$B = "P°V0(Toî))(&i) ( T o P préfoncteur) (définition de up) (hypothèse d'induction sur / ' ) (définition de up) (règleS) On montre de la même façon que * D o ( T o P)(up) o ( T o V){8L2) = up o * p u s h o ( T o P ) ( & 2 ) . Théorème 4.2 Les précatégories TERME(Co) et DIAGR(Co) sont équivalentes. Preuve. Conséquence immédiate des propositions 4.1 et 4.2. • Corollaire 4.1 Les catégories Terme(Co) et diagr(Co) sont équivalentes. La proposition 4.2 nous permet de montrer que deux objets de Terme(Cn) sont isomorphes si et seulement si leurs diagrammes associés sont isomorphes, et deux flèches de Terme(Cn) sont égales si et seulement si leurs morphismes de diagrammes associés sont égaux dans diagr(Cn). Théorème 4.3 Considérons le foncteur V : Terme(Co) —• diagr(Co). • Soit A et B deux objets de Terme(Co). Alors, A^B *> V{A)^V{B). • Soit f,g : A —> B deux flèches de Terme(Co). Alors, f = 9 «• V(f) = V(g). 32 CHAPITRE 4. SEMANTIQUE: DES TERMES AUX DIAGRAMMES Preuve. Les deux implications de gauche à droite sont évidentes car V est un foncteur. Dans l'autre sens, d'après la proposition 4.2, il existe un isomorphisme naturel $ : T o P - ^ ^TermeJCn) entre les foncteurs T oV : Terme(Co) -> Terme(Co) et IdTerme(Co) '• Terme(C0) -+ Terme(C 0 ). • Soit deux objets A et B de Terme(Co). V(A) S V{B) => => A^B {ToV){A)*(ToV)(B) (*'ToV^IdTerme{Co)) • Soit deux flèches / , # : A —>• B de Terme(Cn) telles que P ( / ) = î>(flf) dans diagr(Co). V(f) = V(9) => ( T o P ) ( / ) = ( T o P ) ( s ) => * B O ( T O P ) ( / ) = *J9O(TOÎ))(5) => / o ^ = « o ^ =* / = gf 4.3.3 ($:ToP^/dTerme(Cfl)) (9A isomorphisme) Correction du calcul de d i a g r a m m e s La proposition 4.2 nous permet également de déduire que le calcul de diagrammes décrit par le foncteur V : Terme(Co) —> diagr(Cn) est correct c'est-à-dire que la colimite d'un diagramme associé à une spécification modulaire est isomorphe à cette spécification. Considérons une catégorie d'interprétation £ à objet initial choisi et sommes amalgamées choisies, par exemple la catégorie des spécifications Spec. Soit une interprétation de Co, c'est-à-dire un foncteur SQ : CQ —> £. D'après le théorème 2.7, ce foncteur s'étend aux diagrammes en un foncteur SD : diagr(Co) -> t. On a en fait SD = colim£odiagr(«So). D'après le théorème 3.9, le foncteur SQ s'étend également aux termes en un foncteur ST : Terme(Co) -> S. De plus, comme SD et Sx conservent les colimites, d'après le théorème 2.7, on a SD = STo T. Par conséquent, SD ° V = ST o T o £>, et donc, d'après la proposition 4.2, SD o P = Sj. Ce résultat exprime que la colimite d'un diagramme associé à une spécification modulaire est isomorphe à cette spécification. 4.4. CONCLUSION 4.4 33 Conclusion Dans ce chapitre, nous avons montré comment associer à tout terme qui représente une spécification modulaire un diagramme dont la colimite est isomorphe à cette spécification. Cette association est décrite par le préfoncteur V : TERME(Co) -> DIAGR(C 0 ). Le calcul d'un diagramme associé à un terme consiste simplement à appliquer les règles de calcul de V définies dans le paragraphe 4.1.2. Une des règles principales est la règle 3 qui aplatit un diagramme de diagrammes, c'est-à-dire transforme un objet de DIAGR2(C0) en un objet de DIAGR(C 0 ). Nous avons montré que les précatégories TERME(Cn) et DIAGR(Cn) sont équivalentes, ce qui signifie qu'elles ont essentiellement la même structure "aux isomorphismes entre objets près". Il faut néanmoins remarquer que TERME(Co) et DIAGR(Cn) rce sont pas isomorphes. En fait, pour qu'elles soient isomorphes, il faudrait que ces deux précatégories aient les mêmes choix de pré-colimites, ce qui n'est pas le cas. Par exemple, push (A, B,C, f,g) et push (-4,C, B,g,f) sont deux présommes amalgamées différentes dans TERME(Co) qui sont envoyées sur le même diagramme dans D I A G R ( C Q ) . Chapitre 5 Isomorphismes entre diagrammes Nous considérons une catégorie de base CQ, et nous nous intéressons dans ce chapitre à la détection d'isomorphismes entre deux diagrammes dans la catégorie diagr(Co). Nous avons vu dans le chapitre 4 que deux objets A et B de la catégorie Terme(Co) s o n t isomorphes si et seulement si leurs diagrammes associés V(A) et V(B) sont isomorphes (théorème 4.3 page 31). Une solution pour savoir si deux termes A et B sont isomorphes consiste donc à détecter un isomorphisme entre leurs diagrammes associés. En section 5.1, nous décrivons des transformations de diagrammes, qui sont des fonctions sur l'ensemble des diagrammes sur CQ. Les transformations qui nous intéressent particulièrement sont les transformations stables par isomorphisme, c'est-àdire telles que le diagramme résultat est isomorphe au diagramme de départ. Ces transformations nous serviront à calculer la complétion d'un diagramme. En section 5.2, nous présentons un algorithme pour détecter si deux diagrammes sont isomorphes, dans la cas particulier où la catégorie CQ et finie et sans cycle. Cet algorithme consiste à compléter puis à calculer la forme minimale du diagramme. Ensuite, deux diagrammes sont isomorphes si et seulement si ils ont la même forme minimale. Enfin, en section 5.3, nous montrons les difficultés rencontrées lorsque la catégorie de base CQ comporte des cycles ou est infinie. 5.1 Transformations de diagrammes Nous présentons quelques transformations de diagrammes: la substitution par objet isomorphe, la suppression d'un arc, Yajout d'un arc étiqueté et la contraction d'un arc identité. Définition 5.1 (Transformation de diagrammes) Une transformation de diagrammes est une fonction sur l'ensemble des objets de diagr(Co) T : diagr(Co) -> diagr(Cn). 35 36 CHAPITRE 5. ISOMORPHISMES ENTRE DIAGRAMMES Les transformations intéressantes sont les transformations stables par isomorphisme c'est-à-dire qui produisent un diagramme isomorphe au diagramme de départ. Définition 5.2 (Transformation stable par isomorphisme) Une transformation de diagrammes T : diagr(Co) —> diagr(Co) est stable par isomorphisme si et seulement si pour tout diagramme S, T{I) S S. Deux diagrammes â et /3 sur CQ sont isomorphes dans diagr(Cn) s'il existe deux flèches â : â - * / ? e t r : / ? - » â d e DIAGR(Co) telles que l [ri ° \?] = [idâ] | r o ? « idâ- Rappelons qu'une flèche a : a —> /3 de DIAGR(Co) est un couple (cf. définition 2.18, partie I, page 66) â : 5 - > / ? = ( a * : Q * < N - > / ? * , a : a ~* (5 o a*) où a® : a^ ~-> /î* est un morphisme généralisé de graphes et a : a ^+ /3 o a® est une transformation naturelle généralisée. • Le morphisme généralisé de graphes /3* associe à tout nœud de Û $ un nœud de /?*, et à tout arc a : m —> n de a^ un zigzag &®(a) : a®(m) ~—» /3(cr*(n)). De plus, la condition suivante doit être satisfaite : pour tout arc a : m —> n de a*, anoa{a) 5.1.1 ^ am [a*(a)]. S u b s t i t u t i o n par o b j e t i s o m o r p h e Soit un diagramme S sur CQ, un nœud no de S®, et un objet B de Co isomorphe à £(no). Intuitivement, la substitution par objet isomorphe consiste à remplacer l'étiquette S(UQ) du nœud no par l'objet B. On obtient alors un diagramme isomorphe au diagramme de départ S. Définition 5.3 (Subst_Obj_lso) Soit un diagramme S, un nœud no de £*, et un objet B de CQ isomorphe à S(UQ). Soit : 5(UQ) -» B l'isomorphisme entre S(UQ) et B. Le diagramme /3 = Subst-Obj_lso(£, n0, B, ) est défini de la façon suivante. • Graphe /3* : / 3 * = **. 5.1. TRANSFORMATIONS DE DIAGRAMMES 37 • Foncteur /3 : /?* - • C0. - Action sur les nœuds. • Vn G Nœud(**), n ^ n 0 : /3(n) = 6{n) ; • /3(no) = B. - Action sur les arcs. Soit un arc a : n -> n1 G Arc( o 8(a) ; • si n = no et n7 = no : /3(a) = <£ o £(a) o ~1. P r o p o s i t i o n 5.1 La transformation Subst_Obj_lso est stable par isomorphisme. Preuve. Soit un diagramme 6, un nœud no de S®, et un isomorphisme : S(UQ) —» B de CQ. Soit /3 = Subst_Obj_lso(£, no, B, (f>). On construit deux flèches de DIAGR(Co), W:8-*(3etT:/3 —> S telles que â o r « idp et f o â « idj. • On définit /3 de la façon suivante. - Le morphisme généralisé de graphes a® : 6® —• /3* est l'identité. . a = ic^*. - La transformation naturelle généralisée cr : S ^^> /3 o a* est définie par: • Vn G Nœud (S®) tel que n ^ no, a n = 2^( n ) î • ^n0 = • Cela définit bien une transformation naturelle généralisée car pour tout arc a : n -» n' G Arc(â*), on a <5 o r^ est définie par : • Vn G Nœud(/?*) tel que n ^ UQ, rn = idp^ ; Cela définit bien une transformation naturelle généralisée car pour tout arc a : n -» n' G Arc (/?*), on a rn/ o /3(a) = £(a) o rn. • On vérifie que a o r = id-Q. • On vérifie également que r o a = idj. Par conséquent 6 = /3 dans la catégorie diagr(Co). En fait, les diagrammes 8 et {3 sont ici également isomorphes dans la catégorie DIAGR(Co). D CHAPITRE 5. ISOMORPHISMES ENTRE 38 DIAGRAMMES Exemple 5.1 Considérons le diagramme TT, construit sur le graphe TT*. Soit 4> : A —ï A' un isomorphisme de Co- Alors, nous pouvons considérer le diagramme W1 = Subst_Obj.lso(jf, 0, A', 4>). B fot~l c diagramme itf diagramme n graphe 7r L'isomorphisme a : n —» ïf est composé du morphisme de graphes a* = idn* et de la transformation naturelle généralisée a : n ^ ^ n' o a® définie par GQ = ¢, B •- a\ = ids, 02 = idc- 1 •C an = idc C isomorphisme a : n —> nf 5.1.2 Suppression d'un arc Soit un diagramme S sur CQ. Intuitivement, supprimer Varc aQ : no —» n'Q du diagramme 6 consiste à retirer l'arc ao du graphe S® et à conserver les mêmes étiquettes pour les arcs et les nœuds restants. Définition 5.4 (Suppr_Arc) Soit un diagramme S et un arc ao : no —> n'0 G A r c ( ^ ) . Le diagramme /3 = Suppr_Arc(<$, ao) est défini de la façon suivante. • Le graphe /3* est le graphe ô® auquel on retire l'arc ao- Nœud(/?*) = Nœud($*); - Arc(/3*) = A r c ( £ * ) - { a 0 } . 5.1. TRANSFORMATIONS DE DIAGRAMMES 39 • Le foncteur /3 : /3* —> CQ est la restriction de 8 : 8* -> CQ à /3*. - Vn G Nœud(/3*), /3(n) = «(n) ; - Va : n -+ n' G Arc(/3*), /3(a) = n de 8* qui a le même nœud pour source et but. Définition 5.5 (Boucle) Soit un graphe £*. Un arc a de 8* est une boucle si et seulement si Source(a) = But(a). Une boucle identité SUT un diagramme 8 est une boucle de 6* étiquetée par une flèche identité. Définition 5.6 (Boucle identité) Soit un diagramme 8 sur CQ. Une boucle identité sur 8 est une boucle a : n —> n de 8® telle que 8(a) = ids(ny Proposition 5.2 Soit un diagramme 8 et une boucle identité ao : no Alors, dans la catégorie diagr(Co), Suppr_Arc(£, ao) = 8. no sur 8. 40 CHAPITRE 5. ISOMORPHISMES ENTRE DIAGRAMMES Preuve. Considérons un diagramme 8 et une boucle identité ao : no —>JIQ de 8. Soit /3 = Suppr_Arc( /3 et r : (3 ->8 telles que â o f « idp e t f o â w idj. • On définit a : 8 -> /3 de la façon suivante. - Morphisme généralisé de graphes a® : 8® —> /?*. • V n G N œ u d ^ ) , (3 o a*. • Vn G Nœud (5*), • 8®. • VnGNœud(/3*), r*(n) = n ; • Va€Arc(/?*), r*(a) = a. - Transformation naturelle généralisée r : /3 *v^> (5or $ . • VnGNœud(/3*), rn = id0{n). • On a â o r = id-j. • On vérifie également que f o â « idj. Par conséquent, les diagrammes 8 et /3 sont isomorphes dans la catégorie diagr(Co). D E x e m p l e 5.3 Soit A un objet de CQ. Considérons le diagramme Ic0{A), construit sur le graphe 1*. Rappelons que le graphe 1 $ contient un seul nœud appelé *. O (3) graphe 1* diagramme IcQ{A) Considérons le graphe p® qui contient un nœud appelé 0 et un arc b : 0 —> 0. Etant donné un objet A et une flèche / : A - • A de CQ, on note p(A, f) le diagramme construit sur le graphe p*, qui associe au nœud 0 l'objet A et à l'arc 6 la flèche / . Nous considérons ici le diagramme p(A, icU)- 0 graphe p® diagramme p(A, idù) 5.1. TRANSFORMATIONS 41 DE DIAGRAMMES Les diagrammes Ic0(A) et p(A,idA) sont isomorphes, car ICo{A) = Suppr-Arc(p{A,idA),b) et b est une boucle identité sur p(A, irf^). Un doublet sur un diagramme 8 est un couple d'arcs qui ont tous les deux la même source et le même but, et étiquetés par la même flèche de CQ. Définition 5.7 (Doublet) Soit un diagramme 8 sur CQ. Un doublet sur 8 est un couple d'arcs (ao,ax) tel que Source(a0) = Source(ai), But(a 0 ) = But(ai) et 8(ao) = 8(ai). Exemple 5.4 • Soit deux objets A et B et une flèche / : A -> B de CQ. Considérons le diagramme 7fj~, construit sur le graphe n®, défini par A; 7r(l) = 7r(2) = £ ; 7r(a) = n(b) = f. TT(0) = graphe 7r* diagramme 7Ti Le couple (a,6) n'est pas un doublet sur Tt\, bien que les arcs a et 6 soient étiquetés par la même flèche / de CQ, car ces arcs n'ont pas le même but. • Considérons le diagramme TTf, construit sur le graphe K®. •: 0 • : A graphe K® diagramme K\ B Le couple (a, b) est un doublet de Kï. Proposition 5.3 Soit un diagramme 8 sur CQ et un doublet (ao,ai) de 8. Alors, dans la catégorie diagr(Co), Suppr_Arc(J, ao) = 8. 42 CHAPITRE 5. ISOMORPHISMES ENTRE DIAGRAMMES Preuve. Soit un diagramme 8 et un doublet (a 0 , ai) de ^Soit^/3 = Suppr_Arc(ï, ao). On construit deux flèches de DIAGR(C0), â :ô-+PetT:/3-> 6 telles que âor « id^ et f o â « idj. • On définit cr : 8 -* /3 de la façon suivante. - Morphisme généralisé de graphes a® : 8® —• /3*. . V n G N œ u d ( ^ ) , • 5 de la façon suivante. - Morphisme généralisé de graphes r $ : /3* —• £*. - VnGNœud(/3*), r*(n) = n; - VaGArc(/3*), r*(a) = a. - Transformation naturelle généralisée r : (3 ^1½ 8 o r*. • Vn G Nœud (/3*), rn = idp(n). • On a â o f = icfe. • On vérifie également que f o â « idj. Par conséquent, les diagrammes 8 et j3 sont isomorphes dans la catégorie diagr(Co). D Exemple 5.5 Les diagrammes suivants sont isomorphes dans diagr(Co). A 5.1.3 f B B Ajout d'un arc é t i q u e t é Étant donné un diagramme 8, l'opération d'ajout d'arc étiqueté consiste à ajouter un arc au diagramme sous-jacent 8® et à étiqueter cet arc par une flèche de CQ. Définition 5.8 (Ajout_Arc) Soit un diagramme 8, deux nœuds n 0 et ni de 8® et une flèche / : 8(n0) -¥ 8(rti) de CQ. L'ajout d'un arc de n 0 vers ni étiqueté par / dans le diagramme 8 est le diagramme /3 = Ajout_Arc(£, n0, n\, f) 5.1. TRANSFORMATIONS DE DIAGRAMMES 43 défini de la façon suivante. • Le graphe /3* est le graphe 8® auquel on ajoute un nouvel arc ax : no —• ni. - Nœud(/3*) = Nœud(**); - Arc(/3*) = Arc(£*) U {ax}, où a r ¢. Arc(5 $ ), avec Source(a x ) = no et But(a x ) = ni. • Le foncteur /3 : /3 $ —> CQ étend le foncteur 8 en associant à l'arc ax la flèche / . - Action sur les nœuds. • VnGNœud(/3*), /3(n) = 8{n). - Action sur les arcs. • Va G Arc(/3*), a ^ a*, /3(a) = S (a) ; • /3(ax) = / . La transformation Ajout_Arc n'est évidemment pas stable par isomorphisme dans le cas général. E x e m p l e 5.6 Soit un objet A et une flèche / : A —> A dans CQ. Dans le cas général, les diagrammes Ic0{A) et p(A, f) ne sont pas isomorphes dans diagr(Co). (ED* Proposition 5.4 (Ajout de compositions) Soit un diagramme S sur CQ. Soit deux arcs ao : no —> ni et a\ : n\ —>• n 2 de S*. Alors, dans la catégorie diagr(Co), Ajout_Arc(£, n 0 , n 2 , 8(ai) o £(ao)) = 8. Preuve. Soit un diagramme 8 et deux arcs ao : no —> n\ et a\ : ni —» n 2 de 8®. Posons /3 = Ajout_Arc(à, no, n2,£(ai)o5(ao)). On construit deux flèches de DIAGR(Co), W :8 —> /3 et r : /3 —ï 8 telles que â o f « id-z e t f o â » idj. • On définit G : 8 —» /3 de la façon suivante. - Morphisme généralisé de graphes a® : 8® -> /3 $ . • V n G N œ u d ( ^ ) , a*(n) = n ; • Va G Arc(**), a*(a) = a. - Transformation naturelle généralisée a : 8 ~^t (3 o a®. • Vn G Nœud((J*), <7n = idS(n). • On définit f : /3 —» £ de la façon suivante. - Morphisme généralisé de graphes T® : /3* -> £*. • VnGNœud(/3*), r*(n) = n; CHAPITRE 44 5. ISOMORPHISMES ENTRE DIAGRAMMES Va G Arc(/3*), a ^ ax, r*(a) = a; r®(ax) = no -^> ni -^> n 2 (zigzag de longueur de 2). - Transformation naturelle généralisée r : /3 ' ^ no et a 2 : n 2 —> UQ de 6*. Soit une flèche h : 8(ni) —> <5(n2) de CQ telle que n 0 <— n 2 . Cela définit bien une transformation naturelle généralisée r : (3 £(a 2 ) oh = <5(ai). £ o r * . En effet, D 5.1. TRANSFORMATIONS DE 45 DIAGRAMMES Exemple 5.8 Considérons le diagramme 83, vu une première fois dans la partie I, chapitre 1, page 45, et revu dans le chapitre 4, page 23. Nous obtenons le diagramme (¾ à partir du diagramme £3 en ajoutant deux factorisations à droite. S's 5.1.4 C o n t r a c t i o n d'un arc i d e n t i t é Soit un diagramme 8. lïn arc identité du diagramme 8 est un arc de 8® étiqueté par une flèche identité. Définition 5.9 (Arc identité) Soit un diagramme 8 sur CQ. Un arc ao : no —> ni du graphe 8® est un arc identités! et seulement si 8(UQ) = 8(n\) et <5(ao) = id$(noy Intuitivement, contracter un arc identité ao : no —>• ni dans un diagramme 8 consiste à fusionner les nœuds no et ni et à supprimer l'arc ao. Définition 5.10 (ContractJd) Soit un diagramme S et un arc identité ao : no -» ni de 8, tel que les nœuds no et ni sont distincts. Le diagramme /3 = ContractJd(8, ao) est défini de la façon suivante. • Graphe /3*. - Nœud(/3*) = Nœud(**) - {ni} - L'ensemble Arc(/3$) est défini à partir de l'ensemble A r c ( ^ ) de la façon suivante. Soit un arc a : n -» n' de (5*. • n ^ ni et n' ^ ni =ï a : n -> n' G Arc(/3$) ; • n = ni et n7 / ni => a : UQ -> nf G Arc(/3*) ; • n ^ ni et n ; = ni et a 7^ ao =» a : n —ï n0 £ Arc(/3*) ; • n = ni et n7 = ni => a : UQ -> no G Arc(/3*). • Foncteur /3 : /3* -» C0. - Vn G Nœud(/3*), /3(n) = 5(n) ; 46 CHAPITRE 5. ISOMORPHISMES ENTRE DIAGRAMMES - VaGArc(/3*), /3{a) = 8(a). Nous avons supposé que les nœuds no et ni sont distincts, car si no = ni, cela n'a pas de sens de fusionner ces deux nœuds. De plus, si no = ni, alors ao est une boucle identité, qui peut être supprimée par l'opération Suppr_Arc (cf. proposition 5.2). Proposition 5.6 La transformation ContractJd est stable par isomorphisme. Preuve. Soit un diagramme 8 et un arc identité ao : n 0 -> ni de 8, tel que UQ ^ n\. Posons /3 = ContractJd(8, ao). On construit deux flèches de DIAGR(Co), & : 8 —ï (3 et r : /3 -> 8 telles que â o f % id-z e t f o â » idj. • On définit a : 8 —> /3 de la façon suivante. - Morphisme généralisé de graphes a® : 5 ^ - ^ / 3 ^ . • Vn G N œ u d ( ^ ) , n ^ ni, a®(n) = n ; . a*(ni) = n 0 ; • Va G Arc(5<î>), a ^ a 0 , &®{a) = a ; • a^(ao) = 0 no (zigzag nul ayant pour source et but le nœud no de - Transformation naturelle généralisée a : 8 ~^ (3 oa®. • Vn G N œ u d ( ^ ) , an = ids(ny Cela définit bien une transformation naturelle généralisée car £(ao) = id 8(n0)- • On définit r : /3 —> 8 de la façon suivante. - Morphisme généralisé de graphes r® : /3* —>• 5*. • VneNœud(/3*), r*(n) = n ; • Va€Arc(/3*), r*(a) = a. - Transformation naturelle généralisée r : /3 ^-» 5 o r*. - Vn G Nœud(/3*), r n = id0{n). • On a â o r = icfe. • On vérifie également que f o â « idj. 47 5.1. TRANSFORMATIONS DE DIAGRAMMES Exemple 5.9 1. Les diagrammes V(Pf) et o/ (cf. chapitre 4, page 25) sont isomorphes dans la catégorie diagr(Co)- V(P') 2. Les diagrammes 2?(Aj) et 84 (cf. chapitre 4, page 26) sont isomorphes dans la catégorie diagr(Co). •M A B* \dB id £ • - '• B A • D /m+ S • \ B B» idB MB B \mob •G V{A4) 3. Les diagrammes suivants sont isomorphes dans la catégorie diagr(Co). • A ? idA : • A A Cet exemple montre qu'à partir d'un diagramme dont le graphe sous-jacent n'est pas cyclique, la contraction d'un arc identité peut produire un diagramme dont le graphe sous-jacent est cyclique. 48 CHAPITRE 5.2 5. ISOMORPHISMES ENTRE DIAGRAMMES Catégorie Cn finie et sans cycle Dans cette partie, nous nous intéressons à la détection d'isomorphismes lorsque la catégorie CQ est finie et sans cycle. Nous commençons par définir un cycle dans une catégorie. Définition 5.11 (Cycle) Etant donné une catégorie C, un cycle dans C est une flèche / : A —> A ayant même domaine et codomaine A et telle que / =fi idA. Nous dirons qu'une catégorie C ne comporte pas de cycle si et seulement si pour toute flèche / : A —> A de C, f = idA- 5.2.1 Hypothèses Nous supposons que la catégorie de base CQ est finie et ne comporte pas de cycle. Cette hypothèse est compatible avec le langage de spécification LPG, puisque d'une part on ne peut déclarer qu'un nombre fini de spécifications et morphismes de spécifications, et d'autre part, la déclaration d'un morphisme de spécifications ayant la même spécification pour domaine et codomaine est syntaxiquement interdite. D'autre part, nous supposons qu'il n'existe pas d'isomorphisme entre objets dans la catégorie de base CQ. Cette hypothèse est justifiée par la transformation de substitution par objet isomorphe (proposition 5.1). En effet, supposons qu'on a, au départ, une catégorie XQ qui ne possède pas cette propriété. Pour chaque classe d'isomophisme entre objets de XQ, on choisit un représentant. On considère ensuite la sous-catégorie pleine CQ de XQ ayant pour objets ces représentants. La catégorie CQ satisfait alors la propriété suivante : pour tout couple d'objets (.4, B) de CQ, A = B=$>A = B. Tout diagramme sur XQ peut être transformé en un diagramme sur CQ en utilisant la proposition 5.1. Nous faisons également l'hypothèse qu'on sait détecter une égalité entre deux morphismes de spécifications de base, c'est-à-dire que l'égalité est décidable dans CQ. Enfin nous supposons que toutes les factorisations à droite sont connues. Hypothèses 1. CQ est finie. 2. CQ ne comporte pas de cycle. 3. Pour tout couple d'objets {A, B) de CQ, A^ B => A = B. 4. L'égalité sur CQ est décidable. Soit deux flèches f,g : A —> B de CQ. On sait si / = 9 ou / 5É g. 5. On sait effectuer des factorisations à droite dans CQ. Etant donné deux flèches / : A -> B et g : C —> B, on connaît l'ensemble des flèches h : A -> C telles que f = g o h. 5.2. CATÉGORIE C0 FINIE ET SANS CYCLE 49 Remarque 5.1 Les hypothèses 1 et 2 sont distinctes. En effet, il existe des catégories infinies qui ne comportent pas de cycle, et il existe des catégories finies qui comportent des cycles. La combinaison des hypothèses 2 et 3 est très forte, comme le montre le lemme suivant. Lemme 5.1 Soit deux objets A et B ainsi que deux flèches f : A —> B et g : B —» A dans CQ. Alors, A = B et f = g = idA. Preuve. D'après l'hypothèse 2, g o f = idA et f o g = idB, d'où A = B. D'après l'hypothèse 3, on a donc A = B. On en déduit que f et g sont des flèches de A vers A. Par conséquent, en utilisant de nouveau l'hypothèse 2, on obtient f = g = idA. D 5.2.2 F o n c t i o n de c o m p l é t i o n Dans ce paragraphe, nous détaillons la fonction de complétion d'un diagramme. Compléter un diagramme a sur CQ consiste à contracter les arcs identités, supprimer les boucles identités, supprimer les doublets, ajouter les compositions d'arcs et les factorisations à droite. Fonction Complétion ( â : diagramme): diagramme 8, 8Q : diagramme; Début 8 := Q ; Répéter 80 ~8; Pour tout arc identité a de 8: (1) 8 := ContractJd (J, a) ; Pour toute boucle identité a de 8: (2) 8 := Suppr_Arc(J, a) ; Pour tout doublet (ao,ai) de 8: (3) 8 := Suppr_Arc(<5, a 0 ) ; Pour tout couple d'arcs (ao : no —> ni, ai : ni —> U2) de 8 tel que (4) il n'existe pas d'arc a : UQ —> n UQ, a2 : U2 —> UQ) de 8 tel que (5) • il existe une flèche h : 8(n\) —» 8{n2) de CQ vérifiant 8{a2) oh = 8{a\), • il n'existe pas d'arc a : n\ —> n2 étiqueté par h dans 8, CHAPITRE 50 5. ISOMORPHISMES ENTRE DIAGRAMMES 8 := Ajout_Arc(<$, m , n2, h) ; Jusqu'à 5 = 8Q ; Résultat : 8 ; Fin Complétion Proposition 5.7 La fonction de complétion s'arrête. Preuve. On appelle itération le fait d'exécuter successivement les étapes 1 à 5. D'après la condition d'arrêt, on effectue une itération tant que le diagramme a été modifié par l'itération précédente. Chaque étape de l'itération termine : les étapes 1, 2 et 3 parce qu'elles suppriment un arc dans le graphe, et les étapes 4 et 5 parce que la catégorie CQ est finie et qu'on n'ajoute pas une nouvelle composition ou factorisation à droite si l'arc correspondant appartient déjà au diagramme. On ne peut effectuer qu'un nombre fini d'itérations. En effet, seule la contraction d'un arc identité (étape 1) peut permettre ensuite d'ajouter des nouvelles compositions d'arcs ou des nouvelles factorisations à droite. Comme la contraction supprime un nœud dans le graphe, et comme aucune transformation n'ajoute de nœud dans le graphe, on ne peut effectuer qu'un nombre fini d'itérations. D Proposition 5.8 La complétion est une transformation stable par isomorphisme. Pour tout diagramme 8 surCQ, 8 = Complétion(â) dans diagr(Co). Preuve. Toutes les transformations appliquées sur le diagramme 8 par la fonction de complétion sont stables par isomorphisme, d'après les propositions 5.2, 5.3, 5.4, 5.5, et 5.6. D Exemple 5.10 Considérons les diagrammes 8i, 83 et 84. Si 5.2. CATÉGORIE C0 FINIE ET SANS CYCLE 51 La complétion de ces trois diagrammes produit le même diagramme 8' : Complétions) = Complétion^) = Complétion^) = 8f. Un diagramme est complet si celui-ci est égal à sa complétion. Définition 5.12 (Diagramme complet) Un diagramme 8 sur CQ est complet si et seulement si 8 = Complétion(8). E x e m p l e 5.11 Le diagramme 82 est complet : 82 = Complétion^). L e m m e 5.2 Soit un diagramme complet 8 sur CQ. Alors il n'existe aucune boucle dans le graphe 8®. Preuve. Supposons par l'absurde qu'on a une boucle, c'est-à-dire un arc a : n n dans £*. On a soit 8(a) = id^n), soit 8(a) ^ ids(ny La supposition 8{a) = id$(n) est en contradiction avec l'hypothèse que 8 est complet. La supposition 8(a) ^ ids(n) est en contradiction avec l'hypothèse que CQ ne comporte pas de cycle. Par conséquent, il n'existe pas de boucle dans le graphe 8®. • L e m m e 5.3 Soit un diagramme complet 8 surCQ. Soit deux nœuds n\, U2 et un arc a : n\ —> U2 dans le graphe 8®. Alors, il n'existe aucun arc de U2 vers ni dans 8®. 52 CHAPITRE 5. ISOMORPHISMES ENTRE DIAGRAMMES Preuve. S'il existe un arc a' : n 2 —» ni dans 8®, alors comme 8 est complet, il existe un arc a\ : n\ —¥ n\ étiqueté par la flèche 8{a') o 8(a), ce qui est impossible d'après le lemme 5.2. • 5.2.3 Zigzags é l é m e n t a i r e s e t liens La complétion d'un diagramme permet d'obtenir une forme un peu plus "canonique" pour les diagrammes. Cependant, deux diagrammes complets peuvent être isomorphes dans diagr(Co) sans être identiques. Par exemple, les diagrammes 82 et 81 sont complets et isomorphes, mais ne sont pas identiques. Pour détecter cet isomorphisme, nous devons introduire la notion de zigzag élémentaire. Définition 5.13 (Zigzag élémentaire) Un zigzag élémentaire sur un graphe 8® est un zigzag de longueur 2 de la forme rao <— m\ —> nfi2 tel que les arcs ao et ai sont distincts. Nous avons également besoin d'une relation dHnclusion sur les zigzags. Intuitivement, le zigzag Z est inclus dans le zigzag Z1 si Z est un usous-zigzag" de Z1. Définition 5.14 (Inclusion de zigzags) Soit un graphe 8®. Considérons deux zigzags Z et Z' sur <5*. Posons Z = (k, Zjy, ZA) et Z1 = (kf, Z'N, Z'A), avec Zx = (n0,ni,...,nk) Z,N = {nf0,n\,...,nfk,) et ZA = (a0,ai,..., a^-i) ; et Z'A = {a'0,a'x,.. .,a' fc /_i)- On dit que le zigzag Z est inclus dans le zigzag Z1, et on note Z Ç Z1 si et seulement si il existe un entier j , 0 < j < k' — k, tel que • Vi, 0 < i < k, ni = nj + • ; • Vi, 0 < i < k — 1, a{ = a ' + j . Remarquons que si Z Ç Z1, alors nécessairement A: < kf. Soit un diagramme complet 8. Les zigzags élémentaires sur le diagramme 8 sont les zigzags élémentaires sur le graphe 8®. Nous définissons maintenant une relation d'ordre sur les zigzags élémentaires d'un diagramme complet. Définition 5.15 Soit un diagramme complet 8 sur CQ. On définit une relation d'ordre < sur les zigzags élémentaires du diagramme complet 8 de la façon suivante. Soit deux zigzags élémentaires Z\ et Z2 sur 8. Posons Z\ = vfiQ <^- m\ --½ m2. • On a Z\ < Z2 si et seulement si il existe un zigzag Z' = (Ar',Z^,Z^), avec Z'N = (n'Q, n ^ , . . . , n'k,) tel que — rao = ng et 7712 = n'k, ; 53 5.2. CATÉGORIE C0 FINIE ET SANS CYCLE - Z2CZ'; -S(a0)r^S(ai) [Z1]; - Vi, 0 < i < k', mi ^ n<. • On a Z\ < Z2 si et seulement si Z\ — Z mi« m 2 = n 4 Zx Remarque 5.2 Supposons Z\ < Z2. 1. C'est le zigzag Z\ qui paraît "le plus grand". Nous avons choisi le sens Z\ < Z2 car intuitivement, toute l'information sur les partages contenue dans le zigzag Z\ est contenue dans les zigzags élémentaires de Z'. 2. Soit {ci : 8(m\) —> 8(n'{) ; i € {0, ...,k'}} l'ensemble des flèches qui correspondent à la connexion 5(ao) ~ j 8(a\) [Zf] (cf. définition 2.17, partie I, page 66). Alors, comme le diagramme 8 est complet, pour tout entier i, 0 < i < k1, il existe un arc 6t : rai —¥ n[ dans 8* tel que 8(bi) = c,-. Proposition 5.9 Soit un diagramme complet 8 surCo. La relation < sur les zigzags élémentaires sur 8 est une relation d'ordre. Preuve. On utilise la définition de < ainsi que le lemme 5.3. Réflexivité. La relation < est réflexive par définition. Antisymétrie. Soit deux zigzags élémentaires sur 8 Z1 = 77lo i ao rai ai > 7712, 2 = no <— ni —> n2Supposons Z\ < Z2 et Z2 < Z\. Par l'absurde, si Z\ ^ Z2, alors Z\ < Z2 et Z2 < Z\. Par conséquent, on a rai / ni. De plus, il existe un arc a : m\ -+ n\ et un arc a1 : n\ —> m\ dans 8®. Cela est impossible d'après le lemme 5.3. CHAPITRE 5. ISOMORPHISMES ENTRE 54 DIAGRAMMES Transitivité. Soit trois zigzags élémentaires Z\, Z2 et Z3 sur un diagramme complet S. Supposons Z\ < Z2 et Z2 < Z3. Si Z\ — Z2 ou Z2 = Zz alors on a évidemment Z\ < Z3. Si Z\ < Z2 et Z2 < Z 3 , alors on vérifie que Z\ < Z3. Par exemple, dans le diagramme 6', Mbos_SrnobosG < M Ji_ B^D, bos M D bos grn^çs D rrimOs £ mobos ^ < < B^D, M DP±BÏ^G. • M S • mobos Comme la relation < est une relation d'ordre sur l'ensemble fini des zigzags élémentaires de 8, cet ensemble contient des éléments maximaux. Intuitivement, toute l'information sur les partages est contenue dans les zigzags élémentaires maximaux. Définition 5.16 (Zigzag élémentaire maximal sur un diagramme complet 8) Soit un diagramme complet 8. Un zigzag élémentaire maximal sur 8 est un élément maximal pour la relation d'ordre < sur l'ensemble des zigzags élémentaires de 8. Par exemple, les zigzags élémentaires _b_ M^-B^D D?± B^G sont maximaux dans le diagramme 8f. Par contre, les zigzags élémentaires M i M bos ç, mobos ^ O ^ CJ bos_ grn^os D 771*05 £, mobos j~^ y (_J D <—— D ne sont pas maximaux dans 81. 5.2. CATEGORIE C0 FINIE ET SANS CYCLE 55 Nous avons encore besoin de quelques définitions avant de donner un critère d'isomorphisme entre deux diagrammes. Nous commençons par définir un nœud puits dans un graphe. Un nœud puits est un nœud d'où ne part aucune flèche. Définition 5.17 (Nœud puits) Soit un graphe 8®. Un nœud puits de 8® est un nœud n G Nœud((5$) qui vérifie la condition suivante : il n'existe aucun arc a G A r c ( ^ ) tel que Source(a) = n. Un lien sur un diagramme complet est un zigzag élémentaire maximal entre deux nœuds puits. Définition 5.18 (Lien sur un diagramme complet) Soit un diagramme complet 8 sur CQ. Un lien Z sur 8 est un zigzag élémentaire maximal sur 8 Z ao ai = rao <— rai — > m.2 tel que rao et 77?2 sont des nœuds puits de 8®. L'ensemble des liens d'un diagramme 8 est noté Liens(£). Proposition 5.10 L'ensemble des liens d'un diagramme complet 8 est calculable. Preuve. On calcule l'ensemble des zigzags élémentaires de 8. Cet ensemble est fini. Pour chaque zigzag élémentaire Z ao ai i = rao <— rai — > ra2, on calcule l'ensemble des zigzags Z1 tels que • S(a0)^8(ai) [Z'] • Z' est formé d'une suite de zigzags élémentaires, c'est-à-dire est de la forme Z = n0<— nx —• n 2 . . . nk,_2 <— nk,_x —> nk,, où Vf G { 0 , . . . , y - 1}, n2i <-^- n'2i+l -^½1 n'2i+2 est un zigzag élémentaire. • ViGiO,...,^}, rai ïn\. Le zigzag élémentaire Z\ est alors strictement plus petit que chaque zigzag élémentaire de Z1. Puis on ne conserve que les zigzags élémentaires maximaux entre nœuds puits. O 56 CHAPITRE 5.2.4 5. ISOMORPHISMES ENTRE DIAGRAMMES Forme m i n i m a l e Calculer la forme minimale d'un diagramme complet consiste à ne conserver que les nœuds puits, ainsi que les nœuds et les arcs qui font partie d'un lien du diagramme. Définition 5.19 (Forme minimale) Soit un diagramme complet 8. La forme minimale du diagramme 8 est le diagramme /3 = Minimal (8) défini de la façon suivante. • Graphe /3* : - Nœud(/3^) = {n e Nœud(8®), tel que n est un puits de 8® ou n appartient à un lien de 8®} - Arc(/3$) = {ae Arc(8®), tel que a appartient à un lien de <&*} • Foncteur /3 : /?* -+ CQ. -Vn6 Nœud(/?*), /?(n) = 8{n) ; - VaGArc(/3*), f3{a) = 8{a). Proposition 5.11 Pour tout diagramme complet 8, 8^ Minimal(8). Esquisse de la preuve. Soit (3 = Minimal (8). On définit deux flèches de DIAGR(Co), a : 8 —> /3 et r : /3 —ï 8 telles que â o f % id-n e t f o â » idj. • On définit a : 8 —> (3 de la façon suivante. - Morphisme généralisé de graphes a® : 8® ^-> (3®. • Pour tout nœud n de 8®, tel que n est un nœud puits ou fait partie d'un lien de 8, on pose &®{n) = n. Pour tout autre nœud n de 8®, il existe un nœud puits n1 et un arc an : n —> n' dans 8®. On pose cr^(n) = n'. • Pour tout arc a : n -» n' de 8® qui appartient à un lien de 8, on pose a® (a) = a. Pour tout autre arc a : n —> n' de 8®, n' de 8®, si a appartient à un lien de 8, on a alors évidemment <7n/o£(a) = /3(a)oa n . Si a n'appartient pas à un lien de 8, il existe un zigzag Z tel que onf o 8(a) ~p on [Z]. On pose 0®{a) = Z. • La flèche r : f3 -> 8 est définie de façon évidente. • On a â o f = id-Q. • On vérifie également que r o â de DIAGR(Co) telles que â o f « idp e t r o â » id^ 1. On montre que pour tout nœud puits n de a®, 77i2 de a. On pose no = tr^(rao) et n2 = a $ (ra2). Les nœuds no et n2 sont donc des nœuds puits de /3®, et on a a(ra 0 ) = /3{n0), a{m2) = /3(n 2 ), 0"mo = ^almo)? ^ 2 = ^"0(7712)' On montre qu'il existe un nœud ni dans /3* tel que a(rai) = (3(n\). Enfin, on montre qu'il existe deux arcs 60 ' ^1 -> ^0 e t 61 : ni —» n2 dans (3 tel que a(a0) = /3(60) et a(ax) = /?(&i). 3. Finalement, les diagrammes â et /3 ont donc les mêmes nœuds puits, reliés par les mêmes liens. Les diagrammes â et (3 sont donc identiques. CHAPITRE 58 5. ISOMORPHISMES ENTRE DIAGRAMMES Exemple 5.12 Revenons aux diagrammes 82 et S'. Le diagramme 82 est sous forme minimale ; le diagramme 8f a pour forme minimale le diagramme 82Minimal(82) = 82 ; Minimal^') = 82. Finalement, les diagrammes 82 et 8' sont donc isomorphes. 5.2.5 Algorithme Finalement, un algorithme pour détecter si deux diagrammes sont isomorphes dans la catégorie diagr(C0) consiste à calculer la complétion puis la forme minimale de chaque diagramme, et enfin à comparer les formes minimales. Pour calculer les formes minimales, il est nécessaire de calculer l'ensemble des liens associés à chaque diagramme. Fonction Isomorphe (ÔQ, /3Q : diagramme) : booléen a, j3: diagramme; Début â := Minimal(Complétion(ôô)) ; /3 := Minimal (Complétion(/30)) ; Résultat: â = /3; Fin Isomorphe 5.3 Cas général Dans cette partie, nous examinons les problèmes soulevés lorsque la catégorie CQ est infinie ou contient des cycles. 5.3. CAS 5.3.1 59 GENERAL Zigzags Dans ce paragraphe, nous revenons un instant sur les zigzags. Considérons un diagramme fini 8. Le graphe 8® est fini. Par contre, le nombre de zigzags sur 8® est en général infini. En effet, rien n'interdit de passer plusieurs fois par le même arc. • Si nous considérons un graphe avec une ou plusieurs boucles, il existe évidemment un nombre infini de zigzags sur ce graphe. graphe p® diagramme p(A, f) Nous pouvons en effet considérer les zigzags suivants. oAoAo o A o A o .. • Un diagramme, même s'il est construit sur un graphe sans cycle, contient en général une infinité de zigzags. Considérons par exemple le diagramme W construit sur le graphe TT®. • 1 • •-• a 0 b 2 graphe 7T* - B • A >• 9 • C diagramme 7r Nous pouvons considérer les zigzags suivants. - 0 - 4 2 ^ 0 - H i A o - 4 2 f ^ o A i ^ - 0 ^ 2 De façon générale, il n'existe pas forcément de borne supérieure pour la longueur des zigzags à considérer lorsqu'on veut tester si deux flèches u et v sont connectées, c'est-à-dire s'il existe un zigzag Z tel que u ~y v [Z]. 60 5.3.2 CHAPITRE 5. ISOMORPHISMES ENTRE DIAGRAMMES C a t é g o r i e de base c o m p o r t a n t d e s c y c l e s Nous supposons dans ce paragraphe que la catégorie de base CQ contient des cycles. Remarquons d'abord que la contraction d'un arc identité dans un diagramme peut former des boucles dans le graphe sous-jacent du diagramme, comme dans l'exemple 5.9-3. • : A idA A Si CQ comporte des cycles, l'algorithme présenté en section 5.2 n'est pas correct. En effet, le principal de l'information contenue dans le diagramme n'est plus concentrée dans les nœuds puits. Certains diagrammes, comme p(A, f) n'ont pas de nœud puits. p(A,f) = Si l'ensemble {fn, n G N } est infini, c'est-à-dire si toutes les flèches fn sont différentes, alors on peut ajouter une infinité d'arcs au diagramme. On peut en effet ajouter un arc étiqueté par f2 = / o / , un arc étiqueté par / 3 = / o / o / , etc. Autrement dit, pour tout entier n, les deux diagrammes ci-dessous sont isomorphes. A (M A Par conséquent, si l'ensemble {fn, n G N } est infini, alors la fonction de complétion appliquée sur le diagramme p(A, f) boucle. 5.3.3 C a t é g o r i e de base infinie Lorsque la catégorie de base CQ est infinie, en particulier lorsque CQ comporte un nombre infini de flèches entre deux objets, la procédure qui consiste à ajouter les factorisations à droite peut ne pas s'arrêter, ou, ce qui revient au même, conduire à un diagramme non fini. Exemple 5.13 Soit deux flèches / : A —> C et g : B a une famille indicée par IN (donc infinie) de flèches {hi :A^B, telle que Vt G IN, g o ht; = / . i G IN} C de CQ. Supposons qu'on 5.3. CAS GENERAL 61 C s/ • A V ft " Si on considère un diagramme qui comporte deux arcs a 6 no —> n\ i— n2 étiquetés respectivement par / et g, on peut alors réaliser une infinité de factorisations à droite. Par conséquent, la fonction de complétion boucle. Conclusion 1 Bilan Nous avons proposé un cadre théorique pour étudier les spécifications algébriques modulaires. Nous avons repris une idée classique en spécification algébrique : la composition de spécifications peut être modélisée par des colimites de diagrammes finis. La construction principale est la somme amalgamée qui permet de représenter la composition de deux spécifications en précisant quelles parties sont partagées. Notre travail a consisté à poursuivre cette idée bien connue selon trois directions. • D'un point de vue syntaxique, nous avons défini un langage de termes pour les constructions de colimites finies sur une catégorie de base CQ. Ce langage est défini formellement par la catégorie Terme(Co). • D'un point de vue sémantique, nous avons proposé d'interpréter les termes par des diagrammes finis sur CQ. Cette représentation est plus abstraite que la représentation par des termes car elle permet d'éliminer une partie des choix effectués lors de la construction de la spécification modulaire. • Nous avons défini la notion d'isomorphisme de construction pour les spécifications modulaires. Un isomorphisme de construction entre deux spécifications modulaires correspond à un isomorphisme entre les diagrammes correspondants. Nous avons enfin proposé un algorithme pour détecter si deux diagrammes sont isomorphes, dans le cas particulier où la catégorie de base CQ est finie et ne comporte pas de cycle. Notre travail est articulé en cinq chapitres. 1. Dans le chapitre 1, après quelques rappels sur les spécifications algébriques équationnelles, nous avons présenté plusieurs spécifications modulaires d'anneaux, qui nous ont permis d'introduire la définition d'isomorphisme de construction. Nous avons également précisé le cadre général de notre travail: la théorie des institutions, avec l'hypothèse que la catégorie des spécifications est finiment cocomplète. 2. Dans le chapitre 2, nous avons défini les notions de diagramme et morphisme de diagrammes en utilisant une formulation proche de l'informatique. Notre définition de diagramme est en effet basée sur celle de graphe, et non sur une catégorie quelconque. Nous avons reformulé les définitions de cône et de 63 64 CONCLUSION colimite dans ce cadre. Nous avons défini deux catégories de diagrammes: DIAGR(Co) et diagr(Co). L'intérêt de la catégorie diagr(Co) se situe sur le plan théorique puisque - la catégorie diagr(Co) est finiment cocomplète ; - la catégorie diagr(Co) est une complétion de CQ par colimites finies. La catégorie DIAGR(Co), généralisation de certaines catégories utilisées en informatique — comme celle présentée dans [TBG91] —, est plus concrète que diagr(Co) dans la mesure où elle permet de manipuler les morphismes de diagrammes de façon effective. 3. Le chapitre 3 est consacré à la définition de la précatégorie TERME(Co), qui offre un langage pour les constructions modulaires. Les objets de TERME(Co) sont des termes qui dénotent des spécifications modulaires, et les flèches de TERME(Co) sont des termes qui dénotent des morphismes de spécifications modulaires. Nous proposons une construction stratifiée de cette précatégorie, afin de résoudre le problème de circularité entre la définition des flèches et de l'équivalence dans TERME(Co). On obtient, en passant au quotient, une catégorie Terme(Co). Nous avons montré que - la catégorie Terme(Co) est finiment cocomplète; - la catégorie Terme(Co) est une extension conservatrice de CQ. Enfin, nous avons montré qu'on peut construire une catégorie C(CQ) librement engendrée sur CQ par objet initial choisi et sommes amalgamées choisies. Cette catégorie est obtenue en quotientant TERME(Co) par une congruence sur les objets et flèches de cette précatégorie. 4. Nous proposons dans le chapitre 4 une interprétation des termes représentant des spécifications modulaires par des diagrammes. Cette représentation, qui permet de faire abstraction de certaines étapes particulières choisies pour la construction de la spécification modulaire, est décrite par un préfoncteur V : TERME(Co) -> DIAGR(C0) qui correspond à un foncteur entre les catégories correspondantes V : Terme(Co) -» diagr(C 0 ). Nous avons montré que - le foncteur V définit une équivalence entre les catégories Terme(Co) et diagr(Co) ; - deux objets de Terme(Co) sont isomorphes si et seulement si leurs diagrammes associés sont isomorphes ; - l'interprétation V est correcte, c'est-à-dire qu'une spécification modulaire est isomorphe à la colimite du diagramme qui la représente. CONCLUSION 65 5. La représentation des constructions modulaires par des diagrammes, bien que plus abstraite que celle des termes ne permet pas de détecter immédiatement des isomorphismes de constructions. En effet, deux spécifications modulaires isomorphes sont représentées par des diagrammes qui sont isomorphes, mais pas forcément identiques. Dans le chapitre 5, nous proposons une normalisation des diagrammes, dans le cas particulier où la catégorie des spécifications de base est finie et ne comporte pas de cycle. Ayant montré que deux diagrammes sont isomorphes si et seulement si ils ont la même forme normale, nous disposons donc d'une procédure pour décider si deux diagrammes sont isomorphes. Le formalisme proposé est compositionnel, dans la mesure où des compositions successives de spécifications peuvent être vues comme un assemblage unique. En effet, une suite de constructions de sommes amalgamées est équivalente à la colimite d'un diagramme plus complexe. Cette propriété provient de la structure de monade des précatégories TERME(C 0 ) et DIAGR(C0). Nous espérons avoir montré que la modularité, en particulier le problème des partages entre plusieurs spécifications, est correctement modélisé par les colimites finies. En effet, l'utilisation des colimites permet de faire abstraction d'une part de la définition effective des spécifications et d'autre part des étapes particulières choisies pour la construction d'une spécification modulaire. On peut ainsi se concentrer uniquement sur l'assemblage des différentes spécifications de base. 2 Perspectives Citons quelques voies possibles pour poursuivre ce travail. Contraintes sémantiques De nombreux langages de spécification permettent de préciser des contraintes sémantiques. Un exemple de contrainte sémantique est la persistance d'un foncteur de synthèse entre deux classes d'algèbres. Cette contrainte assure la préservation par exemple d'un module importé, ou encore du paramètre effectif lors d'une instanciation (cf. par exemple [EM85]). Une spécification B qui importe une spécification A est une flèche f : A -+ B. J.-C. Reynaud [Rey90b, Rey93] a proposé de distinguer les flèches auxquelles est associée une contrainte sémantique. Dans notre cadre, l'utilisation de morphismes distingués ne paraît pas suffisante. En effet, comme les deux diagrammes suivants sont isomorphes, l'information d'importation entre A et B est perdue lors du passage à la colimite. • A J -—-• B = [• B Par conséquent, le concept de colimite, qui convient à la modélisation des partages, ne peut pas être appliqué directement pour prendre en considération des contraintes sur des morphismes de spécifications. 66 CONCLUSION Enrichissement et abstraction Deux opérateurs de constructions de spécifications sont fondamentaux en spécification algébrique : Venrichissement, qui permet à partir d'une spécification d'obtenir une nouvelle spécification en ajoutant des sortes et des opérateurs; et Vabstraction, qui permet d'obtenir une nouvelle spécification en supprimant des sortes et des opérateurs. Il semble possible d'étendre le formalisme proposé afin de prendre en compte les enrichissements. Pour nous, un enrichissement d'une spécification modulaire S est une spécification S' accompagnée d'un morphisme de spécifications p : S —» S' qui modélise l'inclusion de 5 dans S'. La spécification S fait partie de Terme(Co), niais pas Sf, ni par conséquent / . Une solution pour permettre d'ajouter de telles flèches est de considérer la catégorie T' qui contient Terme(Co), l'objet S et la flèche / . Ensuite, on considère la sous-catégorie pleine C0 de T' qui a pour objets d'une part l'objet S et d'autre part les objets de CQ. Finalement, la catégorie Terme(Co) contient Terme(Co), ainsi que toutes les constructions qui ont été ajoutées par l'introduction de l'enrichissement Sf. La flèche p : S —• S' appartient bien à la catégorie Terme(Co) car celle-ci a pu être reconstruite à l'aide des flèches up. Le problème de l'abstraction semble plus difficile à résoudre. Dans notre cadre, une abstraction d'une spécification S de Terme(Co) e s t une spécification S' accompagnée d'un morphisme de spécifications q : S' —>• S. Dans ce cas, la construction décrite dans le cas de l'enrichissement ne fonctionne pas, car la flèche q n'appartient pas à la nouvelle catégorie des termes Terme(Co). Une voie de recherche pourrait être ici la prise en considération de colimites distinguées dans la catégorie de base CQ. Colimites distinguées dans CQ En théorie des esquisses [Ehr68, DR94a, DR94b], une esquisse contient des cônes et des cocônes distingués. Le type d'une esquisse correspond à une catégorie librement engendrée par sommes et produits, en conservant les limites et colimites spécifiées. Dans l'état actuel de notre travail, s'il existe par exemple une somme amalgamée dans la catégorie de base CQ, cette somme est "perdue" lors de la construction de la catégorie Terme(Co). Il serait intéressant de généraliser la construction de Terme(Co) de façon à pouvoir conserver certaines colimites. La prise en considération de certaines colimites dans la catégorie de base peut résoudre le problème de l'abstraction. En effet, on peut imaginer ajouter à la catégorie de base la spécification S ainsi que les colimites qui ont permis de construire S, puis d'ajouter S' et le morphisme de spécifications q : S' —> S. On obtient ainsi une catégorie C0, qui contient comme colimites distinguées d'une part les colimites distinguées de CQ, et d'autre part les colimites qui ont permis de construire S. Finalement, la catégorie Terme(Co) contient Terme(Co), Sf, q : S' —> S, ainsi que toutes les constructions qui utilisent Sf. CONCLUSION 67 Généralisation de l'algorithme En ce qui concerne les diagrammes, nous avons proposé un critère pour décider si deux diagrammes sont isomorphes dans diagr(Co). Il resterait à évaluer la complexité de cet algorithme. D'autre part, nous avons supposé que la catégorie des spécifications de base CQ est finie et ne comporte pas de cycle. Cette hypothèse est compatible avec le langage de spécification LPG. Il serait néanmoins intéressant soit de généraliser l'algorithme proposé, soit de montrer l'indécidabilité de ce problème. Application aux langages de spécification et de programmation Notre travail a des retombées pratiques sur le traitement de la modularité dans les langages de spécification et de programmation. Tout d'abord, la somme amalgamée est couramment utilisée dans les langages de spécification algébrique ; par contre les flèches "up", à part dans le langage LPG, sont ignorées. D'un point de vue théorique, cela implique que les catégories considérées ne sont pas finiment cocomplètes. D'un point de vue pratique, cela signifie qu'on ne peut pas modéliser toutes les compositions de spécifications, en particulier certains assemblages décrits dans le chapitre 1 sur l'exemple des anneaux. D'autre part, le langage de termes proposé, qui permet de coder finement les assemblages de modules, a l'avantage d'introduire une gestion explicite des partages entre spécifications. Remarquons également que l'instanciation des modules génériques peut être traitée de façon uniforme dans le même cadre. Ces éléments doivent permettre de définir, pour les langages de la prochaine génération, un concept de modularité plus général et bien fondé d'un point de vue théorique. Réutilisation Enfin, le formalisme que nous avons proposé peut également être appliqué à la réutilisation de programmes. On suppose que l'on dispose d'une bibliothèque de spécifications de base, accompagnées de différentes implantations. Comme il peut être nécessaire d'implanter une même spécification de façons différentes dans diverses parties du programme, par exemple pour des raisons d'efficacité, cette bibliothèque doit contenir différentes implantations pour chaque spécification de base. D'autre part, cette bibliothèque peut également contenir des implantations de spécifications modulaires construites sur les spécifications de base. L'objectif est d'implanter une nouvelle spécification modulaire, en réutilisant au mieux les implantations disponibles. Si cette spécification est isomorphe à une construction déjà implantée, on peut bien évidemment réutiliser cette implantation. De façon plus générale, il s'agit de détecter les implantations réutilisables et les spécifications qui restent à implanter, et, parallèlement, les contraintes posées sur ces implantations par les partages entre les spécifications de base utilisées. L'idée est d'extraire des informations du diagramme associé à la spécification modulaire à implanter, ce diagramme pouvant être considéré comme le degré de liberté dont on dispose pour coder les spécifications de base. 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/manJLpg. dvi. [BBC86] 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 ageneric, 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. 69 70 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. [BW85] 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. [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. [Ehr68] C. Ehresmann. Esquisses et types de structures algébriques. Bulletin de l'Institut Polytechnique, Iasi 14, 1968. Science. RÉFÉRENCES BIBLIOGRAPHIQUES 71 [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. Principles 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. [GTW78] 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. 72 RÉFÉRENCES BIBLIOGRAPHIQUES [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 k 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-ll(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. [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. PhD fondamentales. Springer- RÉFÉRENCES BIBLIOGRAPHIQUES 73 [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 DISCOJ90, 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 18th 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. [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. 74 RÉFÉRENCES BIBLIOGRAPHIQUES [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 troisiè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 4 Sémantique : des termes aux diagrammes 4.1 Sémantique 4.1.1 Précatégorie DIAGR(Co) 4.1.2 Préfoncteur V : TERME(C 0 ) -> DIAGR(C0) 4.2 Exemple des anneaux 4.2.1 Diagramme associé à la spécification A2 4.2.2 Diagramme associé à la spécification A!2 4.2.3 Diagramme associé à la spécification As 4.2.4 Diagramme associé à la spécification A4 4.3 Equivalence entre les catégories Terme(Co) et diagr(Co) 4.3.1 Équivalence entre catégories, équivalence entre précatégories . 4.3.2 Équivalence entre les précatégories DIAGR(C0) et TERME(C 0 ) 4.3.3 Correction du calcul de diagrammes 4.4 Conclusion 13 13 13 16 17 17 19 20 23 26 27 27 32 33 5 Isomorphismes entre diagrammes 5.1 Transformations de diagrammes 5.1.1 Substitution par objet isomorphe 5.1.2 Suppression d'un arc 5.1.3 Ajout d'un arc étiqueté 5.1.4 Contraction d'un arc identité 5.2 Catégorie CQ finie et sans cycle 5.2.1 Hypothèses 5.2.2 Fonction de complétion 5.2.3 Zigzags élémentaires et liens 5.2.4 Forme minimale 5.2.5 Algorithme 35 35 36 38 42 45 48 48 49 52 56 58 75 76 TABLE DE LA TROISIEME PARTIE 5.3 Cas général 5.3.1 Zigzags 5.3.2 Catégorie de base comportant des cycles 5.3.3 Catégorie de base infinie 58 59 60 60 Conclusion 1 Bilan 2 Perspectives 63 63 65 Références bibliographiques 69 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