zbMATH — the first resource for mathematics

Membership algebra as a logical framework for equational specification. (English) Zbl 0903.08009
Parisi Presicce, Francesco (ed.), Recent trends in algebraic development techniques. 12th international workshop, WADT ’97, Tarquinia, Italy, June 3–7, 1997. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1376, 18-61 (1998).
Summary: This paper proposes membership equational logic – a Horn logic in which the basic predicates are equations \(t= t'\) and membership assertions \(t:s\) stating that a term \(t\) belongs to a sort \(s\) – as a logical framework in which a very wide range of total and partial equational specification formalisms can be naturally represented. Key features of this logic include: simplicity, liberality and equational character; generality and expressiveness in supporting subsorts, overloading, errors and partiality; and efficient implementability in systems such as Maude. The paper presents the basic properties of the logic and its models, and discusses in detail how many total and partial equational specification formalisms, including order-sorted algebra and partial membership equational logic, can be represented in it, as well as the practical benefits in terms of tool reusability that this opens up for other languages, including CASL.
For the entire collection see [Zbl 0889.00030].

08A70 Applications of universal algebra in computer science
68Q65 Abstract data types; algebraic specification