Structured Theories and Institutions

Francisco Durán and José Meseguer

Computer Science Laboratory, SRI International Menlo Park, CA 94025, USA

Abstract

Category theory provides an excellent foundation for studying structured specifications and their composition. For example, theories can be structured together in a diagram, and their composition can be obtained as a colimit. There is, however, a growing awareness, both in theory and in specification practice, that structured theories should not be viewed just as the “scaffolding” used to build unstructured theories: they should become first-class citizens in the specification process. Given a logic formalized as an institution I, we therefore ask whether there is a good definition of the category of I-structured theories, and whether they can be naturally regarded as the ordinary theories of an appropriate institution S(I) generalizing the original institution I. We answer both question in the affirmative, and study good properties of the institution I inherited by S(I). We show that, under natural conditions, a number of important properties are indeed inherited, including cocompleteness of the category of theories, liberality, and extension of the basic framework by freeness constraints. The results presented here have been used as a foundation for the module algebra of the Maude language, and seem promising as a semantic basis for a generic module algebra that could be both specified and executed within the logical framework of rewriting logic.

1 Introduction

Structuring mechanisms are vital means for reusing software and for mastering the complexity of large systems at all levels, including specifications and code. Category theory provides an excellent foundation for studying structured specifications and their composition. A key contribution in the late seventies and early eighties was made by Burstall and Goguen with the Clear [4] specification language, that proposed taking colimits of theories as a systematic way of “putting theories together”. Clear was based on many-sorted equational logic, but its categorical semantics was in fact logic-independent. This led Goguen and Burstall to propose the notion of institution as an axiomatization of a general logic, and to generalize the Clear-like operations to institutions [17,18]. These ideas have had a great theoretical and practical impact: see the bibliographies [3,16], the survey [24], and for sample references on logic-independent specification building operations, e.g., [27,10,2,25].

Typically, theory composition operations begin with theories structured in some way—for example, a diagram—and result in an unstructured, or less structured, specification as their result—for example, a colimit. That is, structured theories are often “flattened” when being composed. There are however good reasons for preserving their structure. Besides the obvious understandability and design documentation reasons, it is often very useful to consider theory-building operations whose results are structured theories. For example, refining a software design can be best understood as refining structured theories [30]; also, even when we may want to extract a flattened theory, it can be much more efficient to operate at the level of structured theories [13,12]. There are also more intrinsic reasons, namely, when the semantics associated to a structured module essentially depends on its structure. For example, we often want to associate to the inclusion of a parameter theory into the body of a parameterized specification a freeness constraint, requiring that the models of the body are free extensions of the models of the parameter; more generally, one can similarly consider other notions of constraint [26,4,28,18,15]. In practice, the need for keeping and using structure is both recognized and supported by a number of languages and systems such as, for example, languages in the Clear/OBJ tradition [4,19,9,6], SPECWARE [30], and CASL [8].

Although a number of concepts and techniques have been suggested both at the theoretical and specification language levels to keep and use the necessary amount of structure for specific purposes, the most satisfactory way of addressing the need for preserving structure is to make structured theories first-class citizens. In the categorical spirit, this leads to seeking a good definition of the category of structured theories, and to investigating whether structured theories can naturally be regarded as the ordinary theories of an appropriate institution. The most basic form of structured theory is that of a hierarchy of theory inclusions, in the sense that more complex forms of structured theories can often be normalized to hierarchies [13,12], perhaps keeping some additional information such as freeness constraints. Hierarchies are of course special kinds of diagrams, and this suggests using categories of diagrams and categorical constructions on diagrams as the theoretical basis.

The use of diagrams for structuring purposes has also been emphasized by other authors. In a limited form they were used in Clear to deal with shared structure in categorical constructions by means of based theories [4]. In SPECWARE [30] diagrams are first-class citizens and are used to structure and refine specifications; furthermore, an appropriate diagram category is defined in such a way that a colimit-like functor yields an operation of horizontal composition satisfying, by functoriality, the expected laws of compatibility between horizontal and vertical composition [30]. Based on the SPECWARE ideas, Dimitrakos has proposed a way of parameterizing specifications by diagrams of specifications, and of inducing an instantiation by means of a family of parallel instantiating morphisms whose sources are the components of the parameter diagram [11].

In this paper we address a number of issues about structured theories that, as far as we know, have not been systematically studied before. The most basic issue is: given an institution I, can we naturally associate to it another institution S(I) whose ordinary theories are the structured theories of I? We answer this question in the affirmative, and then proceed to study to what extent good properties of the institution I are also inherited by S(I). We show that, under natural conditions, a number of important properties are indeed inherited, including cocompleteness of the category of theories, liberality, and extension of the basic framework by freeness constraints.

We have used the present work as the theoretical foundation for the module algebra of the Maude specification language [6]. In this module algebra, structured theories are first-class citizens, and module operations result in other structured theories [13,12]. Using the fact that rewriting logic is reflective [7,5], the entire module algebra is both specified and executed within the logic of Maude [12]. As we further explain in the conclusions, using the logic-independent semantics for structured theory compositions developed in this paper and the logical framework properties of Maude [21], we plan to generalize Maude’s module algebra to an executable generic module algebra that could be instantiated for any logic represented in the framework.

The rest of the paper is organized as follows. Section 2 reviews some basic definitions about institutions; Section 3 gives basic results about categories of diagrams; Section 4 presents our main definitions and results about the institution S(I) of structured I-theories and its properties; and Section 5 offers some concluding remarks.

2 Institutions

The theory of institution [18] allows us to discuss the relationship between theories and models without committing ourselves to a particular logical system.

Definition 2.1 [17] An institution I is a 4-tuple (Sign_{I}, sen_{I}, Mod_{I}, ⊧) such that:

• Sign_{I} is a category whose objects are called signatures,

• sen_{I}: Sign_{I} ⟶ Set is a functor associating to each signature Σ a set of Σ-sentences,

• Mod_{I}: Sign_{I} ⟶ Cat^{op} is a functor mapping each signature Σ to a category whose objects are called Σ-models, and

• ⊧ is a function associating to each Σ ∈ |Sign_{I}| a binary relation ⊧_{Σ} ⊆ |Mod_{I}(Σ)| × sen_{I}(Σ) called satisfaction in such a way that the following property holds for any M′ ∈ |Mod_{I}(Σ′)|, H : Σ → Σ′, φ ∈ sen_{I}(Σ):

M′ ⊧_{Σ′} sen_{I}(H)(φ) ⟺ Mod_{I}(H)(M′) ⊧_{Σ} φ.

Given a signature Σ, a presentation of a theory is given by a set Γ of Σ-sentences. We can therefore denote a theory presentation as a pair (Σ, Γ). Given a presentation (Σ, Γ), we define the category Mod_{I}(Σ, Γ) as the full subcategory of Mod_{I}(Σ) determined by those models M ∈ |Mod_{I}(Σ)| that satisfy all the sentences in Γ, i.e., M ⊧_{Σ} φ for each φ ∈ Γ.

We can extend the satisfaction relation to sets of sentences as follows.

M ⊧_{Σ} Γ iff M ⊧_{Σ} φ for each φ ∈ Γ.

Then, the relation between sets of sentences and sentences given by

Γ ⊧_{Σ} φ iff M ⊧_{Σ} φ for each M ∈ |Mod_{I}(Σ, Γ)|

allows us to associate to an institution an entailment system in the sense of [22]. For any signature Σ, the closure of a set Γ of Σ-sentences is Γ^{•} = {φ | Γ ⊧_{Σ} φ}. The Σ-theory presented by (Σ, Γ) is then given by (Σ, Γ^{•}).

Given presentations of theories (Σ, Γ) and (Σ′, Γ′), a theory morphism H: (Σ, Γ) → (Σ′, Γ′) is a signature morphism H: Σ → Σ′ such that if φ ∈ Γ then sen_{I}(H)(φ) ∈ Γ′^{•}, that is, for all φ ∈ Γ, Γ′ ⊧_{Σ′} sen_{I}(H)(φ).

Definition 2.2 Given an institution I, its category Th_{I} of theories^{1} has as objects presentations of theories (Σ, Γ) and as arrows theory morphisms. We denote by sign_{I}: Th_{I} → Sign_{I} the forgetful functor sending each theory to its underlying signature.

For any institution I, the model functor Mod_{I}: Sign_{I} ⟶ Cat^{op} extends to a functor Mod_{I} : Th_{I} → Cat^{op}, by mapping a theory (Σ, Γ) to the full subcategory Mod_{I}(Σ, Γ) of Mod_{I}(Σ). The institution I is called liberal if for each theory morphism H : (Σ, Γ) → (Σ′, Γ′) the functor Mod_{I}(H) has a left adjoint. We call I exact if Mod_{I}: Th_{I} → Cat^{op} preserves colimits.

3 Diagram Categories

The issue of whether the category Dg(C) of diagrams over a category C has colimits is important, because for C = Sign_{I} this specializes to colimits of structured signatures, which can then be used to define colimits of structured theories. We show in this section that, if C is cocomplete, then Dg(C) is also cocomplete. This is probably a “folklore” result. Since we are not aware of a

1 Note that in the above definition the objects of Th_{I} are presentations of theories. We follow here the terminology of Meseguer’s general logics [22], instead of Goguen and Burstall’s original definition [18]. In what follows, when we talk about a theory (Σ, Γ) we shall mean a theory presentation.

suitable textbook exposition to give as a reference, we include it here to make the paper self-contained.

Given a cocomplete category C and a small category A, the category of functors from A to C, which we denote by C^{A}, is also a cocomplete category [20]. Furthermore, in C^{A} all colimits can be constructed pointwise.

Theorem 3.1 (Left Kan extensions [20,29]) Let B be a small category, let F: B → D be a functor, and let C be a cocomplete category. Then, the functor F̃ = C^{F} : C^{D} → C^{B} has a left adjoint Ṽ_{F} : C^{B} → C^{D}, called the left Kan extension along F.

Definition 3.2 [29] Let C be a category. The diagram category Dg(C) has as objects functors T : P → C, where P is a small category. If T : P → C and T′: P′ → C are objects, then a morphism (R, ϱ): T → T′ consists of a functor R: P → P′ and a natural transformation ϱ: T → T′ · R.

The composition of morphisms (R, ϱ) and (R′, ϱ′), as depicted in the figure below, is given by the morphism (R′ · R, ϱ′R · ϱ).

[figure: P; T; R; P′; T′; R′; ϱ; ϱ′; C; P′′; T′′]

Theorem 3.3 Let C be a cocomplete category. Then, the category Dg(C) is also cocomplete.

Since a category with pushouts and coproducts has all colimits, we split the proof of Theorem 3.3 in two separate lemmas. The proofs summarize the main constructions; a detailed exposition can be found in [12].

Lemma 3.4 If C is cocomplete, then Dg(C) has pushouts.

Proof. Given small categories P_{0}, P_{1}, and P_{2}, diagrams D_{0} in C^{P_{0}}, D_{1} in C^{P_{1}}, and D_{2} in C^{P_{2}}, and diagram morphisms (F, α) : D_{0} → D_{1} and (J, β) : D_{0} → D_{2}, we need to construct a pushout object D_{3} in C^{P_{3}}, and corresponding morphisms in Dg(C), as depicted in the following figure:

[figure: D_{2}; (F′,δ); D_{3}; D_{0}; (J,β); (F,α); D_{1}; (J′,γ)]

First, we define the small category P_{3}, with J′: P_{1} → P_{3} and F′: P_{2} → P_{3}, as the pushout of F and J in Cat. The intuitive idea in order to build up the desired diagram D_{3} is the following: if the D_{i} were all in the same category C^{P}, then the pushout could be constructed pointwise. We obtain the more general construction by taking the Kan extensions along the corresponding functors to P_{3} for each of these diagrams, thus “moving” them all to C^{P_{3}}; D_{3} is then the pushout of the Kan-extended diagrams in C^{P_{3}}, which can be computed pointwise.

Lemma 3.5 For any category C, Dg(C) has coproducts.

Proof. Let {D_{i}: J_{i} → C}_{i∈I} be an I-indexed family of diagrams for any set I. Let ∐_{i∈I} J_{i} be the coproduct of {J_{i}}_{i∈I} in Cat, and let us denote the inclusion morphisms by ι_{i}: J_{i} → ∐_{i∈I} J_{i}. It is easy to check that the induced functor D : ∐_{i∈I} J_{i} → C, with the induced family of inclusion morphisms {(ι_{i}, 1_{D_{i}}) : D_{i} → D}_{i∈I}, is the coproduct of the indexed family {D_{i}}_{i∈I} in Dg(C).

4 Structured Theories

In this section we define the institution S(I) of structured theories over a given institution I, and give some results about the cocompleteness of its categories of signatures and theories, the liberality of S(I), and the addition of freeness constraints to structured theories.

4.1 The Institution of Structured Theories

A structured signature can be formalized as a functor D: I → Sign_{I} from a small category I to the category Sign_{I} of signatures and signature morphisms in a given institution I. This is of course a quite general notion. One can specialize the concept to the more familiar concept of hierarchy of signatures by requiring that I is a finite poset and that all the arrows in the diagram are inclusions in an appropriate subcategory of inclusion morphisms. Based on this definition, we build an institution S(I), whose theories are called structured I-theories, by defining functors sen_{S(I)} and Mod_{S(I)} associating to each structured signature D in Sign_{S(I)} a set of D-sentences and a category of D-models, respectively. Then, we give a satisfaction relation for it and show that the satisfaction condition holds.

Definition 4.1 Let us denote by Sign_{S(I)} the category Dg(Sign_{I}) of diagrams over the category of signatures in the institution I. We shall call the objects of Sign_{S(I)}structured (I-)signatures, and will denote each structured signature by its corresponding diagram D : I → Sign_{I}. The morphisms in Sign_{S(I)}are called structured signature morphisms.

Definition 4.2 The functor sen_{S(I)} : Sign_{S(I)} → Set, associating to each structured signature D: I → Sign_{I} a set of sentences and to each structured signature morphism (K, H): D → D′ a corresponding translation at the level of sentences, is defined as follows:

sen_{S(I)}(D) = ∐_{i∈I} sen_{I}(D(i))

sen_{S(I)}((K, H)) = ∐_{i∈I} sen_{I}(H_{i})

We can see each of the sentences of D as a pair (i, φ), where φ is a sentence in sen_{I}(D(i)). Note that, given a structured signature morphism (K, H): D → D′ and a sentence (i, φ) of D, we have

sen_{S(I)}((K, H))((i, φ)) = (K(i), sen_{I}(H_{i})(φ)).

Definition 4.3 Given a structured signature D : I → Sign_{I}, its category of models Mod_{S(I)}(D) has as objects families M = {M_{i}}_{i∈I} with M_{i} in Mod_{I}(D(i)), such that for each ϕ : i → j in I, Mod_{I}(D(ϕ))(M_{j}) = M_{i}. A morphism between two such models f : M → M′ is given by a family {f_{i}: M_{i} → M′_{i}}_{i∈I} with f_{i} in Mod_{I}(D(i)) such that for each ϕ: i → j in I, Mod_{I}(D(ϕ))(f_{j}) = f_{i}.

Definition 4.4 The functor Mod_{S(I)} : Sign_{S(I)} → Cat^{op} assigns to each structured signature D: I → Sign_{I} its category of models Mod_{S(I)}(D), and to each structured signature morphism (K, H): D → D′ the forgetful functor Mod_{S(I)}((K, H)): Mod_{S(I)}(D′) → Mod_{S(I)}(D), defined as follows:

Mod_{S(I)}((K, H))({M′_{j}}_{j∈I′}) = {Mod_{I}(H_{i})(M′_{K(i)})}_{i∈I}
Mod_{S(I)}((K, H))({f′_{j}}_{j∈I′}) = {Mod_{I}(H_{i})(f′_{K(i)})}_{i∈I}

Definition 4.5 Given a structured signature D, a D-model M = {M_{i}}_{i∈I} satisfies a D-sentence (i, φ) if and only if M_{i} ⊧_{D(i)} φ. In this case, we write M ⊧_{D} (i, φ).

Proposition 4.6 (Satisfaction Condition) Let D: I → Sign_{I} and D′: I′ → Sign_{I} be structured signatures, and let (K, H) : D → D′ be a structured signature morphism. Given a D-sentence (i, φ) and a D′-model M′, then

Mod_{S(I)}((K, H))(M′) ⊧_{D} (i, φ) ⟺ M′ ⊧_{D′} sen_{S(I)}((K, H))((i, φ)).

Proof. Mod_{S(I)}((K, H))(M′) is a D-model, namely, the family of models

Mod_{S(I)}((K, H))(M′) = {Mod_{I}(H_{i})(M′_{K(i)})}_{i∈I}.

Since φ is a sentence in D(i), we have

Mod_{S(I)}((K, H))(M′) ⊧_{D} (i, φ) ⟺ Mod_{I}(H_{i})(M′_{K(i)}) ⊧_{D(i)} φ.

On the other hand, since sen_{S(I)}((K, H))((i, φ)) = (K(i), sen_{I}(H_{i})(φ)), and thus sen_{I}(H_{i})(φ) is a sentence in D′(K(i)), we have

M′ ⊧_{D′} sen_{S(I)}((K, H))((i, φ)) ⟺ M′_{K(i)} ⊧_{D′(K(i))} sen_{I}(H_{i})(φ).

By the satisfaction condition for the institution I, we also have

Mod_{I}(H_{i})(M′_{K(i)}) ⊧_{D(i)} φ ⟺ M′_{K(i)} ⊧_{D′(K(i))} sen_{I}(H_{i})(φ),

and therefore,

Mod_{S(I)}((K, H))(M′) ⊧_{D} (i, φ) ⟺ M′ ⊧_{D′} sen_{S(I)}((K, H))((i, φ)).

Definition 4.7 Let S(I) be the institution with:

• Sign_{S(I)} as category of signatures,

• the sentence functor sen_{S(I)}: Sign_{S(I)} → Set, of Definition 4.2,

• the model functor Mod_{S(I)}: Sign_{S(I)} → Cat^{op}, of Definition 4.4, and • the satisfaction relation given in Definition 4.5, for which the satisfaction

condition holds as shown in Proposition 4.6.

Note that the notion of structured I-theory, that is, of a theory presentation in S(I), captures well the intuitive notion of structured theory encountered in actual specifications. Indeed, when a subtheory is imported, its axioms typically are not repeated again; they are implicitly inherited from the subtheory. This means that axioms are presented locally, for a specific local signature D(i), corresponding to our formal notion of a pair (i, φ). It also means that at each stage in the specification only the incremental information of additional axioms has to be made explicit.

Since Sign_{S(I)} = Dg(Sign_{I}), there should be a close and systematic relationship between the category Th_{S(I)} of structured I-theories and the diagram category Dg(Th_{I}). We can express this relationship as an adjunction with particularly good properties.

Let J: Th_{S(I)} → Dg(Th_{I}) be the functor defined on objects by the rule

(D, Γ) ↦ D_{Γ^{∗}},

where if D: I → Sign_{I} is a structured signature, then D_{Γ^{∗}} : I → Th_{I} has D_{Γ^{∗}}(i) = (D(i), Γ_{i}^{∗}) and D_{Γ^{∗}}(ϕ: i → j) = D(ϕ), where

Γ_{i}^{∗} = {φ ∈ sen_{I}(D(i)) | ∀M ∈ Mod_{S(I)}(D, Γ), M_{i} ⊧_{D(i)} φ}.

Note that then D(ϕ): D_{Γ^{∗}}(i) → D_{Γ^{∗}}(j) is a theory morphism because

φ ∈ Γ_{i}^{∗} ⇔ ∀M ∈ Mod_{S(I)}(D, Γ), M_{i} ⊧_{D(i)} φ
⇔ (by satisfaction, with Mod_{I}(ϕ)(M_{j}) = M_{i})
∀M ∈ Mod_{S(I)}(D, Γ), M_{j} ⊧_{D(j)} sen_{I}(D(ϕ))(φ)
⇒ sen_{I}(D(ϕ))(φ) ∈ Γ_{j}^{∗}

Therefore, sen_{I}(D(ϕ))(Γ_{i}^{∗}) ⊆ Γ_{j}^{∗} and D(ϕ) is a theory morphism.

The definition of J on morphisms assigns to each theory morphism (K, H): (D, Γ) → (D′, Γ′) in Th_{S(I)} the diagram morphism (K, H̃): D_{Γ^{∗}} → D′_{Γ′^{∗}} with H̃_{i} = H_{i} for each i ∈ I, which is well-defined by observing that Γ′^{•} = ∐_{j∈I′} Γ′_{j}^{∗}, and using the fact that (K, H) is a theory morphism, so that for each (i, φ) ∈ Γ we have (K(i), sen_{I}(H_{i})(φ)) ∈ Γ′^{•}.

Let R: Dg(Th_{I}) → Th_{S(I)} be the functor defined on objects by the rule

D ↦ (sign_{I} · D, ∐_{i∈I} ax(D(i))),

where, for (Σ, Γ) a theory, we use the notation ax(Σ, Γ) = Γ.

Note that for any theory (D, Γ) in Th_{S(I)} we have a natural isomorphism

RJ(D, Γ) ≃^{ε_{(D,Γ)}} (D, Γ). Indeed, by construction we have RJ(D, Γ) = (D, Γ^{•}). Therefore, both theories are isomorphic, with the identity signature morphism as the isomorphism. We do not need to define R on morphisms, since such a definition follows automatically from the adjunction result below.

Proposition 4.8 The functor J : Th_{S(I)} → Dg(Th_{I}) is full and faithful, with R left adjoint to J and ε as the counit.

Proof. By Theorem 1 of Section IV.3 in [20], if ε is a counit and is an isomorphism, J is full and faithful. So we just have to check the adjunction. A detailed proof showing that ε: RJ → 1_{Dg(Th_{I})} is indeed the counit of the adjunction can be found in [12].

4.2 Cocompleteness and Liberality

Given the institution S(I), we now present some results on the cocompleteness of its categories of signatures and theories, and on the liberality of S(I).

Theorem 4.9 If Sign_{I} is cocomplete then Sign_{S(I)} is cocomplete.

Proof. Since Sign_{S(I)} = Dg(Sign_{I}), this follows from Theorem 3.3.

By the following result from [18], it follows that, given any institution I, its category of theories is cocomplete if its category of signatures is cocomplete.

Theorem 4.10 [18] If I is an institution such that Sign_{I} is cocomplete, then Th_{I} is also cocomplete and the forgetful functor sign_{I} : Th_{I} → Sign_{I} preserves colimits.

Corollary 4.11 If Sign_{I} is cocomplete then Th_{S(I)} is cocomplete, and the functor sign_{S(I)}: Th_{S(I)} → Sign_{S(I)} preserves colimits.

The above result by Goguen and Burstall gives a simple criterion to show when all colimits in the category of theories exist. However, it may not be sufficient. We can have institutions with cocomplete categories of theories whose categories of signatures lack some colimits. For example, if we consider signature morphisms in many-sorted equational logic that can map operations to terms (as it is allowed for views in OBJ [19] and in Maude [6], for example), the category of signatures fails to be cocomplete. The following shows that, independently of the cocompleteness of Sign_{S(I)}, if Th_{I} is cocomplete then Th_{S(I)} is also cocomplete.

Theorem 4.12 If Th_{I} is cocomplete then Th_{S(I)} is cocomplete.

Proof. If Th_{I} is cocomplete, then Dg(Th_{I}) is cocomplete by Theorem 3.3. Then, since ε is a natural isomorphism, any diagram Ω in Th_{S(I)} is isomorphic to the diagram RJΩ. But, since R is a left adjoint to J, and therefore preserves colimits, and since Dg(Th_{I}) has colimits by Theorem 3.3, we have R(colim JΩ) = colim (RJΩ) = colim (Ω).

So far, we have only considered the category Mod_{S(I)}(D) of models of a structured theory D over a fixed institution I. We shall see in Section 4.3 how we can easily add freeness constraints to this setting. Liberality of an institution is an important property for freeness constraints.

Theorem 4.13 If an institution I is liberal and exact and Th_{I} is cocomplete, then S(I) is liberal.

Proof. First of all we observe that, for any (D, Γ) ∈ |Th_{S(I)}| we have the isomorphism

Mod_{S(I)}(D, Γ) ≃ lim (Mod_{I} · D_{Γ^{∗}}). (†)

Indeed, since Γ^{•} = ∐_{i∈I} Γ_{i}^{∗}, (D, Γ) and (D, Γ^{•}) are isomorphic theories. Therefore, for each M ∈ |Mod_{S(I)}(D)| we have M ⊧_{D} Γ iff M ⊧_{D} Γ^{•} iff for each i ∈ I, M_{i} ⊧_{D(i)} Γ_{i}^{∗}. Therefore, M ∈ |Mod_{S(I)}(D, Γ)| iff

(i) ∀i ∈ I, M_{i} ∈ |Mod_{I}(D(i), Γ_{i}^{∗})|, and (ii) ∀ϕ: i → j in I, Mod_{I}(D(ϕ))(M_{j}) = M_{i},

and similarly, f: M → M′ is a morphism in Mod_{S(I)}(D, Γ) iff

(i) ∀i ∈ I, f_{i}: M_{i} → M′_{i} is a morphism in Mod_{I}(D(i), Γ_{i}^{∗}), and (ii) ∀ϕ: i → j in I, Mod_{I}(D(ϕ))(f_{j}) = f_{i}.

The above isomorphism (†) then follows either by an explicit limit construction in Cat, or, more easily, by observing that Cat is monadic [1] over Graph = Set\xymatrix{• \ar[r] \ar[r] & •} (therefore the forgetful functor creates limits [20]) which reduces such a limit construction to a construction of limits in Set.

But since Th_{I} is cocomplete, the colimit of D_{Γ^{∗}} exists, and by exactness of I we have the isomorphism

lim (Mod_{I} · D_{Γ^{∗}}) ≃ Mod_{I}(colim D_{Γ^{∗}}),

which combined with the isomorphism (†) gives us the isomorphism

Mod_{S(I)}(D, Γ) ≃ Mod_{I}(colim D_{Γ^{∗}}).

Notice also that, by cocompleteness of Th_{I}, there is a functor

colim : Dg(Th_{I}) → Th_{I}

such that for any morphism (K, H) : (D, Γ) → (D′, Γ′) in Th_{S(I)} we have, thanks to the above isomorphism, the following commutative diagram.

[figure: Mod_{S(I)}(D, Γ); ≃; Mod_{S(I)}(D′, Γ′); Mod_{S(I)}((K,H)); ≃; Mod_{I}(colim D_{Γ^{∗}}); Mod_{I}(colim D′_{Γ′^{∗}}); Mod_{I}(colim J(K,H))]

By liberality of the institution I there is a left adjoint to Mod_{I}(colim J(K, H)), which, composed with the vertical isomorphisms, gives rise to a left adjoint to Mod_{S(I)}((K, H)).

4.3 Freeness Constraints

One of the key motivations for making structured theories a direct object of study is dealing with freeness constraints, called constraints or data constraints in [18]. They are crucial for the notion of parameterized module, in which the model of the parameterized module’s body should be a free extension of the model of the parameter theory. In many specification languages (e.g., [19,14,9,6,8]) this leads to a distinction between theories, with loose semantics, and modules, with initial or, more generally, free extension semantics. Both theories and modules can be parameterized, but in the case of parameterized modules, a freeness constraint between models of the parameter and models of the body is enforced.

Intuitively, freeness constraints are associated to particular theory maps appearing in the diagram of a structured theory. Suppose that I is liberal and that (D, Γ) is a structured theory with D: I → Sign_{I}, and consider a morphism ϕ: i → j in I. Then, we can associate a freeness constraint to the theory map D(ϕ): D_{Γ^{∗}}(i) → D_{Γ^{∗}}(j) by requiring that the models M of (D, Γ), in addition to satisfying the axioms Γ, satisfy the constraint

M_{j} ≃ F_{D(ϕ)}(M_{i})

for F_{D(ϕ)} : Mod_{I}(D_{Γ^{∗}}(i)) → Mod_{I}(D_{Γ^{∗}}(j)) the left adjoint to the forgetful functor Mod_{I}(D(ϕ)) : Mod_{I}(D_{Γ^{∗}}(j)) → Mod_{I}(D_{Γ^{∗}}(i)). For example, D_{Γ^{∗}}(i) may be the theory TRIV, specifying just one sort Elt, and D_{Γ^{∗}}(j) may be the theory LIST with a sort List, specifying lists formed with data elements from the Elt parameter sort. Then, the freeness constraint requires that the models of LIST are really lists, freely generated from the data elements.

The above notion of freeness constraint should in fact be generalized somewhat, to allow an extra signature map bringing the model to the context in which the constraint is applied. This leads us to the following definition, due to Goguen and Burstall.

Definition 4.14 [18] Let I be an institution. Then a freeness constraint on a signature Σ is a pair

c = (H: T′′ → T′, G: sign(T′) → Σ)

with H a theory morphism and G a signature morphism. A Σ-model M satisfies c if and only if Mod_{I}(G)(M) satisfies T′ and Mod_{I}(H)(Mod_{I}(G)(M)) has a free extension along H such that the corresponding component of the counit of the adjunction ε_{ModI(G)(M)} : F_{H}(Mod_{I}(H)(Mod_{I}(G)(M))) → Mod_{I}(G)(M) is an isomorphism; in this case we write M ⊧_{Σ} c.

Our intuitive notion of freeness constraint in a structured theory can then be recovered by two special cases of the above definition. The case of a parameterized module, illustrated by the theory inclusion TRIV ↪ LIST in our previous example, corresponds to freeness constraints of the form

(D(ϕ): D_{Γ^{∗}}(i) → D_{Γ^{∗}}(j), 1_{D(j)} : D(j) → D(j)),

whereas the case of an unparameterized module, like NAT or BOOL, for which we want an initial model semantics corresponds to a freeness constraint of the form

(∅_{D_{Γ^{∗}}(j)} : ∅ → D_{Γ^{∗}}(j), 1_{D(j)} : D(j) → D(j)),

where ∅ is the initial object in the category of signatures of an exact liberal institution I (so that Mod_{I}(∅) has only one model, let us call it also ∅) because then the initial model of D_{Γ^{∗}}(j) coincides with F_{∅_{D_{Γ^{∗}} (j)}}(∅).

The need for the more general notion of freeness constraint in Definition 4.14 has to do with translation of constraints by composition with signature morphisms. We think of a constraint c = (H: T′′ → T′, G: sign(T′) → Σ) on Σ as a sentence associated to the signature Σ. Then, if Q: Σ → Ω is a signature morphism, we can associate to the constraint c the following constraint on Ω:

sen_{I}(Q)(c) = (H: T′′ → T′, Q · G: sign(T′) → Ω).

The key point is that, as shown by Goguen and Burstall in [18], the satisfaction condition holds for freeness constraints translated along signature morphisms. Goguen and Burstall exploit this satisfaction condition to give a general construction associating to an institution I another institution C(I) (Cf. [18, Proposition 23]) with the same category of signatures and the same model functor as I, and with sen_{C(I)}(Σ) the disjoint union of the sets sen_{I}(Σ) and of the set^{2} of all freeness constraints on Σ. Then, by the general result in Theorem 4.10, if Sign_{I} is cocomplete, then Th_{C(I)} is a cocomplete category.

2 There are foundational questions about the size of the closure of a constraint theory that we will ignore here; as pointed out in [18], they can be solved, for example, by limiting the size of the category of signatures used in the original institution.

Although the construction of C(I) is given by Goguen and Burstall for an institution I whose signatures and theories are unstructured, we have pointed out above how the notion of freeness constraint finds its natural home as additional constraints added to specific components of a structured theory. The way of explicitly combining freeness constraints and structured theories is then straightforward.

Definition 4.15 Given an institution I, the institution of structured I-theories with freeness constraints is by definition the institution S(C(I)).

Theories in S(C(I)) are pairs (D, Γ), with D: I → Sign_{I} a diagram, and with Γ sentences of the form (i, φ), with φ either a sentence in sen_{I}(D(i)) or a freeness constraint on the signature D(i). Therefore, structured I-theories with freeness constraints capture the distinction between theories (with loose semantics) and modules (with initial or free extension semantics) present, as already mentioned, in many algebraic specification languages. Furthermore, they also capture the fact that such theories and modules can be combined into more general structured specifications, whose semantics explicitly depends on their structure.

Notice that, although they are of course related constructions, the institution S(C(I)) defined above is different from the institution C(S(I)), that, by Theorem 4.13 and by the general construction of C(I) of Goguen and Burstall, can also be defined for a liberal and exact institution I with Th_{I} cocomplete. Intuitively speaking, in S(C(I)) the freeness constraints are local to specific components of structured theories, whereas in C(S(I)) the freeness constraints are global, in the sense of involving pairs of structured theories. Notice also that, by Theorems 4.9 and 4.10, if Sign_{I} is cocomplete, then both Th_{S(C(I))} and Th_{C(S(I))} are also cocomplete.

5 Concluding Remarks

We have shown that the addition of structured theories to an institution I results in an institution S(I), and that if the category of signatures Sign_{I} has colimits, then the categories of signatures and theories of S(I) both have colimits. We have also shown other basic results about the category of theories of S(I), and about the liberality of the institution S(I). Finally, we have presented a very simple way of adding freeness constraints to our setting, resulting in institutions S(C(I)) and C(S(I)).

The notion of structured theory is useful not only for institutions, but also for other components of a logic such entailment systems or proof calculi [22], and could be naturally extended to those contexts. As already mentioned, the notions presented in this paper can be specialized to the more familiar case of finite hierarchies of theory inclusions by considering diagrams whose diagram schemes are finite posets, and assuming a subcategory of theory inclusions stable under pushouts along the lines of [10]. We think that it is also quite promising to study heterogeneous structured theories, involving several institutions, following the heterogenous specification ideas of Tarlecki [31].

We plan to studying further the institution S(C(I)), which can serve as a semantic basis for an executable generic module algebra that could be specified and executed in Maude, and could be instantiated for one’s logic of choice, generalizing Maude’s module algebra, which manipulates structured rewrite theories and is expressed and executed within the reflective logical framework of rewriting logic [13,12]. This would allow endowing a specification language of choice with structured theories and with a module algebra for free. Regarding S(C(I)), two important questions are: (1) finding appropriate “normal forms” for freeness constraints under suitable assumptions such as persistence; and (2) finding suitable inductive inference systems that, in spite of their intrinsic incompleteness, can approximate the logic of S(C(I)) for a given I.

References

[1] M. Barr and C. Wells. Toposes, Triples and Theories. Springer-Verlag, 1985.

[2] H. Baumeister. Unifying initial and loose semantics of parameterized specifications in an arbitrary institution. In S. Abramsky and T. Maibaum, editors, Proc. Int. Conf. on Theory and Practice of Software Development, TAPSOFT’91, Brighton, UK, April 1991, volume 493 of Lecture Notes in Computer Science, pages 103–120. Springer-Verlag, 1991.

[3] M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas, and D. Sannella, editors. Algebraic System Specification and Development. A Survey and Annotated Bibliography, volume 501 of Lecture Notes in Computer Science. Springer-Verlag, 1991.

[4] R. Burstall and J. Goguen. The semantics of Clear, a specification language. In D. Bjørner, editor, Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification, volume 86 of Lecture Notes in Computer Science, pages 292–332. Springer-Verlag, 1980.

[5] M. Clavel. Reflection in General Logics and in Rewriting Logic with Applications to the Maude Language. PhD thesis, University of Navarre, 1998.

[6] M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada. Maude: Specification and programming in rewriting logic. SRI International, January 1999. Available at http://maude.csl.sri.com.

[7] M. Clavel and J. Meseguer. Reflection and strategies in rewriting logic.

In Meseguer [23]. Available at http://www.elsevier.nl/locate/entcs/
volume4.html.

[8] CoFI Task Group on Language Design. CASL—The common algebraic specification language, version 1.0. Available at http://www.brics.dk/

Projects/CoFI, October 1998.

[9] R. Diaconescu and K. Futatsugi. CafeOBJ Report. AMAST Series. World Scientific, 1998.

[10] R. Diaconescu, J. Goguen, and P. Stefaneas. Logical support for modularisation. In G. Huet, G. Plotkin, and C. Jones, editors, Proceedings of Workshop on Logical Frameworks (Edinburgh, United Kingdom, May 1991), pages 83–130. Cambridge University Press, 1991.

[11] T. Dimitrakos. Parameterising (algebraic) specifications on diagrams. In Automated Software Engineering–ASE’98, 13th IEEE International Conference, 1998.

[12] F. Durán. A Reflective Module Algebra with Applications to the Maude Language. PhD thesis, University of Málaga, 1999.

[13] F. Durán and J. Meseguer. An extensible module algebra for Maude. volume 15 of Electronic Notes in Theoretical Computer Science. Elsevier, 1998. Available

at http://www.elsevier.nl/locate/entcs/volume15.html.

[14] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Equations and Initial Semantics. Springer-Verlag, 1985.

[15] H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2. Module Specifications and Constraints. Springer-Verlag, 1990.

[16] M. Gogolla and M. Cerioli. What is an Abstract Data Type after all? (A bibliography on the workshops on abstract data types). In E. Astesiano, G. Reggio, and A. Tarlecki, editors, Recent Trends in Data Type Specification, volume 906 of Lecture Notes in Computer Science, pages 499–523. Springer Verlag, 1995.

[17] J. Goguen and R. Burstall. Introducing institutions. In E. Clarke and D. Kozen, editors, Proc. Logics of Programming Workshop, volume 164 of Lecture Notes in Computer Science, pages 221–256. Springer-Verlag, 1984.

[18] J. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery, 39(1):95–146, 1992.

[19] J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J.-P. Jouannaud. Introducing OBJ. Technical Report SRI-CSL-92-03, Computer Science Laboratory, SRI International, March 1992. To appear in Joseph Goguen and Grant Malcolm, editors, Applications of Algebraic Specification Using OBJ, Academic Press.

[20] S. M. Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[21] N. Martí-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. In Meseguer [23]. Available at http://www.elsevier.nl/locate/

entcs/volume4.html.

[22] J. Meseguer. General logics. In H.-D. Ebbinghaus et al., editors, Logic Colloquium’87, pages 275–329. North-Holland, 1989.

[23] J. Meseguer, editor. Proc. 1st Intl. Workshop on Rewriting Logic and its Applications, Asilomar, California, U.S.A, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier, September 1996. Available at http:

//www.elsevier.nl/locate/entcs/volume4.html.

[24] J. Meseguer and N. Martí-Oliet. From abstract data types to logical frameworks. In E. Astesiano, G. Reggio, and A. Tarlecki, editors, Recent Trends in Data Type Specification, volume 906 of Lecture Notes in Computer Science, pages 499–523. Springer Verlag, 1995.

[25] F. Orejas, E. Pino, and H. Ehrig. Institutions for logic programming. Theoretical Computer Science, 173:485–511, 1997.

[26] H. Reichel. Initially - restricting algebraic theories. In P. Dembínski, editor, Proceedings of the 9th Symposium on Mathematical Foundations of Computer Science, volume 88 of Lecture Notes in Computer Science, pages 504–514. Springer-Verlag, 1980.

[27] D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76(2/3):165–210, 1988.

[28] D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. In M. Karpinski, editor, Proceedings of the 1983 International Conference on Foundations of Computation Theory. Borgholm, Sweden, August 21-27, 1983, volume 158 of Lecture Notes in Computer Science, pages 415–427. Springer-Verlag, 1983.

[29] H. Schubert. Categories. Springer-Verlag, 1972.

[30] Y. Srinivas and R. Jüllig. SPECWARE: Formal support for composing software. In B. Moeller, editor, Proceedings of the Conference on Mathematics of Program Construction, volume 947 of Lecture Notes in Computer Science, pages 399–422. Springer-Verlag, 1995.

[31] A. Tarlecki. Towards heterogeneous specifications. In Proc. Workshop on Frontiers of Combining Systems FroCoS’98, Applied Logic Series. Kluwer Academic Publishers, 1998.