Simon Veglioni August 1997, 28pp.
In this paper we describe the role classification play in algebraic approaches to specification of Abstract Data Types (ADTs) and show how they influence expressivity and mechanizability.
In the last two decades many different logic systems for the algebraic specification of ADTs have been developed, each one pursuing its own principles and goals. Since a careful analysis of these logical systems, taking into account not only their expressivity, but also their mechanizability, is important to clarify and organizse a rather rich and controversial subject - for example overloading is a topic that needs to be clarified - we believe our contribution will be useful.
Mechanizability of logical systems is in fact as important as expressivity, and becomes crucial for those logical systems which are meant to define the semantics of declarative and rapid prototyping languages.
We have taken great care to present all arguments in this paper in as elementary a way as possible, in order to make the paper accessible to non-expert readers, even though a minimum knowledge of category theory and institutions might be of help in few points.