# F-coalgebra

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

In mathematics, specifically in category theory, an ${\displaystyle F}$-coalgebra is a structure defined according to a functor ${\displaystyle F}$. For both algebra and coalgebra, a functor is a convenient and general way of organizing a signature. This has applications in computer science: examples of coalgebras include lazy, infinite data structures, such as streams, and also transition systems.

${\displaystyle F}$-coalgebras are dual to ${\displaystyle F}$-algebras. Just as the class of all algebras for a given signature and equational theory form a variety, so does the class of all ${\displaystyle F}$-coalgebras satisfying a given equational theory form a covariety, where the signature is given by ${\displaystyle F}$.

## Definition

An ${\displaystyle F}$-coalgebra for an endofunctor

${\displaystyle F:{\mathcal {C}}\longrightarrow {\mathcal {C}}}$
${\displaystyle \alpha :A\longrightarrow FA}$.
${\displaystyle f:A\longrightarrow B}$
${\displaystyle Ff\circ \alpha =\beta \circ f}$.

Thus the ${\displaystyle F}$-coalgebras for a given functor F constitute a category.

## Examples

Consider the functor ${\displaystyle F:\mathbf {Set} \longrightarrow \mathbf {Set} }$ that sends ${\displaystyle X}$ to ${\displaystyle X\times A\cup \{1\}}$, ${\displaystyle F}$-coalgebras ${\displaystyle \alpha :X\longrightarrow X\times A\cup \{1\}=FX}$ are then finite or infinite streams over the alphabet ${\displaystyle A}$, where ${\displaystyle X}$ is the set of states and ${\displaystyle \alpha }$ is the state-transition function. Applying the state-transition function to a state may yield two possible results: either an element of ${\displaystyle A}$ together with the next state of the stream, or the element of the singleton set ${\displaystyle \{1\}}$ 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 ${\displaystyle X\rightarrow f_{1}\times f_{2}\times \ldots \times f_{n}}$, which readily factorizes into a collection of "selectors", "observers", "methods" ${\displaystyle X\rightarrow f_{1},\,X\rightarrow f_{2}\,\ldots \,X\rightarrow f_{n}}$. Special cases of practical interest include observers yielding attribute values, and mutator methods of the form ${\displaystyle X\rightarrow X^{A_{1}\times \ldots \times A_{n}}}$ taking additional parameters and yielding states. This decomposition is dual to the decomposition of initial ${\displaystyle F}$-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: coalgebras for the endofunctor P(A×(-)) are in bijective correspondence with labelled transition systems. 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 reactive behaviour of systems, including classes in object-oriented programming. While algebraic specification deals with functional behaviour, typically using inductive datatypes generated by constructors, coalgebraic specification is concerned with reactive 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.