An approach to object semantics based on terminal co-algebras

Abstract

The categorical dual construction of initial abstract data types is studied. The resulting terminal co-algebras represent not only an implementation independent semantics of infinite objects such as streams, but also a suitable formal basis for object types in the sense of the object-oriented programming paradigm. Instances of object types may be interpreted as abstract automata with several state transition functions representing the methods of an object, and several output functions representing the attributes. By structuring the index set of the possibly infinite family of methods, and by structuring the output set, one can specify specific object types. For dealing simultaneously with complex data types and object types, it is not necessary to live within a cartesian closed category. In ccc's there are standard functional constructions for object types, but object types are not necessarily a higher-order construction. A world of data types and object types may be combined with the Rewriting Logic of Meseguer to obtain a formal basis for concurrent object systems.