×

Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. (English) Zbl 0778.68056

This is the latest version of a paper which has been circulated informally since about 1978. It provides the basic facts about order- sorted algebras (OSA’s). A second part is promised, which well treat the use of OSA’s for exception handling, error recovery, and sort constraints.
The motivation for the study of OSA is many-fold: it gives a semantic analysis for the topics of inheritance, polymorphism, meaningless expressions (such as top of the empty stack), partial operations which are total on equationally defined subsorts, and others.
We give only the basic notion. Suppose that \((S,\leq)\) is a poset. An \(S\)- sorted order-sorted algebra \(A\) is an \(S\)-sorted algebra such that \(A_ s\subseteq A_{s'}\) when \(s\leq s'\), and such that the operations \(\sigma \in \Sigma_{w,s}\cap \Sigma_{w',s'}\) satisfy the condition: if \(w\leq w'\), then \(s\leq s'\).
The paper describes an equational proof system for OSA, and gives a completeness theorem and an initial algebra construction for conditional equations. There is an existence theorem for initial algebras, and a Birkhoff variety theorem and a McKinsey-Malcev quasi-variety theorem.
Many examples relevant to computer science are given, and the paper is written in the fluid style readers have come to expect. There are only a few minor typographical errors.
Reviewer: S.Bloom (Hoboken)

MSC:

68Q55 Semantics in the theory of computing
08A70 Applications of universal algebra in computer science
06F99 Ordered structures
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Birkhoff, G., On the structure of abstract algebras, Proc. Cambridge Philos. Soc., 31, 433-454 (1935) · Zbl 0013.00105
[2] Bruce, K.; Longo, G., A modest model of records, (Proc. Symp. on Logic in Computer Science (1988), IEEE: IEEE New York), 38-50
[3] Burstall, R.; Goguen, J., Putting theories together to make specifications, (Reddy, R., Proc. 5th Internat. Joint Conf. on Artificial Intelligence (1977), Department of Computer Science, Carnegie-Mellon University), 1045-1058
[4] Burstall, R.; Goguen, J., The semantics of Clear, a specification language, (Bjorner, D., Proc. 1979 Copenhagen Winter School on Abstract Software Specification. Proc. 1979 Copenhagen Winter School on Abstract Software Specification, Lecture Notes in Computer Science, Vol. 86 (1980), Springer: Springer Berlin), 292-332 · Zbl 0456.68024
[5] Burstall, R.; MacQueen, D.; Sannella, D., Hope: an experimental applicative language, (Proc. 1st LISP Conf. (1980), Stanford University), 136-143
[6] Cardelli, L., A semantics of multiple inheritance, (Kahn, G.; MacQueen, D.; Plotkin, G., Semantics of Data Types. Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173 (1984), Springer: Springer Berlin), 51-68
[7] Cardelli, L., Structural subtyping and the notion of power type, (Proc. Symp. on Principles of Programming Languages (1988), Association for Computing Machinery: Association for Computing Machinery New York), 70-79
[8] Cardelli, L.; Wegner, P., On understanding types, data abstraction, and polymorphism, Computing Surveys, 17, 4, 471-522 (1985)
[9] Clocksin, W. F.; Mellish, C., Programming in Prolog (1981), Springer: Springer Berlin · Zbl 0466.68009
[10] Colmerauer, A.; Kanoui, H.; van Caneghem, M., Etude et réalisation d’un système Prolog, (Tech. Report, Groupe d’Intelligence Artificielle, U.E.R. de Luminy (1979), Université d’Aix-Marseille II)
[11] Cunningham, R. J.; Dick, A. J., Rewrite systems on a lattice of types, (Tech. Report (1983), Imperial College, Department of Computing) · Zbl 0575.68043
[12] Dahl, O. J.; Myhrhaug, B.; Nygaard, K., The SIMULA 67 common base language, (Tech. Report (1970), Norwegian Computing Center: Norwegian Computing Center Oslo), Publication S-22
[13] Futatsugi, K.; Goguen, J.; Jouannaud, J.-P.; Mesegeur, J., Principles of OBJ2, (Reid, B., Proc. 12th ACM Symp. on Principles of Programming Languages (1985), Association for Computing Machinery: Association for Computing Machinery New York), 52-66
[14] Futatsugi, K.; Goguen, J.; Meseguer, J.; Okada, K., Parameterized programming OBJ2, (Balzer, R., Proc. 9th Internat. Conf. on Software Engineering (1987), IEEE Computer Society Press: IEEE Computer Society Press Silver Spring, MD), 51-60
[15] Forschungsbericht Nr. 169 (1983), Universität Dortmund, Abteilung Informatik, also
[16] (Neuhold, P., Formal Description of Programming Concepts (1979), North-Holland: North-Holland Amsterdam), 491-522, also published in
[17] Goguen, J., Order sorted algebra, (Tech. Report 14, Semantics and Theory of Computation Series (1978), UCLA Computer Science Department) · Zbl 0939.68710
[18] Goguen, J., Parameterized programming, Trans. Software Engrg., SE-10, 5, 528-543 (1984) · Zbl 0545.68017
[19] Goguen, J., One, none, a hundred thousand specification languages, (Kugler, H.-J., Information Processing ’86, Proc. 1986 IFIP Congress (1986), Elsevier: Elsevier Amsterdam), 995-1003 · Zbl 0606.68010
[20] Goguen, J., Higher-order functions considered unnecessary for higher-order programming, (Turner, D., Proc. University of Texas Year of Programming, Institute of Declarative Programming (1989)), to appear; preliminary version in SRI Technical Report SRI-CSL-88-1, 1988
[21] (Clarke, E.; Kozen, D., Proc. Logics of Programming Workshop. Proc. Logics of Programming Workshop, Lecture Notes in Computer Science, Vol. 164 (1984), Springer: Springer Berlin), 221-256, also submitted for publication a preliminary version appears in
[22] Goguen, J.; Jouannaud, J.-P.; Mesegeur, J., Operational semantics of order-sorted algebra, (Brauer, W., Proc. 1985 Internat. Conf. on Automata, Languages and Programming. Proc. 1985 Internat. Conf. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 194 (1985), Springer: Springer Berlin)
[23] Goguen, J.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (Nielsen, M.; Schmidt, E. M., Proc. 9th Internat. Conf. on Automata, Languages and Programming. Proc. 9th Internat. Conf. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 140 (1982), Springer: Springer Berlin), 265-281 · Zbl 0493.68014
[24] Goguen, J.; Meseguer, J., Programming in Prolog, (Report CSLI-84-15 (1984), Center for the Study of Language and Information, Stanford University)
[25] Goguen, J.; Meseguer, J., J. Logic Programming, 1, 2, 179-210 (1984), an earlier version appears in · Zbl 0575.68091
[26] Goguen, J.; Meseguer, J., SIGPLAN Notices, 22, 4, 41-48 (1987), also in · Zbl 0498.03018
[27] Goguen, J.; Meseguer, J., SIGPLAN Notices, 21, 10, 153-162 (1986), preliminary version in
[28] Goguen, J.; Meseguer, J., Models and equality for logical programming, (Ehrig, H.; Levi, G.; Kowalski, R.; Montanari, U., Proc. 1987 TAPSOFT. Proc. 1987 TAPSOFT, Lecture Notes in Computer Science, Vol. 250 (1987), Springer: Springer Berlin), 1-22
[29] Goguen, J.; Meseguer, J., Tech. Report CSLI-87-92 (1987), Center for the Study of Language and Information, Stanford University, also
[30] Goguen, J.; Meseguer, J., Software for the rewrite rule machine, (Proc. Internat. Conf. on Fifth Generation Computer Systems 1988 (1988), Institute for New Generation Computer Technology (ICOT)), 628-637
[31] Goguen, J.; Meseguer, J.; Plaisted, D., Programming with parameterized abstract objects in OBJ, (Ferrari, D.; Bolognani, M.; Goguen, J., Theory and Practice of Software Technology (1983), North-Holland: North-Holland Amsterdam), 163-193
[32] Goguen, J.; Parsaye-Ghomi, K., Algebraic denotational semantics using parameterized abstract modules, (Formalizing Programming Concepts. Formalizing Programming Concepts, Lecture Notes in Computer Science, Vol. 107 (1981), Springer: Springer Berlin), 292-309 · Zbl 0467.68014
[33] (Gehani, N.; McGettrick, A., Software Specification Techniques (1985), Addison-Wesley: Addison-Wesley Reading, MA), 391-420, reprinted in · Zbl 0705.68039
[34] (Yeh, R., Current Trends in Programming Methodology, IV (1978), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 80-149, appears in
[35] Goguen, J.; Winkler, T., Introducing OBJ3, (Tech. Report SRI-CSL-88-9 (1988), SRI International, Computer Science Lab)
[36] Goldberg, A.; Robson, D., Languange and its Information (1983), Addison-Wesley: Addison-Wesley Reading, MA
[37] Gratzer, G., Universal Algebra (1979), Springer: Springer Berlin · Zbl 0182.34201
[38] Guiho, G., Multioperator algebras, (Proc. 2nd Workshop on Theory and Applications of Abstract Data Types (1983), Universität Passau: Universität Passau Germany)
[39] Harper, R.; MacQueen, D.; Milner, R., Standard ML, (Tech. Report ECS-LFCS-86-2 (1986), Department of Computer Science, University of Edinburgh)
[40] Hartwig, R., An algebraic approach to the syntax and semantics of languages with subscripted variables, Period. Math. Hungar., 15, 1, 61-71 (1984) · Zbl 0517.68029
[41] Higgins, P. J., Algebras with a scheme of operators, Math. Nachr., 27, 115-132 (1963) · Zbl 0117.25903
[42] Hoare, C. A.R., An axiomatic basis for computer programming, Comm. ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105
[43] Hudak, P.; Wadler, P.; Arvind, Report on the functional programming language Haskell. Tech. Report YALEU/DCS/RR-666 (December 1988), Computer Science Department, Yale University, Draft Proposed Standard
[44] Janssen, T., Foundations and applications of Montague grammar, (Ph.D. Thesis (1983), University of Amsterdam) · Zbl 0604.03001
[45] Jones, S. P., The Implementation of Functional Programming Languages (1987), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ
[46] Kamin, S.; Archer, M., Partial implementations of abstract data types: a dissenting view on errors, (Semantics of Data Types. Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173 (1984), Springer: Springer Berlin), 317-336
[47] Kirchner, C.; Kirchner, H.; Meseguer, J., Operational semantics of OBJ3, (Proc. 9th Internat. Conf. on Automata, Languages and Programming. Proc. 9th Internat. Conf. on Automata, Languages and Programming, Lecture Notes in Computer Science, Vol. 241 (1988), Springer: Springer Berlin), 287-301
[48] Kowalski, R., Logic for problem solving, (Tech. Report DCL Memo 75 (1974), Department of Artificial Intelligence, University of Edinburgh), Also, a book in the Artificial Intelligence Series (North-Holland, Amsterdam, 1979) · Zbl 0426.68002
[49] Leinwand, S.; Goguen, J.; Winkler, T., Cell and ensemble architecture of the rewrite rule machine, (Proc. Internat. Conf. on Fifth Generation Computer Systems 1988 (1988), Institute for New Generation Computer Technology (ICOT)), 869-878
[50] Lloyd, J., Foundations of Logic Programming (1984), Springer: Springer Berlin · Zbl 0547.68005
[51] Mac Lane, S., Categories for the Working Mathematician (1971), Springer: Springer Berlin · Zbl 0232.18001
[52] Meseguer, J., Order completion monads, Algebra Universalis, 16, 63-82 (1983) · Zbl 0522.18005
[53] Meseguer, J., General logics, (Ebbinghaus, H.-D., Proc. Logic Colloquium, 1987 (1989), North-Holland: North-Holland Amsterdam), 257-329
[54] Meseguer, J., Tech. Report SRI-CSL-88-13 (1988), Computer Science Lab., SRI International, longer version in
[55] Meseguer, J.; Goguen, J., Deduction with many-soted rewrite rules, (Tech. Report CSLI-85-42. Tech. Report CSLI-85-42, Theoret. Comput. Sci. (1985), Center for the Study of Language and Information, Stanford University), to appear
[56] Meseguer, J.; Goguen, J., Initiality, induction and computability, (Nivat, M.; Reynolds, J., Algebraic Methods in Semantics (1985), Cambridge University Press: Cambridge University Press Cambridge), 459-541 · Zbl 0571.68004
[57] Milner, R., A theory of type polymorphism in programming, J. Comput. System Sci., 17, 3, 348-375 (1978) · Zbl 0388.68003
[58] Montague, R., Formal Philosophy: Selected Papers of Richard Montague (1974), Yale University Press: Yale University Press Yale, edited and with an introduction by R. Thomason
[59] Mosses, P., A basic semantic algebra, (Proc. Internat. Symp. on the Semantics of Data Types. Proc. Internat. Symp. on the Semantics of Data Types, Lecture Notes in Computer Science, Vol. 173 (1985), Springer: Springer Berlin), 87-107
[60] Mosses, P., Unified algebras and institutions, (Tech. Report DAIMI PB-274 (1989), Computer Science Department, Aarhus University) · Zbl 0716.68066
[61] O’Donnell, M., Equational Logic as a Programming Language (1985), MIT Press: MIT Press Cambridge, MA · Zbl 0636.68004
[62] O’Keefe, R., Source level tools for logic programming, (Symp. on Logic Programming (1985), IEEE: IEEE New York), 68-72
[63] Parsaye-Ghomi, K., Higher order data types, (Ph.D. Thesis (1982), UCLA, Computer Science Department)
[64] Plaisted, E., An initial algebra semantics for error presentations (1982), SRI International, Computer Science Laboratory
[65] Poigné, A., On semantic algebras: higher order structures, (Informatik II (1983), Universität Dortmund)
[66] Poigné, A., Parameterization for order-sorted algebraic specification, (Tech. Report Draft (1987), Department of Computing, Imperial College) · Zbl 0694.68020
[67] (Reference manual for the Ada programming language. Reference manual for the Ada programming language, Report ANSI/MIL-STD-1815A (1983), Department of Defense, United States Government) · Zbl 0513.68005
[68] Reynolds, J., Towards a theory of type structure, (Colloquium sur la Programmation. Colloquium sur la Programmation, Lecture Notes in Computer Science, Vol. 19 (1974), Springer: Springer Berlin), 408-423
[69] Reynolds, J., Using category theory to design implicit conversions and generic operators, (Jones, N., Semantics Directed Compiler Generation. Semantics Directed Compiler Generation, Lecture Notes in Computer Science, Vol. 94 (1980), Springer: Springer Berlin), 211-258
[70] Scott, D.; Strachey, C., Towards a mathematical semantics for computer languages, (Proc. 21st Symp. on Computers and Automata (1971), Polytechnic Institute of Brooklyn), 19-46, also appeared as Technical Monograph PRG 6, Oxford University, Programming Research Group
[71] Smolka, G., Order-sorted horn logic: semantics and deduction, (Tech. Report SEKI-Report Sr-86-17 (1986), Fachbereich Informatik, Universitat Kaiserslautern)
[72] Smolka, G.; Nutt, W.; Goguen, J.; Meseguer, J., SEKI Report SR-87-14 (1987), Universität Kaiserslautern, also appears as
[73] Sterling, L.; Shapiro, E., The Art of Prolog (1986), MIT Press: MIT Press Cambridge, MA · Zbl 0605.68002
[74] Stoy, J., Denotational Semantics of Programming Languages (1977), MIT Press: MIT Press Cambridge, MA
[75] Strachey, C., Fundamental concepts in programming languages, Lecture Notes from International Summer School in Computer Programming, Copenhagen (1967)
[76] Touretzky, D. S., The mathematics of inheritance systems, (Ph.D. Thesis (1984), Carnegie-Mellon University) · Zbl 0675.68006
[77] Turner, D., a non-strict functional language with polymorphic types, (Jouannaud, J.-P., Functional Programming Languages and Computer Architectures. Functional Programming Languages and Computer Architectures, Lecture Notes in Computer Science, Vol. 201 (1985), Springer: Springer Berlin), 1-16 · Zbl 0592.68014
[78] Wadge, W., Classified algebras, (Tech. Report 46 (1982), University of Warwick)
[79] Walther, C., A many-sorted calculus based on resolution and paramodulation, (Proc. 8th Internat. Joint Conf. on Artificial Intelligence (1983), Morgan Kaufman: Morgan Kaufman Los Altos, CA), 882-891
[80] Walther, C., A classification of many-sorted unification theories, (Proc. 8th Internat. Conf. on Automated Deduction. Proc. 8th Internat. Conf. on Automated Deduction, Lecture Notes in Computer Science, Vol. 230 (1986), Springer: Springer Berlin), 525-537
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.