Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
type: Item
instance of: scholarly article
title: Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
zbMATH Open document ID: 0778.68056
DOI: 10.1016/0304-3975(92)90302-V
author: Joseph Goguen
author: José Meseguer
published in: Theoretical Computer Science
publication date: 1992-12-16T00:00:00Z
review text: 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.
reviewed by: Stephen L. Bloom
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 08A70
Mathematics Subject Classification ID: 06F99
zbMATH DE Number: 78177
zbMATH Keywords: exception handling
zbMATH Keywords: error recovery
zbMATH Keywords: sort constraints
zbMATH Keywords: inheritance
zbMATH Keywords: polymorphism
zbMATH Keywords: meaningless expressions
zbMATH Keywords: completeness theorem
zbMATH Keywords: initial algebra
zbMATH Keywords: conditional equations
zbMATH Keywords: Birkhoff variety theorem
zbMATH Keywords: McKinsey-Malcev quasi-variety theorem
describes a project that uses: Miranda
describes a project that uses: Simula 67
describes a project that uses: ML
describes a project that uses: Haskell
MaRDI profile type: Publication
cites work: Q5762080
cites work: Q3906394
cites work: Q3332229
cites work: Q3919057
cites work: Rewrite systems on a lattice of types
cites work: An Oxford survey of order sorted algebra
cites work: Parameterized Programming
cites work: Q3745248
cites work: Q3956373
cites work: Equality, types, modules, and (why not?) generics for logic programming
cites work: Q3962973
cites work: Q3030249
cites work: Q3920616
cites work: Q4692787
cites work: Q3943975
cites work: Q5572358
cites work: An algebraic approach to the syntax and semantics of languages with subscripted variables
cites work: Algebras with a Scheme of Operators
cites work: An axiomatic basis for computer programming
cites work: Q3741611
cites work: Q4692880
cites work: Q3345749
cites work: Q3795207
cites work: Q3862380
cites work: Q3339245
cites work: Q5639839
cites work: Order completion monads
cites work: Q3032225
cites work: Q3687683
cites work: A theory of type polymorphism in programming
cites work: Q3332227
cites work: Q3204056
cites work: Q3776590
cites work: Parametrization for order-sorted algebraic specification
cites work: The programming language ADA. Reference manual. American National Standards Institute, Inc. ANSI/MIL-STD-1815A-1983. Approved 17 February 1983
cites work: Q4068054
cites work: Q5685626
cites work: Q3742689
cites work: Q3992826
cites work: Q3721784
cites work: Q3786021
description: scientific article; zbMATH DE number 78177