×

zbMATH — the first resource for mathematics

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 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, (), 38-50
[3] Burstall, R.; Goguen, J., Putting theories together to make specifications, (), 1045-1058
[4] Burstall, R.; Goguen, J., The semantics of clear, a specification language, (), 292-332 · Zbl 0456.68024
[5] Burstall, R.; MacQueen, D.; Sannella, D., Hope: an experimental applicative language, (), 136-143
[6] Cardelli, L., A semantics of multiple inheritance, (), 51-68
[7] Cardelli, L., Structural subtyping and the notion of power type, (), 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 Berlin · Zbl 0466.68009
[10] Colmerauer, A.; Kanoui, H.; van Caneghem, M., Etude et réalisation d’un système prolog, ()
[11] Cunningham, R.J.; Dick, A.J., Rewrite systems on a lattice of types, () · Zbl 0575.68043
[12] Dahl, O.J.; Myhrhaug, B.; Nygaard, K., The SIMULA 67 common base language, (), Publication S-22
[13] Futatsugi, K.; Goguen, J.; Jouannaud, J.-P.; Mesegeur, J., Principles of OBJ2, (), 52-66
[14] Futatsugi, K.; Goguen, J.; Meseguer, J.; Okada, K., Parameterized programming OBJ2, (), 51-60
[15] Gogolla, M., Partially ordered sorts in algebraic specifications, (), Forschungsbericht nr. 169, 139-153, (1983), Universität Dortmund, Abteilung Informatik, also
[16] Goguen, J., Abstract errors for abstract data types, (), 491-522, also published in
[17] Goguen, J., Order sorted algebra, () · 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, (), 995-1003 · Zbl 0606.68010
[20] Goguen, J., Higher-order functions considered unnecessary for higher-order programming, (), to appear; preliminary version in SRI Technical Report SRI-CSL-88-1, 1988
[21] Goguen, J.; Burstall, R., Institutions: abstract model theory for computer science, (), 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, ()
[23] Goguen, J.; Meseguer, J., Universal realization, persistent interconnection and implementation of abstract modules, (), 265-281 · Zbl 0493.68014
[24] Goguen, J.; Meseguer, J.; Goguen, J.; Meseguer, J.; Goguen, J.; Meseguer, J.; Goguen, J.; Meseguer, J., Programming in prolog, (), 16, 7, 24-37, (1982), preliminary versions have appeared in
[25] Goguen, J.; Meseguer, J.; Goguen, J.; Meseguer, J., Eqlog: equality, types, and generic modules for logic programming, (), J. logic programming, 1, 2, 179-210, (1984), an earlier version appears in · Zbl 0575.68091
[26] Goguen, J.; Meseguer, J.; Goguen, J.; Meseguer, J., Remarks on many-sorted equational logic, Bull. EATCS, SIGPLAN notices, 22, 4, 41-48, (1987), also in · Zbl 0498.03018
[27] Goguen, J.; Meseguer, J.; Goguen, J.; Meseguer, J., Unifying functional, object-oriented and relational programming, with logical semantics, (), SIGPLAN notices, 21, 10, 153-162, (1986), preliminary version in
[28] Goguen, J.; Meseguer, J., Models and equality for logical programming, (), 1-22
[29] Goguen, J.; Meseguer, J.; Goguen, J.; Meseguer, J., Tech. report CSLI-87-92, (), 18-29, (1987), Center for the Study of Language and Information, Stanford University, also
[30] Goguen, J.; Meseguer, J., Software for the rewrite rule machine, (), 628-637
[31] Goguen, J.; Meseguer, J.; Plaisted, D., Programming with parameterized abstract objects in OBJ, (), 163-193
[32] Goguen, J.; Parsaye-Ghomi, K., Algebraic denotational semantics using parameterized abstract modules, (), 292-309 · Zbl 0467.68014
[33] Goguen, J.; Tardo, J., An introduction to OBJ: a language for writing and testing software specification, (), 391-420, reprinted in
[34] Goguen, J.; Thatcher, J.; Wagner, E., An initial algebra approach to the specification, correctness and implementation of abstract data types, (), 80-149, appears in
[35] Goguen, J.; Winkler, T., Introducing OBJ3, ()
[36] Goldberg, A.; Robson, D., Languange and its information, (1983), Addison-Wesley Reading, MA
[37] Gratzer, G., Universal algebra, (1979), Springer Berlin · Zbl 0182.34201
[38] Guiho, G., Multioperator algebras, ()
[39] Harper, R.; MacQueen, D.; Milner, R., Standard ML, ()
[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, () · Zbl 0604.03001
[45] Jones, S.P., The implementation of functional programming languages, (1987), Prentice-Hall Englewood Cliffs, NJ
[46] Kamin, S.; Archer, M., Partial implementations of abstract data types: a dissenting view on errors, (), 317-336
[47] Kirchner, C.; Kirchner, H.; Meseguer, J., Operational semantics of OBJ3, (), 287-301
[48] Kowalski, R., Logic for problem solving, (), 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, (), 869-878
[50] Lloyd, J., Foundations of logic programming, (1984), Springer Berlin · Zbl 0547.68005
[51] Mac Lane, S., Categories for the working Mathematician, (1971), 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, (), 257-329
[54] Meseguer, J.; Meseguer, J., Tech. report SRI-CSL-88-13, (), 228-241, (1988), Computer Science Lab., SRI International, longer version in
[55] Meseguer, J.; Goguen, J., Deduction with many-soted rewrite rules, (), to appear
[56] Meseguer, J.; Goguen, J., Initiality, induction and computability, (), 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, edited and with an introduction by R. Thomason
[59] Mosses, P., A basic semantic algebra, (), 87-107
[60] Mosses, P., Unified algebras and institutions, () · Zbl 0716.68066
[61] O’Donnell, M., Equational logic as a programming language, (1985), MIT Press Cambridge, MA · Zbl 0636.68004
[62] O’Keefe, R., Source level tools for logic programming, (), 68-72
[63] Parsaye-Ghomi, K., Higher order data types, ()
[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, ()
[66] Poigné, A., Parameterization for order-sorted algebraic specification, () · Zbl 0694.68020
[67] ()
[68] Reynolds, J., Towards a theory of type structure, (), 408-423
[69] Reynolds, J., Using category theory to design implicit conversions and generic operators, (), 211-258
[70] Scott, D.; Strachey, C., Towards a mathematical semantics for computer languages, (), 19-46, also appeared as Technical Monograph PRG 6, Oxford University, Programming Research Group
[71] Smolka, G., Order-sorted Horn logic: semantics and deduction, ()
[72] Smolka, G.; Nutt, W.; Goguen, J.; Meseguer, J.; Smolka, G.; Nutt, W.; Goguen, J.; Meseguer, J.; Smolka, G.; Nutt, W.; Goguen, J.; Meseguer, J., SEKI report SR-87-14, (), Proc. coll. on the resolution of equations in algebraic structures, 299-367, (1987), Universität Kaiserslautern, also appears as
[73] Sterling, L.; Shapiro, E., The art of prolog, (1986), MIT Press Cambridge, MA · Zbl 0605.68002
[74] Stoy, J., Denotational semantics of programming languages, (1977), 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, () · Zbl 0675.68006
[77] Turner, D., A non-strict functional language with polymorphic types, (), 1-16
[78] Wadge, W., Classified algebras, ()
[79] Walther, C., A many-sorted calculus based on resolution and paramodulation, (), 882-891
[80] Walther, C., A classification of many-sorted unification theories, (), 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.