This page is a sub-page of our page on Category Theory.
• Categorical Informatics
• Limits and Colimits
• Functor Categories
• Category of Bundles (over a Base Space)
• Naturally Related Functors and Processes
• Adjoint Functors
• Institution Theory
• The Human Category
In his overview of the development of Institution theory, Diaconescu (2009) states that:
30 years have passed since the introduction by Joseph Goguen and Rod Burstall of the concept of ‘institution’ (under the name ‘language’). Since then institution theory has gradually developed from a simple and strikingly elegant general category theoretic formulation of the informal notion of logical system into an important trend of what is now called ‘universal logic’, with substantial applications and implications in both logic and computing science. […]
Institution theory may be the only important trend in universal logic that has emerged from within computing science, the others emerging from logic, and perhaps philosophy. This origin of institution theory may surprise many, since computing science is often blamed for its poor intellectual value. While this perception may be generally correct in average, there are very significant exceptions.
In fact, what is now labelled as ‘computing science’ is hardly a science in the way mathematics or physics are. Some say it is still too young and there was not enough time to coagulate, however one can hear this since 50 years already and probably in the next 50 years too. It may be more realistic to view computing science as a playground were several actors, most notably mathematics, but also logic, engineering, philosophy, sociology, biology, play.
Sometimes an extremely interesting play, which has not only brought significant changes and developments to the actors, but also has revolutionized our scientific thinking in many ways. Institution theory is such an example, the way we think of logic and model theory will never be the same as before.
As the paper included in this anthology shows, the birth of the institution concept came as a response to the population explosion of logical systems in use in specification theory and practice at the time. People felt that many of the theoretical developments (concepts, results, etc.), and even aspects of implementations, are in fact independent of the details of the actual logical systems, that especially in the area of structuring of specifications or programs, it would be possible to develop the things in a completely generic way. The benefit would be not only in uniformity, but also in clarity since for many aspects of specification theory the concrete details of actual logical systems may appear as irrelevant, with the only role being to suffocate the understanding. The first step to achieve this was to come up with a very general formal definition for the informal concept of logical system.
Due to their generality, category-theoretic concepts appeared as ideal tools. However there is something else which makes category theory so important for this aim: its deeply embedded non-substantialist thinking which gives prominence to the relationships (morphisms) between objects in the detriment of their internal structure.
Moreover, category theory was at that time, and continues even now to be so, the mathematical field of the utmost importance for computing science. In fact, it was computing science which recovered the status of category theory, at the time much diminished in conventional mathematical areas. The essay that Joseph Goguen wrote remains one of the most beautiful essays on the significance of category theory for computing science – and not only for computing science.
//////// End of Quote
Five dogmas of category theory:
(Joseph Goguen: A Categorical Manifesto, 1989):
Below is a short summary from Joseph Goguen’s Categorical Manifesto from 1989:
//////// Quote from Joseph Goguen’s Categorical Manifesto:
This informal paper tries to motivate the use of category tbeory in computing science by giving heuristic guidelines for applying five basic categorical concepts: category, functor, natural transformation, adjoint, and colimit. Several examples and some general discussion are given for each concept, and a number of references are cited, although no attempt has been made for completeness. Some additional categorical concepts and suggestions for further research are also mentioned. The paper concludes with a brief discussion of some implications for foundations. […]
Among the reasons why a computing scientist might be interested in category theory are that it can provide help with the following:
• Formulating definitions and theories. In fields that are not yet very well developed, like computing science, it often seems that formulating basic concepts is the most difficult part of research. The five guidelines given below provide relatively explicit measures of elegance and coherence that can be helpful in this regard.
• Carrying out proofs. Once basic concepts have been correctly formulated in a categorical language, it often seems that proofs “just happen”: at each step, there is a “natural” thing to try, and it works. Diagram chasing […] provides many nice examples of this. It could almost be said that the purpose of category theory is to reduce all proofs to such simple calculations.
• Discovering and exploiting relations with other fields. Finding similar structures in different areas suggests trying to find further similarities. For example, an analogy between Petri nets and the -calculus might suggest looking for a closed category structure on nets ([…], which seems to open an entirely new approach to concurrency).
• Formulating conjectures and research directions. For example, if you have found an interesting functor, you might be well advised to investigate its adjoints.
• Dealing with abstraction and representation independence. In computing science, abstract viewpoints are often better, because of the need to achieve independence from the often overwhelmingly complex details of how things are represented or implemented. A corollary of the first guideline is that two objects are “abstractly the same” iff they are isomorphic; […]. Moreover, universal constructions (i.e., adjoints) define their results uniquely up to isomorphism, i.e., abstractly in just this sense. […]
This note presents five guidelines for using category theory, each with some general discussion and some specific examples. There is no claim to originality, since I believe the underlying intuitions are shared by essentially all workers in category theory, although they have been understandably reluctant to place such dogmatic assertions in textbooks or other written documents.
The five guidelines are necessarily imprecise, and will seem exaggerated if taken too literally, since they are not objective facts, but rather heuristics for applying certain mathematical concepts. In particular, they may seem difficult to apply, or even impossible, in some situations, and they may need refinement in others. As a reminder that they should not be taken too dogmatically, I will call them dogmas.
The first dogma is as follows:
To each species of mathematical structure, there corresponds a category
whose objects have that structure, and whose morphisms preserve it.
It is part of this dogma that in order to understand a structure, it is necessary to understand the morphisms that preserve it. Indeed, many category theorists feel that the morphisms are more important than the objects, since they reveal what the structure really is. Moreover, the category concept can be defined using only morphisms. It is the bias of modern Western language and culture towards objects, rather than towards relationships, that assigns precedence to objects over morphisms. […]
The second dogma says:
To any construction on structures of one species, say widgets,
yielding structures of another species, say whatsits,
there corresponds a functor from the category of widgets to the category of whatsits.
It is part of this dogma that a construction is not merely a function from objects of one species to objects of another species, but must also preserve the essential relationships among these objects, including their structure preserving morphisms, and compositions and identities for these morphisms. This provides a test for whether or not the construction has been properly formalized. Of course, functorality does not guarantee correct formulation, but it can be surprisingly helpful in practice. […]
The third dogma says:
To each natural relationship between two functors
corresponds a natural transformation (or perhaps).
Although this looks like a mere definition of the phrase “natural relationship,” it can nevertheless be very useful in practice. It is also interesting that this concept was the historical origin of category theory. […]
The fourth dogma says:
Any canonical construction from widgets to whatsits
is an adjoint of another functor, from whatsits to widgets.
Although this can be seen as just a definition of “canonical construction,” it can be very useful in practice. The essence of an adjoint is the universal property that is satisfied by its value objects. This property says that there is a unique morphism satisfying a certain condition.
It is worth noting that any two (right, or left) adjoints to a given functor are naturally equivalent, i.e., adjointness determines a construction uniquely up to isomorphism. […] One of the more spectacular adjoints is that between syntax and semantics for algebraic theories, due to Lawvere in his thesis. […]
The fifth dogma says:
Given a category of widgets,
the operation of putting a system of widgets together to form some super-widget
corresponds to taking the colimit of the diagram of widgets
that shows how to interconnect them.
At least for me, this dogma first appeared in the context of General Systems Theory.
////// End of quote from Joseph Goguen’s Categorical Manifesto