Institution (computer science)

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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 languages (like structuring of specifications, parameterization, implementation, refinement, development), proof calculi and even tools in a way completely independent of the underlying logical system. There are also morphisms 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.

Definition[edit]

The theory of institutions does not assume anything about the nature of the logical system. That is, models 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

  • a category Sign of signatures,
  • a functor sen:Sign \to Set giving, for each signature \Sigma, the set of sentences sen(\Sigma), and for each signature morphism \sigma:\Sigma\to\Sigma', the sentence translation map sen(\sigma):sen(\Sigma)\to sen(\Sigma'), where often sen(\sigma)(\varphi) is written as \sigma(\varphi),
  • a functor Mod:Sign^{op}\toCat giving, for each signature \Sigma, the category of models Mod(\Sigma), and for each signature morphism \sigma:\Sigma\to\Sigma', the reduct functor Mod(\sigma):Mod(\Sigma')\to Mod(\Sigma), where often Mod(\sigma)(M') is written as M'|_{\sigma},
  • a satisfaction relation {\models_{\Sigma}}\subseteq|{Mod(\Sigma)|\times sen(\Sigma)} for each \Sigma\in Sign,

such that for each \sigma:\Sigma\to\Sigma' in Sign the following satisfaction condition holds:

M'\models_{\Sigma'}\sigma(\varphi) if and only if M'|_{\sigma}
\models_{\Sigma} \varphi

for each M'\in Mod(\Sigma') and \varphi\in sen(\Sigma).

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 2-category of all small categories.

Examples of Institutions[edit]

References[edit]

  • J. A. Goguen 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
  • R. Diaconescu, Institution-independent Model Theory Birkhäuser, Basel, 2008,
  • T. Mossakowski, J. A. Goguen, R. Diaconescu, A. Tarlecki, "What is a Logic?", '. In Jean-Yves Beziau (Ed.), Logica Universalis: Towards a General Theory of Logic, pp. 113–133. Birkhäuser, Basel, 2005, 2nd Edition 2007.

External links[edit]

See also[edit]