Hostname: page-component-745bb68f8f-b6zl4 Total loading time: 0 Render date: 2025-01-24T06:36:06.321Z Has data issue: false hasContentIssue false
  • English
  • Français

An Oxford survey of order sorted algebra†

Published online by Cambridge University Press:  04 March 2009

Joseph Goguen  and
Răzvan Diaconescu
Joseph Goguen
Affiliation:
Programming Research Group, Oxford University
Răzvan Diaconescu
Affiliation:
Programming Research Group, Oxford University
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper surveys several different variants of order sorted algebra (abbreviated OSA), comparing some of the main approaches (overloaded OSA, universe OSA, unified algebra, term declaration algebra, etc.), emphasising motivation and intuitions, and pointing out features that distinguish the original ‘overloaded’ OSA approach from some later developments. These features include sort constraints and retracts; the latter is particularly useful for handling multiple data representations (including automatic coercions among them). Many examples are given, for most of which, runs are shown on the OBJ3 system.

This paper also significantly generalises overloaded OSA by dropping the regularity and monotonicity assumptions, and by adding signatures of non-monotonicities, which support simple semantics for some aspects of object oriented programming. A number of new results for this generalisation are proved, including initiality, variety, and quasi-variety theorems. Axiomatisability results à la Birkhoff are also proved for unified algebras.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 4 , Issue 3 , September 1994 , pp. 363 - 392
Copyright
Copyright © Cambridge University Press 1994

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aczel, P. (1990) Term Declaration Logic and Generalised Composita, University of Manchester (draft).Google Scholar
Andréka, H. and Németi, I. (1981) A General Axiomatizability Theorem Formulated in Terms of Cone-Injective Subcategories. In: Csakany, B., Fried, E. and Schmidt, E. T. (eds.), Universal Algebra. Colloquia Mathematics Societas János Bolyai 29, North-Holland13–35.Google Scholar
Antimirov, V. and Degtyarev, A. (1992) Consistency of Equational Enrichments. Proceedings, CRTS’92, St. Petersberg. Springer-Verlag Lecture Notes in Computer Science.Google Scholar
Benabou, J. (1968) Structures Algébriques dans les Catégories. Cahiers de Topologie et Géometrie Différentiel 10 1–126.Google Scholar
Birkhoff, G. (1935) On the Structure of Abstract Algebras. Proceedings of the Cambridge Philosophical Society 31 433–454.CrossRefGoogle Scholar
Burstall, R. and Diaconescu, R. (1992) Hiding and Behaviour: an Institutional Approach, Technical report ECS-LFCS-8892–253, Laboratory for Foundations of Computer Science, University of Edinburgh. (Also in Roscoe, A. W. (ed.) (1994) A Classical Mind: Essays in Honour of C. A. R. Hoare Prentice-Hall.)Google Scholar
Diaconescu, R. (1992) The Formal Completeness of Equational Logics, Technical report PRG-TR- 12–92, Programming Research Group, Oxford University.Google Scholar
Diaconescu, R., Goguen, J. and Stefaneas, P. (1993) Logical Support for Modularisation. In: Huet, G., AND Plotkin, G. (eds.) Logical Environments, Proceedings of a Workshop held in Edinburgh, Scotland, May 1991, Cambridge University Press 83–130.Google Scholar
Gogolla, M. (1984) Partially Ordered Sorts in Algebraic Specifications. In: Courcelle, B. (ed.) Proceedings, Ninth CAAP (Bordeaux), Cambridge University Press 139–153. (Also Forschungsbericht 169 Universität Dortmund, Abteilung Informatik, 1983.)Google Scholar
Goguen, J. (1974) Semantics of Computation. In: Manes, E. G. (ed.) Proceedings, First International Symposium on Category Theory Applied to Computation and Control, University of Massachusetts at Amherst234–249. (Also in Springer-Verlag Lecture Notes in Computer Science 25 151–163.)Google Scholar
Goguen, J. (1978) Order Sorted Algebra, Technical Report 14, UCLA Computer Science Department (Semantics and Theory of Computation Series).Google Scholar
Goguen, J. (1991) Types as Theories. In: Reed, G. M., Roscoe, A. W. and Wachter, R. F. (eds.) Topology and Category Theory in Computer Science (Proceedings of a Conference held at Oxford, June 1989), Oxford University Press 357–390.CrossRefGoogle Scholar
Goguen, J. (1994) Theorem Proving and Algebra, MIT (to appear).Google Scholar
Goguen, J. and Burstall, R. (1985) Institutions: Abstract Model Theory for Specification and Programming. Journal of the Association for Computing Machinery 39 (1) 95–146. (Draft appears as Report ECS-LFCS-90–106, Computer Science Department, University of Edinburgh, January 1990. An early ancestor is ‘Introducing Institutions’ in: Clarke, E. and Kozen, D. (eds.) (1984) Proceedings, Logics of Programming Workshop, Springer-Verlag Lecture Notes in Computer Science 164 221–256.)CrossRefGoogle Scholar
Goguen, J. and Diaconescu, R. (1993) Towards an Algebraic Semantics for the Object Paradigm. Proceedings, Tenth Workshop on Abstract Data Types, Springer-Verlag.Google Scholar
Goguen, J., Jouannaud, J.-P. and Meseguer, J. (1985) Operational Semantics of Order-Sorted Algebra. In: Brauer, W. (ed.) Proceedings, 1985 International Conference on Automata, Languages and Programming. Springer-Verlag Lecture Notes in Computer Science 194.CrossRefGoogle Scholar
Goguen, J. and Malcolm, G. (1994) Proof of Correctness of Object Representation. In: Roscoe, A. W. (ed.) A Classical Mind: Essays in Honour of C. A. R. Hoare, Prentice-Hall 119–142.Google Scholar
Goguen, J. and Meseguer, J. (1982) Universal Realization, Persistent Interconnection and Implementation of Abstract Modules. In: Nielsen, M. and Schmidt, E. M. (eds.) Proceedings, 9th International Conference on Automata, Languages and Programming, Aarhus, Denmark. Springer-Verlag Lecture Notes in Computer Science 140 265–281.CrossRefGoogle Scholar
Goguen, J. and Meseguer, J. (1985) Completeness of Many-sorted Equational Logic. Houston Journal of Mathematics 11 (3) 307–334. (Preliminary versions have appeared in: SIGPLAN Notices (1981) 16 (7) 24–37; Technical Report CSL-135 (1982) SRI Computer Science Lab; and Technical Report CSLI-84–15 (1984) Center for the Study of Language and Information, Stanford University.)Google Scholar
Goguen, J. and Meseguer, J. (1986a) Eqlog: Equality, Types, and Generic Modules for Logic Programming. In: DeGroot, D. and Lindstrom, G. (eds.) Logic Programming: Functions, Relations and Equations, Prentice-Hall, 295–363, (An earlier version appears in Journal of Logic Programming (1984) 1 (2) 179–210.)Google Scholar
Goguen, J. and Meseguer, J. (1986b) Remarks on Remarks on Many-Sorted Equational Logic. Bulletin of the European Association for Theoretical Computer Science 30 66–73. (Also in SIGPLAN Notices 22 (4) 41–48.)Google Scholar
Goguen, J. and Meseguer, J. (1987a) Models and Equality for Logical Programming. In: Ehrig, H., Levi, G., Kowalski, R. and Montanari, U. (eds.) Proceedings, 1987 TAPSOFT, Pisa, Italy. Springer- Verlag Lecture Notes in Computer Science 250 1–22. (Also, Report CSLI-87–91 (1987) Center for the Study of Language and Information, Stanford University; reprinted in Mathematical Logic in Programming, Mir (Moscow) (1991) 274–310 (in Russian).)CrossRefGoogle Scholar
Goguen, J. and Meseguer, J. (1987b) Order-Sorted Algebra Solves the Constructor Selector, Multiple Representation and Coercion Problems. In: Proceedings, Second Symposium on Logic in Computer Science, Ithaca NY, IEEE Computer Society 18–29. (Also: Report CSLI-87–92 (1987) Center for the Study of Language and Information, Stanford University; revised version in Information and Computation 103.)Google Scholar
Goguen, J. and Meseguer, J. (1987c) Unifying Functional, Object-Oriented and Relational Programming, with Logical Semantics. In: Shriver, B. and Wegner, P. (eds.) Research Directions in Object-Oriented Programming, MIT 417–477. (Preliminary version in SIGPLAN Notices 21 (10) 153–162. Also, Report CSLI-87–93 (1987) Center for the Study of Language and Information, Stanford University.)Google Scholar
Goguen, J. and Meseguer, J. (1992) Order-Sorted Algebra I: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations. Theoretical Computer Science 105 (2) 217–273. (Also: Programming Research Group Technical Monograph PRG-80 (1989) Oxford University, and Technical Report SRI-CSL-89–10 (1989) SRI International, Computer Science Lab; originally given as lecture at Seminar on Types, Carnegie-Mellon University, June 1983; many draft versions exist, from as early as 1985.)CrossRefGoogle Scholar
Goguen, J., Stevens, A., Hobley, K. and Hilberdink, H. (1992) 2OBJ, a Metalogical Framework based on Equational Logic. Philosophical Transactions of the Royal Society Series A 339 69–86. (Also in Hoare, C. A. R. and Gordon, M. J. C. (eds.) (1992) Mechanized Reasoning and Hardware Design, Prentice-Hall, 69–86.)Google Scholar
Goguen, J., Thatcher, J. and Wagner, E. (1976) An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types. Technical Report RC 6487, IBM T. J. Watson Research Center. (Also in Yeh, R. (ed.) (1978) Current Trends in Programming Methodology, IV, Prentice-Hall 80–149.)Google Scholar
Goguen, J., Thatcher, J., Wagner, E. and Wright, J. (1977) Initial Algebra Semantics and Continuous Algebras. Journal of the Association for Computing Machinery 24 (1) 68–95. An early version is ‘Initial Algebra Semantics’, Technical Report RC 4865 (1974), IBM T. J. Watson Research Center.)CrossRefGoogle Scholar
Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K. and Jouannaud, J.-P. (1994) Introducing OBJ. In: Goguen, J. (ed.) Applications of Algebraic Specification using OBJ, Cambridge University Press, (Also to appear as Technical Report from SRI International.)Google Scholar
Goguen, J. and Wolfram, D. (1991) On Types and FOOPS. In: Meersman, R., Kent, W. and Khosla, S. (eds.) Object Oriented Databases: Analysis, Design and Construction (Proceedings, IFIP TC2 Conference, Windermere, UK 1990), North-Holland1–22.Google Scholar
Halmos, P. R. (1963) Lectures on Boolean Algebras (Mathematical Studies, Volume 1), Van Nostrand.Google Scholar
Harper, R., MacQueen, D. and Milner, R. (1986) Standard ML, Technical Report ECS-LFCS-86–2, Department of Computer Science, University of Edinburgh.Google Scholar
Higgins, P. J. (1963) Algebras with a Scheme of Operators. Mathematische Nachrichten 27 115–132.CrossRefGoogle Scholar
Isakowitz, T. (1989) Theorem Proving Methods for Order Sorted Logic, Ph.D. thesis, University of Pennsylvania. (Also appeared in Logic in Computer Science ‘89 304–312.)Google Scholar
Lawvere, F. W. (1963) Functorial Semantics of Algebraic Theories. Proceedings, National Academy of Sciences, U.S.A. 50 869–872. (Summary of Ph.D. Thesis, Columbia University.)CrossRefGoogle ScholarPubMed
Meseguer, J. and Goguen, J. (1985) Deduction with Many-Sorted Rewrite Rules, Technical Report CSLI-85–42, Center for the Study of Language and Information, Stanford University. (To appear in Theoretical Computer Science.)Google Scholar
Mosses, P. (1989a) Unified Algebras and Action Semantics. Proceedings, Symposium on Theoretical Aspects of Computer Science. Springer-Verlag Lecture Notes in Computer Science 349.CrossRefGoogle Scholar
Mosses, P. (1989b) Unified Algebras and Institutions. In: Proceedings, Fourth Annual Conference on Logic in Computer Science, IEEE 304–312.Google Scholar
Mosses, P. (1989c) Unified Algebras and Modules. In: Proceedings 16th Annual ACM Symposium on Principles of Programming Languages, ACM 329–343.Google Scholar
Poigné, A. (1984) Another Look at Parametrization using Algerbaic Specifications with Subsorts. Proceedings, Mathematical Foundations of Computer Science ‘84. Springer-Verlag Lecture Notes in Computer Science 176.CrossRefGoogle Scholar
Poigné, A. (1990) Once More on Order-Sorted Algebra, Technical Report Draft, GMD.CrossRefGoogle Scholar
Reichel, H. (1981) Behavioural Equivalence-A Unifying Concept for Initial and Final Specifications. In: Arata, M. and Varga, L. (eds.) Proceedings, Third Hungarian Computer Science Conference, Akademiai Kiado, Budapest.Google Scholar
Sannella, D. and Tarlecki, A. (1988) Specifications in an Arbitrary Institution. Information and Control 76 165–210. (Earlier version in Proceedings, International Symposium on the Semantics of Data Types (1985). Springer-Verlag Lecture Notes in Computer Science 173.)Google Scholar
Schmidt-Schauss, M. (1989) Computational Aspects of an Order-Sorted Logic with Term Declarations. Springer-Verlag Lecture Notes in Artificial Intelligence 395.Google Scholar
Smolka, G. (1986) Order-Sorted Horn Logic: Semantics and Deduction, Technical Report SEKI SR-86–17 Report, Fachbereich Informatik, Universität Kaiserslautern.Google Scholar
Smolka, G., Nutt, W., Goguen, J. and Meseguer, J. (1989) Order-Sorted Equational Computation. In: Nivat, M. and Aït-Kaci, H. (eds.) Resolution of Equations in Algebraic Structures, Volume 2: Rewriting Techniques, Academic Press. (Preliminary version in Proceedings, Colloquium on the Resolution of Equations in Algebraic Structures, held in Lakeway, Texas, 1987; and SEKI Report SR-87–14, Universität Kaiserslautern (1987) 299–367.)Google Scholar
Strachey, C. (1967) Fundamental Concepts in Programming Languages, Lecture Notes from International Summer School in Computer Programming, Copenhagen.Google Scholar
Waldmann, U. (1992) Semantics of order-sorted specifications. Theoretical Computer Science 94 (1) 1–35.CrossRefGoogle Scholar
Walther, C. (1985) A Mechanical Solution of Schubert's Steamroller by Many-sorted Resolution. Artificial Intelligence 26 (2) 217–214.CrossRefGoogle Scholar
Walther, C. (1990) Many-Sorted Inferences in Automated Theorem Proving. In: Sorts and Types in Artificial Intelligence. Springer-Verlag Lecture Notes in Artificial Intelligence 418 18–48.Google Scholar
Whitehead, A. N. (1898) A Treatise on Universal Algebra, with Applications, I, Cambridge University Press. (Reprinted 1960.)Google Scholar
Yan, H. (1994) Theory and Implementation of Sort Constraints for Order Sorted Algebra, D. Phil. thesis, Programming Research Group, Oxford University.Google Scholar