Catherine Oriat.
Detecting equivalence of modular specifications with categorical
diagrams.
Theoretical Computer Science 247 (2000) 141-190.
Abstract
The composition of modular specifications can be modeled, in a category
theoretic framework, by colimits of diagrams. Pushouts in particular
describe the combination of two specifications sharing a common part.
In this paper, we propose to represent the combination of modular
specification as diagrams.
First, we define
a term language to represent modular specifications built
with colimit constructions over a category of base specifications.
Then, we propose to associate with each term a diagram.
This interpretation provides us with a more abstract representation
of modular specifications because irrelevant steps of the
construction are eliminated.
Finally, we propose an algorithm to normalize diagrams, in the case
when the base category is skeletal, finite and cycle free. This allows
us to detect ``construction isomorphisms'' between modular specifications,
i.e. isomorphisms which do not depend on the semantics of the base
specifications, but only on their combination.
Publications