Institution Morphisms |
| |
| Authors: | Joseph Goguen Grigore Ro?u |
| |
| Affiliation: | (1) Department of Computer Science and Engineering, University of California at San Diego, La Jolla, California, USA, US;(2) NASA Ames Research Center – RIACS, and Fundamentals of Computing, Faculty of Mathematics, University of Bucharest, Hungary, HU |
| |
| Abstract: | Institutions formalise the intuitive notion of logical system, including syntax, semantics, and the relation of satisfaction
between them. Our exposition emphasises the natural way that institutions can support deduction on sentences, and inclusions
of signatures, theories, etc.; it also introduces terminology to clearly distinguish several levels of generality of the institution
concept. A surprising number of different notions of morphism have been suggested for forming categories with institutions
as objects, and an amazing variety of names have been proposed for them. One goal of this paper is to suggest a terminology
that is uniform and informative to replace the current chaotic nomenclature; another goal is to investigate the properties
and interrelations of these notions in a systematic way. Following brief expositions of indexed categories, diagram categories,
twisted relations and Kan extensions, we demonstrate and then exploit the duality between institution morphisms in the original
sense of Goguen and Burstall, and the ‘plain maps’ of Meseguer, obtaining simple uniform proofs of completeness and cocompleteness
for both resulting categories. Because of this duality, we prefer the name ‘comorphism’ over ‘plain map’; moreover, we argue
that morphisms are more natural than comorphisms in many cases. We also consider ‘theoroidal’ morphisms and comorphisms, which
generalise signatures to theories, based on a theoroidal institution construction, finding that the ‘maps’ of Meseguer are
theoroidal comorphisms, while theoroidal morphisms are a new concept. We introduce ‘forward’ and ‘semi-natural’ morphisms,
and develop some of their properties. Appendices discuss institutions for partial algebra, a variant of order sorted algebra,
two versions of hidden algebra, and a generalisation of universal algebra; these illustrate various points in the main text.
A final appendix makes explicit a greater generality for the institution concept, clarifies certain details and proves some
results that lift institution theory to this level.
Received December 2000 / Accepted in revised form January 2002 |
| |
| Keywords: | : Abstract model theory Category theory Institution Kan extension Logic Specification |
| 本文献已被 SpringerLink 等数据库收录！ |
|
