F-coalgebra
Encyclopedia
In mathematics
, specifically in category theory
, an
-coalgebra is a structure defined according to a functor
. 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 structure
s, such as streams, and also transition systems
.
-coalgebras are dual to 
-algebra
s. Just as the class of all algebras
for a given signature and equational theory form a variety
, so does the class of all
-coalgebras satisfying a given equational theory form a covariety, where the signature is given by 
.
-coalgebra for an endofunctor
is an object
of 
together with a 
-morphism
.
An
-coalgebra homomorphism
from
to another 
-coalgebra
is a morphism
in
such that
.
Thus the
-coalgebras for a given functor F constitute a category.
that sends 
to 
, 
-coalgebras 
are then finite or infinite streams 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 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
, 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: coalgebras for the endofunctor P(A×(-)) are in bijective correspondence with labelled transition systems.
Homomorphisms between coalgebras correspond to functional bisimulation
s between labelled transition systems.
, 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
.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, specifically in category theory
Category theory
Category theory is an area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as collections of objects and arrows , where these collections satisfy certain basic conditions...
, an
-coalgebra is a structure defined according to a functorFunctor
In category theory, a branch of mathematics, a functor is a special type of mapping between categories. Functors can be thought of as homomorphisms between categories, or morphisms when in the category of small categories....
. For both algebra and coalgebra, a functor is a convenient and general way of organizing a signature. This has applications in computer scienceComputer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
: examples of coalgebras include lazy
Lazy evaluation
In programming language theory, lazy evaluation or call-by-need is an evaluation strategy which delays the evaluation of an expression until the value of this is actually required and which also avoids repeated evaluations...
, infinite data structure
Data structure
In computer science, a data structure is a particular way of storing and organizing data in a computer so that it can be used efficiently.Different kinds of data structures are suited to different kinds of applications, and some are highly specialized to specific tasks...
s, such as streams, and also transition systems
State transition system
In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states, which may be labeled with labels chosen from a set; the same label may appear on more than one transition...
.
-coalgebras are dual to -algebraF-algebra
In mathematics, specifically in category theory, an F-algebra is a structure defined according to a functor F. F-algebras can be used to represent data structures used in programming, such as lists and trees...
s. Just as the class of all algebras
Algebraic structure
In abstract algebra, an algebraic structure consists of one or more sets, called underlying sets or carriers or sorts, closed under one or more operations, satisfying some axioms. Abstract algebra is primarily the study of algebraic structures and their properties...
for a given signature and equational theory form a variety
Variety (universal algebra)
In mathematics, specifically universal algebra, a variety of algebras is the class of all algebraic structures of a given signature satisfying a given set of identities. Equivalently, a variety is a class of algebraic structures of the same signature which is closed under the taking of homomorphic...
, so does the class of all
-coalgebras satisfying a given equational theory form a covariety, where the signature is given by .Definition
An-coalgebra for an endofunctoris an object
of together with a -morphismMorphism
In mathematics, a morphism is an abstraction derived from structure-preserving mappings between two mathematical structures. The notion of morphism recurs in much of contemporary mathematics...
.An
-coalgebra homomorphismHomomorphism
In abstract algebra, a homomorphism is a structure-preserving map between two algebraic structures . The word homomorphism comes from the Greek language: ὁμός meaning "same" and μορφή meaning "shape".- Definition :The definition of homomorphism depends on the type of algebraic structure under...
from
to another -coalgebra is a morphismin
such that.Thus the
-coalgebras for a given functor F constitute a category.Examples
Consider the functor that sends to , -coalgebras are then finite or infinite streams 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 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
, 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: coalgebras for the endofunctor P(A×(-)) are in bijective correspondence with labelled transition systems.
Homomorphisms between coalgebras correspond to functional bisimulation
Bisimulation
In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa....
s between labelled transition systems.
Applications
In computer scienceComputer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, coalgebra has emerged as a convenient and suitably general way of specifying the reactive
Reactive programming
In computing, reactive programming is a programming paradigm oriented around data flows and the propagation of change. This means that it should be possible to express static or dynamic data flows with ease in the programming languages used, and that the underlying execution model will...
behaviour of systems, including classes in object-oriented programming
Object-oriented programming
Object-oriented programming is a programming paradigm using "objects" – data structures consisting of data fields and methods together with their interactions – to design applications and computer programs. Programming techniques may include features such as data abstraction,...
. While algebraic specification
Algebraic specification
Algebraic specification, is a software engineering technique for formally specifying system behavior. Algebraic specification seeks to systematically develop more efficient programs by:...
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
Automata theory
In theoretical computer science, automata theory is the study of abstract machines and the computational problems that can be solved using these machines. These abstract machines are called automata...
. 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
Modal logic
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
.