Catherine Oriat.
Étude des spécifications modulaires :
constructions de colimites finies, diagrammes, isomorphismes.
Thèse de doctorat, INPG, Grenoble, Janvier 1996.
Résumé
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 de'finissons une cate'gorie de diagrammes ``concre`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 spe'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 specifications
can be modeled, in a category
theoretic framework, by means of colimits of diagrams.
Pushouts in particular allow us to gather two specifications
sharing a common part. Our work extends this classic
idea along three lines.
From a syntactic point of view, we define a language to
represent modular specifications built from a category
of base specifications and base specification morphisms.
This language is formally characterized by a finitely
cocomplete category of terms.
From a semantic point of view, we propose to associate
with each term a diagram. This interpretation
allows us to abstract some choices made while
constructing a modular specification.
We thus define a ``concrete'' 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 equivalence between the category of terms and
the category of diagrams, which shows
the soundness of this interpretation.
At last, we propose an algorithm to decide whether
two diagrams are isomorphic, when the base category is finite and cycle free.
This allows us to detect ``construction isomorphisms''
between modular specifications, i.e. isomorphisms which do not depend on the
base specifications, but only on their combination.
Publications