Theory and Applications of Categories, Vol. 1, No. 8, 1995, pp. 156–173.

CATEGORICAL DATA-SPECIFICATIONS

FRANK PIESSENS AND ERIC STEEGMANS

Transmitted by Jiri Rosicky

ABSTRACT. We introduce MD-sketches, which are a particular kind of Finite Sum sketches. Two interesting results about MD-sketches are proved. First, we show that, given two MD-sketches, it is algorithmically decidable whether their model categories are equivalent. Next we show that data-specifications, as used in database-design and software engineering, can be translated to MD-sketches. As a corollary, we obtain that equivalence of data-specifications is decidable.

1. Introduction

This paper is about the correspondence between two kinds of specification mechanisms: sketches and data-specifications.

Sketches were invented by Charles Ehresmann in the late sixties, for the purpose of specifying algebraic structures. Since then, they have been studied intensively. An outline of the theory of sketches, with a large number of references, can be found in [17]. It is well-known that the categories of models of sketches (in Set) are exactly the accessible categories. An accessible category is complete iff it is the model category of a Limit sketch iff it is a locally presentable category. Locally presentable categories have the pleasant property that it is possible to define a canonical Limit sketch with the given category as model category. All these results can be found in [2]. For other accessible categories, it is not possible to define a canonical sketch with the given category as model category. In a number of recent papers ([3, 4]), various equivalence preserving transformations between sketches are studied. These transformations preserve (up to equivalence) the model category in Set, but do not necessarily preserve model categories in other categories than Set. Hence, it is clear that model categories in Set do not determine the sketch in the same way as this is the case for Limit sketches. In this paper we are interested in algorithmic decidability of the equivalence problem, and we will prove that the equivalence problem is decidable for the class of MD-sketches.

Semantic data-specifications like Chen’s Entity-Relationship diagrams ([10]) on the other hand, have been used for many years in the early stages of database design. However, most specification systems used in practice are of an informal nature, and have little or no mathematical foundation. This makes it impossible to prove interesting results about them. [13] formalized these specification systems using categorical language, and proved a first interesting result: the existence of so-called canonical forms for a large subset of data-specifications. Other categorical formalisations of semantic data-specifications exist.

The first author is a Research Assistant of the Belgian Fund for Scientific Research

Received by the editors 19 June 1995.

Published on 2 November 1995

1991 Mathematics Subject Classification : 18A25, 18C99, 68P15.

Key words and phrases: data-specifications, sketches.

\begin{matrix}c \\ ◯ \end{matrix} Frank Piessens and Eric Steegmans 1995. Permission to copy for private use granted.

[9] and [11] propose generalized sketches in the sense of [12] as a formalisation for dataspecifications. In [15], object-oriented data-specification systems based on categorical constructs are defined, and a query language based on universal constructions is shown to be at least as expressive as relational algebra.

The structure of this paper is as follows:

First, in section 2, we introduce a special kind of Finite Sum sketch ([5]), in which you can only specify certain monicity and disjointness constraints. This kind of sketch is called an MD-sketch. The main result about MD-sketches is that equivalence of the model-categories of two MD-sketches is decidable.

In section 3 we define data-specifications, and their model-categories. Our definition is equivalent to the definition of specification with attributes in [13]. If the modelcategories of two different data-specifications are equivalent, this means that they are different formalizations of the same real world situation. Recognizing that two different data-specifications are equivalent is very important when one tries to integrate a number of data-specifications into one large data-specification. Hence, it would be interesting to have an algorithm to decide equivalence of data-specifications.

In section 4, we show that data-specifications can be translated to MD-sketches, and as a corollary, we obtain that equivalence of data-specifications is decidable. Combining the translation algorithm with the algorithm to decide equivalence of MD-sketches gives us an algorithm to decide equivalence of data-specifications.

1.1. Acknowledgments. We want to thank Francis Borceux for a number of very clarifying discussions about accessible categories and about Kan-extensions, and Jiří Rosický for a very interesting discussion about the equivalence problem for sketches when one considers models in Set or in FinSet. We also want to thank Dominic Verity, Roy Crole and all the other readers of the categories mailing list who took the time and effort to answer our questions about discrete opfibrations.

2. MD-sketches

An MD-sketch is a peculiar kind of Finite Sum sketch. MD-sketches are interesting because equivalence of their model categories is algorithmically decidable (theorem 2.18), and yet they have sufficient expressive power to allow for a translation of data-specifica-tions to MD-sketches (theorem 4.3).

2.1. Preliminary Definitions.

2.2. Definition. A (finite) source in a category C is a pair (X, (f_{i})_{i∈I}) consisting of an object X of C and a family of morphisms f_{i} : X → Y_{i} of C, indexed by some (finite) set I.

In this paper, we only consider finite sources, and we will take the unqualified word “source” to mean finite source. We will use the notations (X, (f_{i})_{i∈I}) and f_{i} : X → Y_{i} interchangeably. A source (X, (f_{i})_{i∈I}) is a mono-source if f_{i} ∘ x = f_{i} ∘ y for all i ∈ I implies that x = y. The base of a source f_{i} : X → Y_{i} is the indexed family of objects Y_{i}. Hence, the base of a source is a discrete diagram.

These definitions of source and mono-source in a category are standard, and can be found for instance in [1].

2.3. Definition. A double-source in a category C is a pair of two sources f_{i} : X → Y_{i} and g_{i} : Z → Y_{i} in C, on the same base.

A double-source (f_{i}, g_{i}) looks like this:

[figure: Y_{1}; X; f_{1}; f_{n}; ⋮; Z; g_{1}; g_{n}; Y_{n}]

We say that a double-source (f_{i}, g_{i}) is disjoint, iff the limit of the diagram above is the initial object. In FinSet, the category of finite sets and functions, this means that there are no elements x ∈ X and z ∈ Z such that f_{i}(x) = g_{i}(z) for all i.

2.4. Definition. An MD-sketch is a triple (C, M, D) where C is a finite category, M is a finite set of sources in C, D is a finite set of double-sources in C.

2.5. Definition. A model of an MD-sketch (C, M, D) is a functor from C to FinSet, which takes every source in M to a mono-source and every double-source in D to a disjoint double-source.

A source μ will sometimes be called a monicity condition. A monicity condition μ is satisfied by a functor F iff F takes μ to a mono-source. In a similar way, a double-source δ will sometimes be called a disjointness condition, and a disjointness condition δ is satisfied by a functor F iff F takes δ to a disjoint double-source.

The model-category of an MD-sketch, denoted Mod(C, M, D) is the full subcategory of Fun(C, FinSet) containing only the models. We use the notation Mod(C, M) to denote the full subcategory of Fun(C, FinSet) consisting of all those functors that take all sources in M to mono-sources (but do not necessarily satisfy the disjointness conditions).

2.6. Remark. It should be obvious that an MD-sketch is a restricted kind of Finite Sum sketch ([5]). The requirement that a source must be mono can be stated by requiring a certain cone to be a limit cone. To state the disjointness conditions, you add a new object to C, and an arrow from the new object to every object of C. Then a disjointness condition can be stated by requiring the new object to be initial, and by requiring that the limit of the double-source is this new object.

We could consider models of MD-sketches in other categories than FinSet. However, for the application that we have in mind (data-specifications), only models in FinSet are needed. Therefore, we restrict our attention to models in FinSet.

Example. We give an example to show that model categories of MD-sketches are not necessarily finitely complete. Since model categories of Finite Limit sketches are always finitely complete, it follows that an MD-sketch is not a restricted kind of Finite Limit sketch. Consider the following MD-sketch:

C = [figure: X; f; Y; g; Z] , M = ∅, D = {(f, g)}

(Only the non-identity arrows of the category C are drawn). Models of this MD-sketch are functors F : C → FinSet such that the images of F f and F g are disjoint. It is easy to see that the category of models does not have a terminal object.

2.7. Properties of MD-Sketches.

2.8. Lemma. Mod(C, M) is an epi-reflective subcategory of Fun(C, FinSet). Moreover, there exists an algorithm to compute the reflection of a functor F : C → FinSet.

The algorithm to compute the reflection is given in the proof below.

Proof. The construction of the reflection of a functor F is as follows:

1. Define a relation R on the elements of F where xRy iff there exists some source f_{i} : X → Y_{i} ∈ M such that F f_{i}(x) = F f_{i}(y) for all i.

2. Construct the smallest congruence relation on the elements of F, containing R.

3. Take the quotient of F by this congruence relation.

The universal arrow from F to its reflection is the projection of F on this quotient. We leave the verification to the reader.

Hence, we have the following situation:

[figure: Fun(C, FinSet); R; Mod(C, M); I; Mod(C, M, D); J]  (1)

where I and J are inclusions and R is left adjoint to I.

2.9. Lemma. Suppose F is in the range of J (i.e. F = J(G) for some G), and suppose there exists a morphism α : F′ → F in Mod(C, M), then F′ is also in the range of J.

Proof. Suppose F′ is not in the range of J. This means that there exists a disjointness condition (f_{i} : X → Y_{i}, g_{i} : Z → Y_{i}) in D which is not satisfied by F′. Hence, there exists elements x′ ∈ F′(X) and z′ ∈ F′(Z) such that F′(f_{i})(x′) = F′(g_{i})(z′) for all i. But then, let x = α_{X}(x′) and z = α_{Z}(z′), and we find that F (f_{i})(x) = F (g_{i})(z) for all i. As a consequence, the disjointness condition (f_{i}, g_{i}) is not satisfied by F and F cannot be in the range of J. Contradiction.

2.10. Lemma. J preserves and reflects colimits.

Proof. Since J is full and faithfull, it is obvious that it reflects colimits. To prove that it preserves colimits, consider a diagram D in Mod(C, M, D), and suppose it has a colimit (L, ι). We must prove that the colimit of J(D) is (J(L), J(ι)). Since Mod(C, M) is cocomplete, J(D) must have a colimit (L′, ι′). By the universal property of the colimit, we find an arrow α : L′ → J(L) such that α ∘ ι′ = J(ι). But, by the previous lemma, this means that L′ is in the range of J. Since J reflects colimits, we conclude that L′ and J(L) are isomorphic.

2.11. Definition. An MD-sketch (C, M, D) is normal, or is in normal form, if all the representable functors from C are models.

2.12. Lemma. For every MD-sketch, there exists a normal MD-sketch with an equivalent model category. Moreover, there exists an algorithm to compute such a normal MD-sketch.

An algorithm to compute an equivalent normal MD-sketch is contained in the proof below.

Proof. Suppose an MD-sketch (C, M, D) is given. Consider diagram (1), and let η be the unit of the adjunction (R, I). We define a congruence relation on the arrows of C in the following way:

f ∼ g iff η_{Hom(C,−)}(f) = η_{Hom(C,−)}(g)

with C the source of f and g. Let C′ be C/ ∼ and let P : C → C/ ∼ be the projection. Since Nat(Hom(C, −), IM) = Nat(IRHom(C, −), IM), we can conclude that the arrows that are identified by ∼ must be taken to the same function in every model. Define M′ to be {P (μ) | μ ∈ M} and D′ to be {P (δ) | δ ∈ D}. It is easy to verify that Mod(C, M, D) is equivalent to Mod(C′, M′, D′), and that all representable functors from C′ satisfy all the monicity conditions in M′.

Next, suppose that Hom(C′, −) does not satisfy a disjointness condition δ in D′. By lemma 2.9, it follows that all models of (C′, M′, D′) must take C′ to the empty set. Hence, Mod(C′, M′, D′) is equivalent to Mod(C′′, M′′, D′′) with:

• C′′ is the full subcategory of C′ containing all the objects X for which Hom(X, −) is a model of (C′, M′, D′).

• M′′ = {f_{i} : X → Y_{i} ∈ M′ | X ∈ C′′}

• D′′ = {(f_{i} : X → Y_{i}, g_{i} : Z → Y_{i}) ∈ D′ | X ∈ C′′ and Z ∈ C′′}

It is easy to verify that (C′′, M′′, D′′) is normal, and that its model category is equivalent to that of (C′, M′, D′), and hence to that of (C, M, D).

Since C is a finite category, all these constructions are clearly computable.

Example. Consider the following MD-sketch:

C = [figure: B; f; C; i; D; A; g; h] , M = {i}, D = {(f, f)}

with i ∘ h = i ∘ g. It is clear that Hom(A, −) does not satisfy the monicity conditions, since Hom(A, i) is not an injective function. The first part of the construction given in the previous proof gives us:

C′ = [figure: B; f; C; i; D; A; g] , M′ = {i}, D′ = {(f, f)}

Hom(B, −) does not satisfy the disjointness condition. Applying the second part of the construction in the previous proof leads to:

C′′ = [figure: A; g; C; i; D] , M′′ = {i}, D′′ = {}

2.13. Proposition. Let (C, M, D) be a normal MD-sketch and let μ = (f_{i} : X → Y_{i}) be a finite source in C, then it is decidable whether μ is taken to a mono-source in every model of (C, M, D).

An effective decision procedure is contained in the proof below.

Proof. Suppose that μ is taken to a mono-source by every functor in Mod(C, M, D). Then we have the following situation:

[figure: Mod(C, M); Mod(C, M ∪ {μ}); J′; Mod(C, M, D); J′′]

where J = J′ ∘ J′′ preserves colimits (by lemma 2.10), and where J′ and J′′ are full inclusions, and hence reflect colimits.

Consider the following diagram in Mod(C, M ∪ {μ}):

[figure: Hom(Y_{1}, −); Hom(f_{1},−); Hom(f_{1},−); Hom(X, −); ⋮; Hom(X, −); Hom(Y_{n}, −); Hom(f_{n},−); Hom(f_{n},−)]

Its colimit is Hom(X, −). But since J′′ reflects and J′ ∘ J′′ preserves this colimit, the colimit of this diagram in Mod(C, M) is also Hom(X, −).

Conversely, if the colimit of that diagram in Mod(C, M) is Hom(X, −), it follows easily that μ will be taken to a mono-source by every functor of Mod(C, M, D).

Hence, we can decide whether μ is taken to a mono-source in every model by computing the colimit of the diagram above in Mod(C, M), and checking if this colimit is naturally isomorphic to Hom(X, −).

Since colimits of finite diagrams in Mod(C, M) are computable (first compute the colimit in Fun(C, FinSet) and then compute the reflection of this colimit along the inclusion), the result follows.

2.14. Proposition. Let (C, M, D) be a normal MD-sketch and let δ = (f_{i}, g_{i}) be a finite double-source in C, then it is decidable whether δ is taken to a disjoint double-source in every model of (C, M, D).

Again, an effective decision procedure is contained in the proof below.

Proof. Let (F, ι) be the colimit of the following diagram in Mod(C, M):

[figure: Hom(Y_{1}, −); Hom(f_{1},−); Hom(g_{1},−); Hom(X, −); ⋮; Hom(Z, −); Hom(Y_{n}, −); Hom(f_{n},−); Hom(g_{n},−)]

Suppose F satisfies all disjointness conditions in D. Then F is a model which does not satisfy δ, and hence δ is not satisfied in all models of (C, M, D).

Suppose F does not satisfy all disjointness conditions in D. Given any functor F′ which does not satisfy δ, we can easily construct a commutative cocone on the above diagram into F′, and hence an arrow α : F → F′. By lemma 2.9, F′ can not be a model. Hence, all models of (C, M, D) satisfy δ.

Hence, we can decide whether δ is satisfied in all models by computing the colimit of the above diagram in Mod(C, M), and checking whether all disjointness conditions in D are satisfied in the vertex of this colimit.

Recall that a category is skeletal iff no two distinct object are isomorphic, and that it is Cauchy-complete iff every idempotent arrow is split ([7, 8]).

2.15. Lemma. For every normal MD-sketch (C, M, D), there exists an equivalent normal MD-sketch (C′, M′, D′) where C′ is skeletal and Cauchy-complete. Moreover, there exists an algorithm to compute such an equivalent MD-sketch.

The proof below describes an algorithm to compute an equivalent skeletal, Cauchycomplete normal MD-sketch.

Proof. Let C′ be the skeleton of the Cauchy-completion of C, and consider the functor p ∘ i where p is the projection on the skeleton and i is the injection in the Cauchycompletion ([7]). Let M′ = {p(i(μ)) | μ ∈ M} and let D′ = {p(i(δ)) | δ ∈ D}. It is easy to verify that Mod(C, M, D) and Mod(C′, M′, D′) are equivalent, and that (C′, M′, D′) will be normal if (C, M, D) was normal. Again, since C is finite, it is clear that this construction is computable.

2.16. Lemma. Every model M : C → FinSet of a normal MD-sketch (C, M, D) is a colimit of representable models.

Proof. It is well-known that every object in Fun(C, FinSet) is a colimit of representable functors ([8]). Moreover, we know that all the representable functors are models (since (C, M, D) is normal). From this and the fact that the inclusion of the model-category in Fun(C, FinSet) reflects colimits (since it is full and faithful), the result follows.

2.17. Lemma. Let (C, M, D) be a normal MD-sketch with C Cauchy-complete, then the following are equivalent:

1. M is a representable model.

2. The arrows ϵ : colimNat(M, D) → Nat(M, colimD), induced by the universality of the colimit, are epis for every diagram D in Mod(C, M, D) for which the colimit exists.

Proof. First we show that representable models have property 2. Let H be a Homfunctor. H belongs to the model-category since the given MD-sketch is normal. Consider again diagram 1. Let η be the unit of the adjunction (R, I). Since Mod(C, M) is an epi-reflective subcategory (lemma 2.8), every η_{X} is epi.

Nat(H, colimD) = Nat(IJH, IJcolimD) (since I ∘ J is full and faithfull)
= Nat(IJH, IcolimJD) (J preserves colimits)
= Nat(IJH, η_{colimIJD} ∘ colimIJD)
= Nat(IJH, η_{colimIJD}) ∘ Nat(IJH, colimIJD)
= Nat(IJH, η_{colimIJD}) ∘ colimNat(IJH, IJD)
= Nat(IJH, η_{colimIJD}) ∘ colimNat(H, D)

(For the third equality, see the computation of colimits in epi-reflective subcategories in [1]) Since η_{colimIJD} is epi, and since Nat(IJH, −) preserves epis, we conclude that H has property 2.

Secondly, suppose that M has property 2. We know from lemma 2.16 that M = colimD where all objects from D are representable models. Let β : D → M be the colimiting cocone. We have the following commutative diagram:

[figure: colimNat(M, D); ϵ; Nat(M, M); Nat(M, D); ι; Nat(M,β)]

with ϵ an epi. So some object H of Nat(M, D) contains an α such that β_{H} ∘ α = Id_{M}. Hence, M is a splitting of an idempotent of a representable model H. But since every idempotent in C is split, M must be a representable model.

2.18. Theorem. Equivalence of MD-sketches is decidable.

An algorithm to decide equivalence is given in the proof.

Proof. Suppose we are given two MD-sketches (C, M, D) and (C′, M′, D′). We may assume that both MD-sketches are normal and that C and C′ are skeletal and Cauchycomplete, by lemmas 2.12 and 2.15. We claim that the two sketches are equivalent iff there exists an isomorphism i : C → C′ such that

1. for each μ ∈ M and for each δ ∈ D, i(μ) is a mono-source in every model of (C′, M′, D′) and i(δ) is a disjoint double-source in every model of (C′, M′, D′).

2. for each μ′ ∈ M′ and for each δ′ ∈ D′, i^{−1}(μ′) is a mono-source in every model of (C, M, D) and i^{−1}(δ′) is a disjoint double-source in every model of (C, M, D).

Since C and C′ are finite, we can enumerate all isomorphisms between them, and hence, by propositions 2.13 and 2.14, it follows that equivalence is decidable.

It remains to prove that the condition above is indeed a sufficient and necessary condition for equivalence. It is obvious that the condition is sufficient. We prove that it is necessary. Suppose we have an equivalence between the two model-categories. Since the property mentioned in lemma 2.17 is clearly preserved by equivalence, we know that the equivalence maps representable models to representable models. By the Yoneda lemma and the fact that C and C′ are skeletal, we conclude that the equivalence between the model-categories induces an isomorphism between C and C′. It is easy to verify that this isomorphism satisfies the two conditions mentioned above.

3. Data-Specifications

3.1. Definition and Examples.

3.2. Definition. A data-specification is a triple (S, M, A), where

1. S is a finite category.

2. M is a finite set of sources in S.

3. A : S_{0} → FinSet is a functor, where S_{0} is the discrete category whose set of objects is the set of objects of S.

Essentially, A is just a function from the objects of S to the class of finite sets.

3.3. Definition. A model of a data-specification (S, M, A) is a pair (M, λ), where

1. M : S → FinSet is a functor taking every μ ∈ M to a mono-source.

2. λ : M ∘ I → A is a natural transformation, where I : S_{0} → S is the inclusion.

The following examples are taken from [13]. The category S of the specification is often given as a graph G, and a set E of equations. The category S is defined to be the free category on G, divided by the congruence generated by the equations in E. We begin with a few examples for which the functor A is the constant functor on 1, the terminal set. Such data-specifications are in fact the same as MD-sketches with an empty set of disjointness conditions.

Example. If S is a discrete category (no non-identity arrows), the models are just typed sets. Let S be the discrete category with two objects (call them COMPUTER and PRINTER) and no arrows, and let M be empty. This specification says that the part of the world we want to specify consists of two kinds of entities (computers and printers), and that is all it says.

Example. Arrows in the category specify existential dependencies. Consider for instance:

G = [figure: COMPUTER; l; LOCATION] , E = ∅, M = ∅

Since the arrow must be taken to a function in a model, this specifies that every computer must have a location associated with it. (An entity of type COMPUTER is always associated with an entity of type LOCATION.)

Example. A source with n arrows in the category can be seen as an n-ary multirelation:

G = [figure: CONNECTION; c; p; COMPUTER; PRINTER] , E = ∅, M = ∅

This specification says that connection is a multirelation between computers and printers: every entity of type CONNECTION is associated with a couple of entities (x, y) with x of type COMPUTER and y of type PRINTER. It is possible that two different entities of type CONNECTION are associated with the same couple. Hence CONNECTION is a multi-relation over COMPUTER and PRINTER. For example, a printer could be connected twice to a computer, once with a serial cable, and once with a parallel cable. Example. A multi-relation is an ordinary relation (no duplicates allowed) if and only if the corresponding source is a mono-source. The specification:

G = [figure: CONNECTION; c; p; COMPUTER; PRINTER] , E = ∅, M = {(CONNECTION,(c,p))}

says that CONNECTION is an ordinary relation over COMPUTER and PRINTER. A printer can be connected only once to a computer. Example. By requiring certain equations to be valid in S, we can express equality constraints:

G = [figure: CONNECTION; c; p; COMPUTER; l_{1}; PRINTER; l_{2}; LOCATION] , E = {l_{2} ∘ p = l_{1} ∘ c}, M = ∅

This specification says that computers and printers can be connected only if they have the same location. This kind of constraint occurs very often in practice.

In the examples we have discussed up to now, the functor A was always the constant functor 1. A data-specification with A = 1 only specifies the types of entities that exist in the part of the world we want to specify, and some structural constraints (e.g. a computer is always associated with a location, a printer can only be connected to a computer if they share the same location). In a database, we also want to store attributes of the entities. For example, for a printer, we might want to store whether it is a laserprinter or a matrixprinter, and for a computer, we might want to store the type of its processor, or its amount of memory. With the functor A, we specify for each type of entity (each node of S) the set of attribute values that entities of that type can have. Looking at the definition of a model of a data-specification, it is easy to see that in every model M, all entities of type C (i.e. all elements of the set M(C)) will be labelled with an element of A(C). The function which takes each entity to its label is the component of the natural transformation λ at C.

Example. Consider for example:

G = [figure: CONNECTION; c; p; COMPUTER; l_{1}; PRINTER; l_{2}; { matrix, laser }; LOCATION]  (2)

E = {l_{1} ∘ c = l_{2} ∘ p}, M = {(CONNECTION, (c, p)}

The functor A is defined on the figure, using dotted lines: if there is a dotted line from a node of the graph to a finite set, then this defines the functor A for that node. For example: A(PRINTER) is the set { matrix, laser}. If there is no dotted line from a given node n in the graph, then A(n) is defined to be the terminal set. In a model of this specification, every entity of type PRINTER will be labelled with a value from the set { matrix, laser }. In a similar way, we could have labelled computers with their type of processor, and connections with their data-transmission speed. However, remember that attribute sets must be finite sets.

With these examples in mind, it should be clear that data-specifications provide for an intuitive way to specify the structure of a database. The last example, for instance specifies a (small) database, containing information about the hardware equipment of a company. A model (M, λ) of this data-specification is a possible instance of the database. The functor M indicates how many entities of each type exist, and how they are related to each other. The natural transformation λ gives an attribute value for each entity.

In fact, the most widely used data-specification mechanisms, namely those based on Entity-Relationship diagrams ([10]), are very close to our data-specifications. For more details on how to convert Entity-Relationship diagrams to our data-specifications, consult [13]. That Entity-Relationship diagrams are of major importance in database design can be judged from the fact that an annual international conference on the Entity-Relationship Approach has been organized since 1981. Almost any introductory book on database design includes examples of Entity-Relationship diagrams (see for instance [14] or [16]). Since these diagrams can be reformulated as categorical data-specifications, we refrain from giving more extended examples in this paper, referring the reader to books like [14] and [16] instead.

3.4. Definition. A homomorphism between two models (M, λ) and (M′, λ′) of a dataspecification (S, M, A) is a natural transformation α : M → M′ such that λ′ ∘ αI = λ.

In other words, it is a natural transformation between M and M′ that is compatible with the labelling.

Models and homomorphisms of models of a specification F = (S, M, A) form a category, the model category of F, which is denoted as Mod(F). Let I : S_{0} → S be the inclusion, let I^{∗} : Fun(S, FinSet) → Fun(S_{0}, FinSet) be the functor of composition with I and let \overline{A} : 1 → Fun(S_{0}, FinSet) be the functor picking out A. Then, 3.5. Lemma. Mod(F) is a full subcategory of the comma-category (I^{∗} ↓ \overline{A}).

The proof of this lemma is trivial. An object (F, α) of (I^{∗} ↓ \overline{A}) belongs to Mod(F) iff the functor F takes all sources in M to mono-sources.

3.6. Lemma. Let A^{!} : S → FinSet be the right Kan extension of A along I. (I^{∗} ↓ \overline{A}) is isomorphic to Fun(S, FinSet)/A^{!}.

Proof. First, note that the right Kan extension exists, since S is a finite category, and FinSet is finitely complete. ¿From the universal property of the right Kan extension, we get the natural isomorphism:

Nat(I^{∗}(F), A) ≈ Nat(F, A^{!})  (3)

Objects of (I^{∗} ↓ \overline{A}) are couples (F, λ) with F : S → FinSet a functor and λ : I^{∗}(F) → A a natural transformation. Objects of Fun(S, FinSet)/A^{!} are couples (F, \overline{λ}) with F : S → FinSet a functor and \overline{λ} : F → A^{!} a natural transformation. By (3), there is a bijection between the objects of both categories.

Arrows in both categories are natural transformations α. In (I^{∗} ↓ \overline{A}) they must satisfy commutativity of:

[figure: I^{∗}(F_{1}); I^{∗}(α); λ_{1}; A; I^{∗}(F_{2}); λ_{2}]

In Fun(S, FinSet)/A^{!} they must satisfy commutativity of:

[figure: F_{1}; α; _{\overline{λ}_{1}}; A^{!}; F_{2}; _{\overline{λ}_{2}}]

However by the naturality in F of (3), these two conditions are equivalent, and hence (I^{∗} ↓ \overline{A}) and Fun(S, FinSet)/A^{!} are isomorphic.

3.7. Equivalence of Data-Specifications. We say that two data-specifications are equivalent iff their model-categories are equivalent. What we want to find is an algorithm to decide equivalence of data-specifications. Our approach will be to translate dataspecifications to MD-sketches and then apply theorem 2.18. But first we give an example of equivalent data-specifications.

Example. The following specification is equivalent to specification (2).

G = [figure: M-CONNECTION; m; c_{1}; L-CONNECTION; c_{2}; l_{1}; MATRIXPRINTER; l_{2}; COMPUTER; l_{3}; LASERPRINTER; l_{4}; LOCATION]  (4)

E = {l_{2} ∘ m = l_{3} ∘ c_{1}, l_{3} ∘ c_{2} = l_{4} ∘ l_{1}}
M = {(M-CONNECTION, (m, c_{1})), (L-CONNECTION, (c_{2}, l_{1}))}

Informally, it is not too hard to see that the two specifications are semantically equivalent. In the specification above, two different entity types are used for matrix-printers and laserprinters, instead of one entity type with an attribute. Further in this paper, we will prove that the model-categories are indeed equivalent.

The fact that the same real-world situation can be specified in a number of nonisomorphic ways is an important problem in database design and software engineering. Suppose for example, that a number of different data-specifications exist, and that these different specifications overlap partly: certain parts of the real world are specified in more than one of the specifications. It is very likely that these parts are specified differently in each of the specifications, and that makes it hard to combine the given specifications into one large specification. This problem of combining data-specifications is called the view integration problem in the database literature, and has been studied extensively. We refer the reader to [6] for a survey. The usual approach is to develop heuristic algorithms which try to identify the equivalent subspecifications, and then leave it to a database designer to decide which subspecifications are indeed equivalent and which are not. A provably correct algorithm (in contrast with a heuristic algorithm) could minimize the amount of work that is left to the database designer. In the sequel of this paper, we will develop such an algorithm, by giving a constructive proof of the decidability of equivalence of data-specifications.

4. Translating data-specifications to MD-sketches

In this section we show that, given an arbitrary data-specification, we can compute an MD-sketch with an equivalent model-category. Since we can decide equivalence of MDsketches, as a corollary, we find that we can decide equivalence of data-specifications.

4.1. Set-valued functors and discrete opfibrations. It is well-known that the category Fun(C, FinSet) is equivalent with the category FinDof(C) of finite discrete opfibrations over C. (See for instance [5] for a description of the equivalence)

Suppose F : C → FinSet is the functor corresponding to a discrete opfibration (dof) Ψ : E → C under this equivalence. In this section, we investigate under what conditions (for Ψ) the functor F takes a source μ to a mono-source, or a double-source δ to a disjoint double-source.

Let μ = (f_{i} : X → Y_{i}) be a source in C and suppose B and B′ are nodes of E such that Ψ(B) = Ψ(B′) = X. The arrow-lifting property of dofs ensures us the existence of two unique sources g_{i} : B → Z_{i} and g′_{i} : B′ → Z′_{i} such that Ψ(g_{i}) = Ψ(g′_{i}) = f_{i}. We say that B ∼_{μ}^{Ψ} B′ iff Z_{i} = Z′_{i} for all i. This situation is illustrated in the following picture:

[figure: E; C; Ψ; X; B; B′; Y_{1}; Y_{n}; Z_{1} = Z′_{1}; Z_{n} = Z′_{n}; f_{1}; f_{n}; g_{1}; g′_{1}; g′_{n}; g_{n}; …; …]

It is clear that the functor corresponding to Ψ takes μ to a mono-source iff B ∼_{μ}^{Ψ} B′ ⇒ B = B′.

Now, let δ = (f_{i} : X → Y_{i}, f′_{i} : X′ → Y_{i}) be a double-source in C. The functor corresponding to Ψ takes δ to a disjoint double-source iff there is no double-source δ′ = (g_{i} : B → Z_{i}, g′_{i} : B′ → Z_{i}) in E such that Ψ(δ′) = δ.

4.2. Definition. Let (S, M, A) be a data-specification. Let A^{!} be the right Kan extension of A along I : S_{0} → S and let ∫ A^{!} be the category of elements of A^{!}, with associated projection Π : ∫ A^{!} → S. We define the translation of (S, M, A) to be the MD-sketch (C^{t}, M^{t}, D^{t}) where

1. C^{t} is ∫ A^{!}.

2. M^{t} is {μ | Π(μ) ∈ M}.

3. D^{t} is {(f_{i} : X → Y_{i}, g_{i} : Z → Y_{i}) | X ≠ Z, Π(f_{i}) = Π(g_{i}) ∈ M}.

4.3. Theorem. The model-category of a data-specification (S, M, A) is equivalent to the model-category of its translation (C^{t}, M^{t}, D^{t}).

Proof. First we prove that both model categories are equivalent to full subcategories of FinDof(C^{t}).

For Mod(C^{t}, M^{t}, D^{t}), this is obvious, since this category is a full subcategory of Fun(C^{t}, FinSet), and we know that Fun(C^{t}, FinSet) is equivalent with FinDof(C^{t}).

For Mod(S, M, A), we know from lemmas 3.5 and 3.6 that this category is a full subcategory of Fun(S, FinSet)/A^{!}. Therefor, it is equivalent to a full subcategory of FinDof(S)/(Π : ∫ A^{!} → S). But it is well-known that:

FinDof(S)/(Π : ∫ A^{!} → S) is equivalent with FinDof(∫ A^{!})

Hence, we conclude that both model categories are equivalent to full subcategories of FinDof(C^{t}). It remains to verify that an object of FinDof(C^{t}) corresponds to a model of (C^{t}, M^{t}, D^{t}) iff it corresponds to a model of (S, M, A).

An object Ψ : E → C^{t} corresponds to a model of (C^{t}, M^{t}, D^{t}) iff the functor F : C^{t} → FinSet corresponding to Ψ satisfies all monicity conditions in M^{t} and all disjointness conditions in D^{t}. We have seen in paragraph 4.1 what this means in terms of Ψ.

An object Ψ : E → C^{t} corresponds to a model of (S, M, A) iff the functor F : S → FinSet corresponding to the dof Π ∘ Ψ satisfies all monicity conditions in M.

We prove that these two conditions are equivalent.

1. Suppose Ψ : E → C^{t} corresponds to a model of (S, M, A). Then we know that B ∼_{μ}^{Π∘Ψ} B′ implies that B = B′, for all μ ∈ M.

Let μ′ be an element of M^{t} and suppose B ∼_{μ′}^{Ψ} B′, then B ∼_{μ}^{Π∘Ψ} B′ where μ = Π(μ′), and hence B = B′. We conclude that all sources in M^{t} are taken to mono-sources.

Let δ′ = (f′_{i} : X′ → Y′_{i}, g′_{i} : Z′ → Y′_{i}) be an element of D^{t}. Suppose δ′ is not satisfied by the functor corresponding to Ψ. This means that there is a double-source δ = (f_{i} : X → Y_{i}, g_{i} : Z → Y_{i}) such that Ψ(δ) = δ′. From the definition of the translation we know that μ = Π(f′_{i}) = Π(g′_{i}) ∈ M, and that X′ ≠ Z′. Since Ψ(X) = X′ and Ψ(Z) = Z′, it follows that X ≠ Z. Yet, we have that X ∼_{μ}^{Π∘Ψ} Z, which contradicts the fact that Ψ corresponds to a model of (S, M, A). We conclude that all doublesources in D^{t} are taken to disjoint double-sources.

Hence, Ψ : E → C^{t} also corresponds to a model of (C^{t}, M^{t}, D^{t}).

2. Suppose Ψ : E → C^{t} corresponds to a model of (C^{t}, M^{t}, D^{t}).

Let μ ∈ M and suppose B ∼_{μ}^{Π∘Ψ} B′. Then Ψ(B) must be equal to Ψ(B′) , or a disjointness condition in D^{t} would be violated. But that means that B ∼_{μ′}^{Ψ} B′ for some μ′ with Π(μ′) = μ. Hence B = B′ and Ψ corresponds to a model of (S, M, A).

4.4. Corollary. Equivalence of data-specifications is decidable.

Proof. Apply theorem 4.3 to compute two equivalent MD-sketches, and then apply theorem 2.18 to decide the equivalence of these two MD-sketches.

4.5. Remark. Because of theorem 4.3, which states that any data-specification can be translated to an MD-sketch, the reader might wonder whether data-specifications are now obsolete (subsumed by MD-sketches). We believe that this is not the case. Data-specifications have a very intuitive nature, and are very close to the kind of dataspecifications that are used in practice. MD-sketches are cumbersome to work with in practice. For example, the translation of a data-specification to an MD-sketch tends to make the specification much larger, and unreadable to a human reader. On the other hand, MD-sketches are easier to treat mathematically, since they are sketches, and a lot is known about sketches and their model categories. Therefor, we believe that both kinds of specifications have their uses.

We end this section with an example of an equivalence proof of two data-specifications.

Example. It is an easy exercise to translate specifications (2) and (4) to MD-sketches. Specification (4) is already an MD-sketch, since the functor A is the constant functor on 1. To translate specification (2), you must compute the category of elements of the right Kan extension of A along the inclusion of S_{0} into S. These constructions are straightforward, algorithms can be found in [8]. The resulting category is isomorphic (call the isomorphism i) to the underlying category of specification (4). The set of doublesources of the translation is empty, and the set of sources contains 2 sources which map under i to the 2 sources in the set of sources of specification (4). Hence, the translations of specifications (2) and (4) are isomorphic as MD-sketches. We conclude that their model-categories are equivalent.

5. Conclusion

We have studied MD-sketches, a specific kind of Finite Sum sketches, and we have proved that equivalence of model categories is algorithmically decidable for this class of sketches. Moreover, our proof was constructive: an algorithm to decide the equivalence of MDsketches can be extracted from the proof.

Then we have shown that data-specifications, as used in database design, can be translated to MD-sketches. Again, the proof was constructive, and an algorithm to compute the translation was given.

As a consequence, we obtain an algorithm to decide the equivalence of data-specifica-tions. Moreover, the proofs are also constructive in the following sense: if you find that two data-specifications (or two MD-sketches) are indeed equivalent, then the equivalence between the model categories itself is also computable. Given a model of the first specification, it is possible to compute the image of this model under the equivalence, giving you a corresponding model of the second specification.

The ability to decide equivalence of data-specifications, and to compute corresponding models for equivalent specifications is of major importance during view-integration, the process of combining several partly overlapping data-specifications into one big dataspecification.

References

[1] J. Adámek, H. Herrlich, G. E. Strecker. Abstract and Concrete Categories Wiley-Interscience publications, 1990.

[2] J. Adámek, J. Rosický. Locally presentable and accessible categories, Cambridge University Press, 1994.

[3] J. Adámek, J. Rosický. “Finitary sketches” Journal of Symbolic Logic, to appear.

Theory and Applications of Categories, Vol. 1, No. 8 173 [4] J. Adámek, J. Rosický. “On geometric and finitary sketches”, preprint.

[5] M. Barr, C. Wells. Category Theory for Computing Science Prentice Hall International Series in Computer Science, 1990.

[6] C. Batini, M. Lenzerini, S.B. Navathe. “A comparitive analysis of methodologies for database schema integration” ACM Computing Surveys, Vol. 15, nr. 4, 1986, pp. 323–364.

[7] F. Borceux, D. Dejean. “Cauchy Completion in Category Theory” Cahiers de Topologie et Géometrie Différentielle Catégoriques, Vol. XXVII–2, pp. 133–146, 1986.

[8] F. Borceux. Handbook of categorical algebra I Cambridge University Press, 1993.

[9] B. Cadish, Z. Diskin. “Algebraic graph-based approach to management of multibase systems, I: Schema integration via sketches and equations.” To appear in the proceedings of Next Generation of Information Technologies and Systems, NGITS’95, Naharia, Israel, June 1995.

[10] P. P. Chen. “The Entity-Relationship Model – Towards a Unified View of Data” ACM Transactions on Database Systems, Vol. 1, No. 1,1976,pp. 9–36.

[11] Z. Diskin, B. Cadish, I.Beylin. “Algebraic graph-based approach to management of multibase systems, II: Algebraic aspects of schema integration.” To appear in the proceedings of the Moscow ACM Chapter Conference ADBIS’95, Moscow, Russia, June 1995.

[12] M. Makkai. “Generalized sketches as a framework for completeness theorems.” To appear in Journal of Pure and Applied Algebra.

[13] F. Piessens, E. Steegmans. “Canonical forms for data-specifications”, Proceedings of Computer Science Logic 94, Springer Verlag LNCS 933, pp. 397–411.

[14] T. J. Teorey. Database Modeling and Design, Morgan Kaufmann Publishers, Inc. , 1990.

[15] C. Tuijn. “Data modeling from a categorical perspective”, Phd. thesis. University of Antwerpen, 1994.

[16] J. D. Ullman. Principles of Database and Knowledge-base Systems, vol. I, Computer Science Press, 1988.

[17] C. Wells. “Sketches: outline with references”.

Dept. of Computer Science, Katholieke Universiteit Leuven Celestijnenlaan 200A, B-3001 Heverlee, Belgium

Email: Frank.Piessens@cs.kuleuven.ac.be

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/1995/v1n8.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/gopher/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi and Postscript format. Details will be emailed to new subscribers and are available by WWW/gopher/ftp. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and LaTEX is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at URL http://www.tac.mta.ca/tac/ or by anonymous ftp from ftp.tac.mta.ca in the directory pub/tac/info. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

John Baez, University of California, Riverside: baez@math.ucr.edu Michael Barr, McGill University: barr@triples.math.mcgill.ca Lawrence Breen, Université de Paris 13: breen@dmi.ens.fr Ronald Brown, University of North Wales: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, University of Genoa: carboni@vmimat.mat.unimi.it P. T. Johnstone, University of Cambridge: ptj@pmms.cam.ac.uk G. Max Kelly, University of Sydney: kelly m@maths.su.oz.au Anders Kock, University of Aarhus: kock@mi.aau.dk F. William Lawvere, State University of New York at Buffalo: mthfwl@ubvms.cc.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.ruu.nl Susan Niefield, Union College: niefiels@gar.union.edu Robert Paré, Dalhousie University: pare@cs.dal.ca Andrew Pitts, University of Cambridge: ap@cl.cam.ac.uk Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@charlie.math.unc.edu Ross Street, Macquarie University: street@macadam.mpce.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca R. W. Thomason, Université de Paris 7: thomason@mathp7.jussieu.fr Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Sydney: walters b@maths.su.oz.au R. J. Wood, Dalhousie University: rjwood@cs.da.ca