In mathematics, specifically in category theory, an
F
F
F
F
F
F
Let
F:l{C}\longrightarrowl{C}
be an endofunctor on a category
\alpha:A\longrightarrowFA
of
l{C}
(A,\alpha)
An
F
(A,\alpha)
F
(B,\beta)
f:A\longrightarrowB
in
l{C}
Ff\circ\alpha=\beta\circf
Thus the
F
Consider the endofunctor
X\mapstoX\sqcup\{*\}:Set\toSet
\{\ast\}
(\overline{N
\overline{N
\alpha
\alpha(0)=\ast
\alpha(n)=n-1
n=1,2,\ldots
\alpha(infty)=infty
(\overline{N
More generally, fix some set
A
F:Set\longrightarrowSet
X
(X x A)\cup\{1\}
F
\alpha:X\longrightarrow(X x A)\cup\{1\}=FX
X
\alpha
A
\{1\}
In many practical applications, the state-transition function of such a coalgebraic object may be of the form
X\rarrf1 x f2 x \ldots x fn
X\rarrf1,X\rarrf2\ldotsX\rarrfn
X\rarr
A1 x \ldots x An | |
X |
F
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(A×(-)) are in bijective correspondence with labelled transition systems, and homomorphisms between coalgebras correspond to functional bisimulations between labelled transition systems.
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.