# Introducing institutions

## Abstract

There is a population explosion among the logical systems being used in computer science. Examples include first order logic (with and without equality), equational logic, Horn clause logic, second order logic, higher order logic, infinitary logic, dynamic logic, process logic, temporal logic, and modal logic; moreover, there is a tendency for each theorem prover to have its own idiosyncratic logical system. Yet it is usual to give many of the same results and applications for each logical system; of course, this is natural in so far as there are basic results in computer science that are independent of the logical system in which they happen to be expressed. But we should not have to do the same things over and over again; instead, we should generalize, and do the essential things once and for all! Also, we should ask what are the relationships among all these different logical systems. This paper shows how some parts of computer science can be done in any suitable logical system, by introducing the notion of an institution as a precise generalization of the informal notion of a "logical system." A first main result shows that if an institution is such that interface declarations expressed in it can be glued together, then theories (which are just sets of sentences) in that institution can also be glued together. A second main result gives conditions under which a theorem prover for one institution can be validly used on theories from another; this uses the notion of an institution morphism. A third main result shows that institutions admiting free models can be extended to institutions whose theories may include, in addition to the original sentences, various kinds of constraints upon interpretations; such constraints are useful for defining abstract data types, and include so-called "data," "hierarchy," and "generating" constraints. Further results show how to define insitutions that mix sentences from one institution with constraints from another, and even mix sentences and (various kinds of) constraints from several different institutions. It is noted that general results about institutions apply to such "multiplex" institutions, including the result mentioned above about gluing together theories. Finally, this paper discusses some applications of these results to specification languages, showing that much of that subject is in fact independent of the institution used.

## Keywords

Specification Language Order Logic Logical System Predicate Symbol Horn Clause## Preview

Unable to display preview. Download preview PDF.

## References

- [Arbib & Manes 75]Arbib, M. A. and Manes, E.
*Arrows, Structures and Functors*. Academic Press, 1975.Google Scholar - [Aubin 76]Aubin, R.
*Mechanizing Structural Induction*. PhD thesis, University of Edinburgh, 1976.Google Scholar - [Barwise 74]Barwise, J. Axioms for Abstract Model Theory.
*Annals of Mathematical Logic*7:221–265, 1974.Google Scholar - [Benabou 68]Benabou, J. Structures Algebriques dans les Categories.
*Cahiers de Topologie et Geometrie Differentiel*10:1–126, 1968.Google Scholar - [Birkhoff & Lipson 70]Birkhoff, G. and Lipson, J. Heterogeneous Algebras.
*Journal of Combinatorial Theory*8:115–133, 1970.Google Scholar - [Bloom 76]Bloom, S. L. Varieties of Ordered Algebras.
*Journal of Computer and System Sciences*13:200–212, 1976.Google Scholar - [Boyer & Moore 80]Boyer, R. and Moore, J. S.
*A Computational Logic*. Academic Press, 1980.Google Scholar - [Broy, Dosch, Partsch, Pepper & Wirsing 79]Broy, M., Dosch, N., Partsch, H., Pepper, P. and Wirsing, M. Existential Quantifiers in Abstract Data Types. In
*Proceedings, 6th ICALP*, pages 73–87. Springer-Verlag, 1979. Lecture Notes in Computer Science, volume 71.Google Scholar - [Burstall & Goguen 77]Burstall, R. M. and Goguen, J. A. Putting Theories together to Make Specifications.
*Proceedings, Fifth International Joint Conference on Artificial Intelligence*5:1045–1058, 1977.Google Scholar - [Burstall & Goguen 78]Burstall, R. M. and Goguen, J. A. Semantics of Clear. 1978. Unpublished notes handed out at the Symposium on Algebra and Applications, Stefan Benach Center, Warszawa, Poland.Google Scholar
- [Burstall & Goguen 80]Burstall, R. M., and Goguen, J. A. The Semantics of Clear, a Specification Language. In
*Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification*, pages 292–332. Springer-Verlag, 1980. Lecture Notes in Computer Science, Volume 86.Google Scholar - [Burstall & Goguen 81]Burstall, R. M. and Goguen, J. A. An Informal Introduction to Specifications using Clear. In Boyer, R. and Moore, J (editor),
*The Correctness Problem in Computer Science*, pages 185–213. Academic Press, 1981.Google Scholar - [Burstall & Goguen 82]Burstall, R. M. and Goguen, J. A. Algebras, Theories and Freeness: An Introduction for Computer Scientists. In
*Proceedings, 1981 Marktoberdorf NATO Summer School*,. Reidel, 1982.Google Scholar - [Burstall & Rydeheard 80]Burstall, R. M. and Rydeheard, D. E.
*Signatures, Presentations and Theories: a Monad Approach*. Technical Report, Computer Science Department, University of Edinburgh, 1980.Google Scholar - [Clark 78]Clark, K. L. Negation as Failure. In H. Gallaire and J. Minker (editor),
*Logic in Data Bases*, pages 293–322. Plenum Press, 1978.Google Scholar - [Cohn 65]Cohn, P. M.
*Universal Algebra*. Harper and Row, 1965. Revised edition 1980.Google Scholar - [Ehrich 78]Ehrich, H.-D.
*On the Theory of Specification, Implementation and Parameterization of Abstract Data Types*. Technical Report, Forschungsbericht, Dortmund, 1978.Google Scholar - [Ehrig, Kreowski, Rosen & Winkowski 78]Ehrig, E., Kreowski, H.-J., Rosen, B. K. and Winkowski, J. Deriving Structures from Structures. In
*Proceedings, Mathematical Foundations of Computer Science*, Springer-Verlag, Zakopane, Poland, 1978. Also appeared as technical report RC7046 from IBM Watson Research Center, Computer Sciences Dept.Google Scholar - [Ehrig, Wagner & Thatcher 82]Ehrig, H., Wagner, E. and Thatcher, J.
*Algebraic Specifications with Generating Constraints*. Technical Report, IBM Research Center, Yorktown Heights, New York, 1982. Draft report.Google Scholar - [Gabriel & Ulmer 71]Gabriel, P. and Ulmer, F.
*Lokal Prasentierbare Kategorien*. Springer-Verlag, 1971. Springer Lecture Notes in Mathematics, vol. 221.Google Scholar - [Gerhard, Musser et al. 79]Gerhard, S. L., Musser, D. R., Thompson, D. H., Baker, D. A., Bates, R. W., Erickson, R. W., London, R. L., Taylor, D. G., and Wile, D. S.
*An Overview of AFFIRM: A Specification and Verification System*. Technical Report, USC Information Sciences Institute, Marina del Rey, CA, 1979.Google Scholar - [Goguen 71]Goguen, J. Mathematical Foundations of Hierarchically Organized Systems. In E. Attinger (editor),
*Global Systems Dynamics*, pages 112–128. S. Karger, 1971.Google Scholar - [Goguen 74]Goguen, J. A. Semantics of Computation. In
*Proceedings, First International Symposium on Category Theory Applied to Computation and Control*, pages 234–249. University of Massachusetts at Amherst, 1974. Also published in Lecture Notes in Computer Science, Vol. 25., Springer-Verlag, 1975, pp. 151–163.Google Scholar - [Goguen 77]Goguen, J. A. Abstract Errors for Abstract Data Types. In
*IFIP Working Conference on Formal Description of Programming Concepts*,. MIT, 1977. Also published by North-Holland, 1979, edited by P. Neuhold.Google Scholar - [Goguen 78]Goguen, J. A.
*Order Sorted Algebra*. Technical Report, UCLA Computer Science Department, 1978. Semantics and Theory of Computation Report No. 14; to appear in*Journal of Computer and System Science*.Google Scholar - [Goguen 80]Goguen, J. A. How to Prove Algebraic Inductive Hypotheses without Induction: with applications to the correctness of data type representations. In W. Bibel and R. Kowalski (editor),
*Proceedings, 5th Conference on Automated Deduction*, pages 356–373. Springer-Verlag, Lecture Notes in Computer Science, Volume 87, 1980.Google Scholar - [Goguen 82a]Goguen, J. A. Ordinary Specification of Some Construction in Plane Geometry. In Staunstrup, J. (editor),
*Proceedings, Workshop on Program Specification*, pages 31–46. Springer-Verlag, 1982. Lecture Notes in Computer Science, Volume 134.Google Scholar - [Goguen 82b]Goguen, J. A. Ordinary Specification of KWIC Index Generation. In Staunstrup, J. (editor),
*Proceedings, Aarhus Workshop on Specification*, pages 114–117. Springer-Verlag, 1982. Lecture Notes in Computer Science, Volume 134.Google Scholar - [Goguen & Burstall 78]Goguen, J. A. and Burstall, R. M.
*Some Fundamental Properties of Algebraic Theories: a Tool for Semantics of Computation*. Technical Report, Dept. of Artificial Intelligence, University of Edinburgh, 1978. DAI Research Report No. 5; to appear in*Theoretical Computer Science*.Google Scholar - [Goguen & Ginali 78]Goguen, J. A. and Ginali, S. A Categorical Approach to General Systems Theory. In Klir, G. (editor),
*Applied General Systems Research*, pages 257–270. Plenum, 1978.Google Scholar - [Goguen & Meseguer 81]Goguen, J. A. and Meseguer, J. Completeness of Many-sorted Equational Logic.
*SIGPLAN Notices*16(7):24–32, July, 1981. Also appeared in*SIGPLAN Notices*, January 1982, vol. 17, no. 1, pages 9–17; extended version as SRI Technical Report, 1982, and to be published in*Houston Journal of Mathematics*.Google Scholar - [Goguen & Meseguer 83]Goguen, J. A. and Meseguer, J. An Initiality Primer. In Nivat, M. and Reynolds, J. (editor),
*Application of Algebra to Language Definition and Compilation*, North-Holland, 1983. To appear.Google Scholar - [Goguen & Parsaye-Ghomi 81]Goguen, J. A. and Parsaye-Ghomi, K. Algebraic Denotational Semantics using Parameterized Abstract Modules. In J. Diaz and I. Ramos (editor),
*Formalizing Programming Concepts*, pages 292–309. Springer-Verlag, Peniscola, Spain, 1981. Lecture Notes in Computer Science, volume 107.Google Scholar - [Goguen & Tardo 79]Goguen, J. A. and Tardo, J. An Introduction to OBJ: A Language for Writing and Testing Software Specifications. In
*Specification of Reliable Software*, pages 170–189. IEEE, 1979.Google Scholar - [Goguen, Thatcher & Wagner 78]Goguen, J. A., Thatcher, J. W. and Wagner, E. An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types. In R. Yeh (editor),
*Current Trends in Programming Methodology*, pages 80–149. Prentice-Hall, 1978. Original version, IBM T. J. Watson Research Center Technical Report RC 6487, October 1976.Google Scholar - [Goguen, Thatcher, Wagner & Wright 75a]Goguen, J. A., Thatcher, J. W., Wagner, E. G., and Wright, J. B.
*An Introduction to Categories, Algebraic Theories and Algebras*. Technical Report, IBM T. J. Watson Research Center, Yorktown Heights, N. Y., 1975. Research Report RC 5369.Google Scholar - [Goguen, Thatcher, Wagner & Wright 75b]Goguen, J. A., Thatcher, J. W., Wagner, E. and Wright, J. B. Abstract Data Types as Initial Algebras and the Correctness of Data Representations. In
*Computer Graphics, Pattern Recognition and Data Structure*, pages 89–93. IEEE, 1975.Google Scholar - [Goldblatt 79]Goldblatt, R.
*Topoi, The Categorial Analysis of Logic*. North-Holland, 1979.Google Scholar - [Higgins 63]Higgins, P. J. Algebras with a Scheme of Operators.
*Mathematische Nachrichten*27:115–132, 1963.Google Scholar - [Hoare 72]Hoare, C. A. R. Proof of Correctness of Data Representation.
*Acta Informatica*1:271–281, 1972.Google Scholar - [Kaphengst & Reichel 71]Kaphengst, H. and Reichel, H.
*Algebraische Algorithemtheorie*. Technical Report WIB Nr. 1, VEB Robotron, Zentrum fur Forschung und Technik, Dresden, 1971. In German.Google Scholar - [Landin 66]Landin, P. J. The Next 700 Programming Languages.
*Communications of the Association for Computing Machinery*9, 1966.Google Scholar - [Lawvere 63]Lawvere, F. W. Functorial Semantics of Algebraic Theories.
*Proceedings, National Academy of Sciences*50, 1963. Summary of Ph.D. Thesis, Columbia University.Google Scholar - [Lawvere 64]Lawvere, F. W. An Elementary Theory of the Category of Sets.
*Proceedings, National Academy of Sciences, U.S.A.*52:1506–1511, 1964.Google Scholar - [Levitt, Robinson & Silverberg 79]Levitt, K., Robinson, L. and Silverberg, B.
*The HDM Handbook*. Technical Report, SRI, International, Computer Science Lab, 1979. Volumes I, II, III.Google Scholar - [MacLane 71]MacLane, S.
*Categories for the Working Mathematician*. Springer-Verlag, 1971.Google Scholar - [MacLane & Birkhoff 67]MacLane, S. and Birkhoff, G.
*Algebra*. Macmillan, 1967.Google Scholar - [Mahr & Makowsky 82a]Mahr, B. and Makowsky, J. A.
*An Axiomatic Approach to Semantics of Specification Languages*. Technical Report, Technion, Israel Institute of Technology, 1982. Extended Abstract.Google Scholar - [Mahr & Makowsky 82b]Mahr, B. and Makowsky, J. A.
*Characterizing Specification Languages which Admit Initial Semantics*. Technical Report, Technion, Israel Institute of Technology, February, 1982. Technical Report #232.Google Scholar - [McCarthy 80]McCarthy, J. Circumscription — A Form of Non-Monotonic Reasoning.
*Artificial Intelligence*13(1,2):27–39, 1980.Google Scholar - [Parsaye-Ghomi 82]Parsaye-Ghomi, K.
*Higher Order Data Types*. PhD thesis, UCLA, Computer Science Department, January, 1982.Google Scholar - [Reichel 80]Reichel, H. Initially Restricting Algebraic Theories.
*Springer Lecture Notes in Computer Science*88:504–514, 1980. Mathematical Foundations of Computer Science.Google Scholar - [Shostak, Schwartz & Melliar-Smith 81]Shostak, R., Schwartz, R. & Melliar-Smith, M.
*STP: A Mechanized Logic for Specification and Verification*. Technical Report, Computer Science Lab, SRI International, 1981.Google Scholar - [Tarski 44]Tarski, A. The Semantic Conception of Truth.
*Philos. Phenomenological Research*4:13–47, 1944.Google Scholar - [Thatcher, Wagner & Wright 79]Thatcher, J. W., Wagner, E. G. and Wright, J. B. Data Type Specification: Paramerization and the Power of Specification Techniques. In
*Proceedings of 1979 POPL*,. ACM, 1979.Google Scholar - [Wright, Thatcher, Wagner & Goguen 76]Wright, J. B., Thatcher, J. W., Wagner, E. G. and Goguen, J. A. Rational Algebraic Theories and Fixed-Point Solutions.
*Proceedings, 17th Foundations of Computing Symposium*:147–158, 1976. IEEE.Google Scholar