Structured theories and institutions

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 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 structured I-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 questions 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 free-ness 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. We are grateful to Narciso Martí -Oliet, Peter Mosses, and the anonymous referees for their careful reading of a previous version and for many useful suggestions to improve the exposition.