An approach to object semantics based on terminal co-algebras. (English) Zbl 0854.18006

Reichel, Horst

Math. Struct. Comput. Sci. 5, No. 2, 129-152 (1995).

The paper presents terminal coalgebras as categorical dual concept of initial algebras and shows, by several formalization examples, the possibility of using terminal coalgebras in semantics of object-oriented programming. The aim of the paper is to propose a formal basis for object type semantics that could be an approach analogous to the initiality in ADT. The key point for theoretical advantages in such a perspective is that a foundation of terminality, in a proper categorical setting, can produce a semantics for infinite objects that is abstract in as much it is independent from any implementation of them. The paper starts with the notion of \(T\)-algebra, borrowed from M. Barr [Theor. Comput. Sci. 114, No. 2, 299-315 (1993; Zbl 0779.18004)], as a pair consisting of an object \(C\) in a prefixed category and a morphism between \(T\) and \(C\), where \(T\) is an endofunctor in the considered category. A \(T\)-coalgebra is obtained just by choosing an object and a morphism in the opposite direction. Categories of \(T\)-algebras and \(T\)-coalgebras are defined by requiring the commutativity of usual diagrams. An ADT is easily seen as in a suitable \(T\)-algebra where in a sense \(T\) encodes the structural schema of the type. The rest of the paper presents some crucial examples where abstract object types result to be terminal \(T\)-coalgebras for some suitable endofunctors: streams, reals, bank accounts (in Meseguer’s sense), and simple databases. The adopted syntax refers to the experimental programming language CHARITY. It is worthwhile to note that, in terminal semantics, defining equations lead to subalgebras of terminal coalgebras. The final two sections of the paper are devoted to object systems (where objects are used as attribute values of other objects) and to concurrent object systems, in order to outline a possible combination of the sketched object type semantics with the logical theory of concurrent objects introduced by J. Meseguer [ACM SIGPLAN Notices 25, No. 10, 101-155 (1990)].

Reviewer: V.Manca (Pisa)

MSC:

18C10	Theories (e.g., algebraic theories), structure, and semantics
68Q55	Semantics in the theory of computing
68Q65	Abstract data types; algebraic specification
18D15	Closed categories (closed monoidal and Cartesian closed categories, etc.)

Keywords:

terminal semantics; terminal coalgebras; object-oriented programming; object type semantics; concurrent objects

Citations:

Zbl 0779.18004

Software:

Miranda; OBJ3