Unified Algebras and Institutions

Abstract

A novel framework for algebraic specification of abstract data types is introduced. It involves so-called ''unified algebras'', where sorts are treated as values, so that operations may be applied to sorts as well as to the elements that they classify.

An institution for unified algebras is defined, and shown to be liberal. However, the ordinary ''forgetful'' functor does not forget any values in unified algebras, so the usual data constraints do not have any models. A ''more forgetful'' functor is introduced and used to define so-called ''bounded'' data constraints, which have the expected models.