Institution (computer science)
Encyclopedia
The notion of institution has been created by Joseph Goguen
and Rod Burstall
in the late 1970s
in order to deal with the "population explosion among the logical systems used in
computer science
". The notion tries to capture the essence of the concept of "logical system".
With this, it is possible to develop concepts of specification language
s (like structuring of specifications, parameterization, implementation, refinement, development), proof calculi and even tool
s in a way completely independent of the underlying logical system. There are also morphism
s that allow to relate and translate logical systems. Important applications of this are re-use of logical structure (also called borrowing), heterogeneous specification and combination of logics. Recently, institutional model theory
has generalized many notions and deep results of model theory
.
s and sentences
may be arbitrary objects; the only assumption being that there is a satisfaction relation between models and sentences, telling whether a sentence holds in a model or not. Satisfaction is inspired by Tarski's truth definition
, but can in fact be any binary relation.
A crucial feature of institutions now is that models, sentences and their satisfaction are always being considered to live in some vocabulary or context (called signature) that defines the (non-logical) symbols that may be used in sentences and that need to be interpreted in models. Moreover, signature morphisms allow to extend signatures, change notation etc. Nothing is assumed about signatures and signature morphisms except that signature morphisms can be composed; this amounts to having a
category
of signatures and morphisms. Finally, it is assumed that signature morphisms lead to translations of sentences and models in a way that satisfaction is preserved. While sentences are translated along with signature morphisms (think of symbols being replaced along the morphism), models are translated (or better: reduced) against signature morphisms: for example, in case of a signature extension, a model of the (larger) target signature may be reduced to a model of the (smaller) source signature by just forgetting some components of the model.
Formally, an institution consists of
such that for each
in 
the following satisfaction condition holds:
if and only if 
for each
and 
.
The satisfaction condition expresses that truth is invariant under change of notation
(and also under enlargement or quotienting of context).
Strictly speaking, the model functor ends in the quasi-category
of all large categories.
Joseph Goguen
Joseph Amadee Goguen was a computer science professor in the Department of Computer Science and Engineering at the University of California, San Diego, USA, who helped develop the OBJ family of programming languages. He was author of A Categorical Manifesto and founder and Editor-in-Chief of the...
and Rod Burstall
Rod Burstall
Rodney Martineau Burstall is one of four founders of the Edinburgh Laboratory for Foundations of Computer Science.He was an early and influential proponent of functional programming, pattern matching, and list comprehension, and is known for his work with Robin Popplestone on POP, an innovative...
in the late 1970s
in order to deal with the "population explosion among the logical systems used in
computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
". The notion tries to capture the essence of the concept of "logical system".
With this, it is possible to develop concepts of specification language
Specification language
A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...
s (like structuring of specifications, parameterization, implementation, refinement, development), proof calculi and even tool
Tool
A tool is a device that can be used to produce an item or achieve a task, but that is not consumed in the process. Informally the word is also used to describe a procedure or process with a specific purpose. Tools that are used in particular fields or activities may have different designations such...
s in a way completely independent of the underlying logical system. There are also morphism
Morphism
In mathematics, a morphism is an abstraction derived from structure-preserving mappings between two mathematical structures. The notion of morphism recurs in much of contemporary mathematics...
s that allow to relate and translate logical systems. Important applications of this are re-use of logical structure (also called borrowing), heterogeneous specification and combination of logics. Recently, institutional model theory
Institutional model theory
Institutional model theory generalizes a large portion of first-order model theory to an arbitrary logical system.- Overview :The notion of "logical system" here is formalized as an institution. Institutions constitute a model-oriented meta-theory on logical systems similar to how the theory of...
has generalized many notions and deep results of model theory
Model theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
.
Definition
The theory of institutions does not assume anything about the nature of the logical system. That is, modelInterpretation (logic)
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation...
s and sentences
Sentence (mathematical logic)
In mathematical logic, a sentence of a predicate logic is a boolean-valued well formed formula with no free variables. A sentence can be viewed as expressing a proposition, something that may be true or false...
may be arbitrary objects; the only assumption being that there is a satisfaction relation between models and sentences, telling whether a sentence holds in a model or not. Satisfaction is inspired by Tarski's truth definition
T-schema
The T-schema or truth schema is used to give an inductive definition of truth which lies at the heart of any realisation of Alfred Tarski's semantic theory of truth...
, but can in fact be any binary relation.
A crucial feature of institutions now is that models, sentences and their satisfaction are always being considered to live in some vocabulary or context (called signature) that defines the (non-logical) symbols that may be used in sentences and that need to be interpreted in models. Moreover, signature morphisms allow to extend signatures, change notation etc. Nothing is assumed about signatures and signature morphisms except that signature morphisms can be composed; this amounts to having a
category
Category (mathematics)
In mathematics, a category is an algebraic structure that comprises "objects" that are linked by "arrows". A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. A simple example is the category of sets, whose...
of signatures and morphisms. Finally, it is assumed that signature morphisms lead to translations of sentences and models in a way that satisfaction is preserved. While sentences are translated along with signature morphisms (think of symbols being replaced along the morphism), models are translated (or better: reduced) against signature morphisms: for example, in case of a signature extension, a model of the (larger) target signature may be reduced to a model of the (smaller) source signature by just forgetting some components of the model.
Formally, an institution consists of
- a categoryCategory (mathematics)In mathematics, a category is an algebraic structure that comprises "objects" that are linked by "arrows". A category has two basic properties: the ability to compose the arrows associatively and the existence of an identity arrow for each object. A simple example is the category of sets, whose...
of signatures, - a functorFunctorIn category theory, a branch of mathematics, a functor is a special type of mapping between categories. Functors can be thought of as homomorphisms between categories, or morphisms when in the category of small categories....
SetCategory of setsIn the mathematical field of category theory, the category of sets, denoted as Set, is the category whose objects are sets. The arrows or morphisms between sets A and B are all functions from A to B...
giving, for each signature
, the set of sentences 
, and for each signature morphism 
, the sentence translation map 
, where often 
is written as 
, - a functorFunctorIn category theory, a branch of mathematics, a functor is a special type of mapping between categories. Functors can be thought of as homomorphisms between categories, or morphisms when in the category of small categories....
CatCategory of small categoriesIn mathematics, specifically in category theory, the category of small categories, denoted by Cat, is the category whose objects are all small categories and whose morphisms are functors between categories...
giving, for each signature
, the category of models 
, and for each signature morphism 
, the reduct functor 
, where often 
is written as 
, - a satisfaction relationBinary relationIn mathematics, a binary relation on a set A is a collection of ordered pairs of elements of A. In other words, it is a subset of the Cartesian product A2 = . More generally, a binary relation between two sets A and B is a subset of...
for each 
,
such that for each
in the following satisfaction condition holds: if and only if for each
and .The satisfaction condition expresses that truth is invariant under change of notation
(and also under enlargement or quotienting of context).
Strictly speaking, the model functor ends in the quasi-category
Quasi-category
In mathematics, a quasi-category is a higher categorical generalization of a notion of a category introduced by .André Joyal has much advanced the study of quasi-categories showing that most of the usual basic category...
of all large categories.
Examples of Institutions
- First-order logicFirst-order logicFirst-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
- Higher-order logicHigher-order logicIn mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
- Intuitionistic logicIntuitionistic logicIntuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
- Modal logicModal logicModal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
- Temporal logicTemporal logicIn logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. In a temporal logic we can then express statements like "I am always hungry", "I will eventually be hungry", or "I will be hungry...
- CASLCommon Algebraic Specification LanguageThe Common Algebraic Specification Language is a general-purpose specification languagebased on first-order logic with induction. Partial functionsand subsorting are also supported....
Papers
- J. A. GoguenJoseph GoguenJoseph Amadee Goguen was a computer science professor in the Department of Computer Science and Engineering at the University of California, San Diego, USA, who helped develop the OBJ family of programming languages. He was author of A Categorical Manifesto and founder and Editor-in-Chief of the...
and R. M. Burstall, Introducing Institutions, Lecture Notes in Computer Science 164, pp. 221–256, 1984. - J. A. Goguen and R. M. Burstall, Institutions: Abstract Model Theory for Specification and Programming, Journal of the Association for Computing Machinery 39, pp. 95–146, 1992.
- J. Meseguer, General Logics, Logic Colloquium 87, pp. 275–329, North Holland, 1989.
- J. A. Goguen and G. Rosu, Institution morphisms, Formal aspects of computing 13, pp. 274–307, 2002.
- D. Sannella and A. Tarlecki, Specifications in an arbitrary institution, Information and Computation 76, pp. 165–210, 1988
- T. Mossakowski, J. A. Goguen, R. Diaconescu, A. Tarlecki. What is a Logic?. In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113–133. Birkhäuser 2005.
External links
- Institutions by Joseph Goguen
- Formalism, Logic, Institution - Relating, Translating and Structuring (including large bibliography)
- Razvan Diaconescu's publication list - contains recent work on institutional model theory