Let be an endofunctor on a category. An -coalgebra is an object of together with a morphism of, usually written as. An -coalgebra homomorphism from to another -coalgebra is a morphism in such that Thus the -coalgebras for a given functor F constitute a category.
Examples
Consider the endofunctor that sends a set to its disjoint union with the singleton set. A coalgebra of this endofunctor is given by, where is the so-called conatural numbers, consisting of the nonnegative integers and also infinity, and the function is given by, for and. In fact, is the terminal coalgebra of this endofunctor. More generally, fix some set, and consider the functor that sends to. Then an -coalgebra is a finite or infinite stream over the alphabet where is the set of states and is the state-transition function. Applying the state-transition function to a state may yield two possible results: either an element of together with the next state of the stream, or the element of the singleton set as a separate "final state" indicating that there are no more values in the stream. In many practical applications, the state-transition function of such a coalgebraic object may be of the form, which readily factorizes into a collection of "selectors", "observers", "methods". Special cases of practical interest include observers yielding attribute values, and mutator methods of the form taking additional parameters and yielding states. This decomposition is dual to the decomposition of initial -algebras into sums of 'constructors'. Let P be the power set construction on the category of sets, considered as a covariant functor. The P-coalgebras are in bijective correspondence with sets with a binary relation. Now fix another set, A. Then coalgebras for the endofunctor P are in bijective correspondence with labelled transition systems, and homomorphisms between coalgebras correspond to functional bisimulations between labelled transition systems.
Applications
In computer science, coalgebra has emerged as a convenient and suitably general way of specifying the behaviour of systems and data structures that are potentially infinite, for example classes in object-oriented programming, streams and transition systems. While algebraic specification deals with functional behaviour, typically using inductive datatypes generated by constructors, coalgebraic specification is concerned with behaviour modelled by coinductive process types that are observable by selectors, much in the spirit of automata theory. An important role is played here by final coalgebras, which are complete sets of possibly infinite behaviours, such as streams. The natural logic to express properties of such systems is coalgebraic modal logic.
