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.
Research supported in part by Office of Naval Research contracts N00014-80-0296 and N00014-82-C-0333, and National Science Foundation Grant MCS8201380.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Arbib, M. A. and Manes, E. Arrows, Structures and Functors. Academic Press, 1975.
Aubin, R. Mechanizing Structural Induction. PhD thesis, University of Edinburgh, 1976.
Barwise, J. Axioms for Abstract Model Theory. Annals of Mathematical Logic 7:221–265, 1974.
Benabou, J. Structures Algebriques dans les Categories. Cahiers de Topologie et Geometrie Differentiel 10:1–126, 1968.
Birkhoff, G. and Lipson, J. Heterogeneous Algebras. Journal of Combinatorial Theory 8:115–133, 1970.
Bloom, S. L. Varieties of Ordered Algebras. Journal of Computer and System Sciences 13:200–212, 1976.
Boyer, R. and Moore, J. S. A Computational Logic. Academic Press, 1980.
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.
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.
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.
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.
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.
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.
Burstall, R. M. and Rydeheard, D. E. Signatures, Presentations and Theories: a Monad Approach. Technical Report, Computer Science Department, University of Edinburgh, 1980.
Clark, K. L. Negation as Failure. In H. Gallaire and J. Minker (editor), Logic in Data Bases, pages 293–322. Plenum Press, 1978.
Cohn, P. M. Universal Algebra. Harper and Row, 1965. Revised edition 1980.
Ehrich, H.-D. On the Theory of Specification, Implementation and Parameterization of Abstract Data Types. Technical Report, Forschungsbericht, Dortmund, 1978.
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.
Ehrig, H., Wagner, E. and Thatcher, J. Algebraic Specifications with Generating Constraints. Technical Report, IBM Research Center, Yorktown Heights, New York, 1982. Draft report.
Gabriel, P. and Ulmer, F. Lokal Prasentierbare Kategorien. Springer-Verlag, 1971. Springer Lecture Notes in Mathematics, vol. 221.
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.
Goguen, J. Mathematical Foundations of Hierarchically Organized Systems. In E. Attinger (editor), Global Systems Dynamics, pages 112–128. S. Karger, 1971.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Goldblatt, R. Topoi, The Categorial Analysis of Logic. North-Holland, 1979.
Higgins, P. J. Algebras with a Scheme of Operators. Mathematische Nachrichten 27:115–132, 1963.
Hoare, C. A. R. Proof of Correctness of Data Representation. Acta Informatica 1:271–281, 1972.
Kaphengst, H. and Reichel, H. Algebraische Algorithemtheorie. Technical Report WIB Nr. 1, VEB Robotron, Zentrum fur Forschung und Technik, Dresden, 1971. In German.
Landin, P. J. The Next 700 Programming Languages. Communications of the Association for Computing Machinery 9, 1966.
Lawvere, F. W. Functorial Semantics of Algebraic Theories. Proceedings, National Academy of Sciences 50, 1963. Summary of Ph.D. Thesis, Columbia University.
Lawvere, F. W. An Elementary Theory of the Category of Sets. Proceedings, National Academy of Sciences, U.S.A. 52:1506–1511, 1964.
Levitt, K., Robinson, L. and Silverberg, B. The HDM Handbook. Technical Report, SRI, International, Computer Science Lab, 1979. Volumes I, II, III.
MacLane, S. Categories for the Working Mathematician. Springer-Verlag, 1971.
MacLane, S. and Birkhoff, G. Algebra. Macmillan, 1967.
Mahr, B. and Makowsky, J. A. An Axiomatic Approach to Semantics of Specification Languages. Technical Report, Technion, Israel Institute of Technology, 1982. Extended Abstract.
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.
McCarthy, J. Circumscription — A Form of Non-Monotonic Reasoning. Artificial Intelligence 13(1,2):27–39, 1980.
Parsaye-Ghomi, K. Higher Order Data Types. PhD thesis, UCLA, Computer Science Department, January, 1982.
Reichel, H. Initially Restricting Algebraic Theories. Springer Lecture Notes in Computer Science 88:504–514, 1980. Mathematical Foundations of Computer Science.
Shostak, R., Schwartz, R. & Melliar-Smith, M. STP: A Mechanized Logic for Specification and Verification. Technical Report, Computer Science Lab, SRI International, 1981.
Tarski, A. The Semantic Conception of Truth. Philos. Phenomenological Research 4:13–47, 1944.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Goguen, J.A., Burstall, R.M. (1984). Introducing institutions. In: Clarke, E., Kozen, D. (eds) Logics of Programs. Logic of Programs 1983. Lecture Notes in Computer Science, vol 164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12896-4_366
Download citation
DOI: https://doi.org/10.1007/3-540-12896-4_366
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12896-0
Online ISBN: 978-3-540-38775-6
eBook Packages: Springer Book Archive