F-algebra
Encyclopedia
In mathematics
, specifically in category theory
, an
-algebra is a structure defined according to a functor
. 
-algebras can be used to represent data structures used in programming, such as lists and trees. Initial 
-algebras encapsulate an induction principle.
-algebras are dual to 
-coalgebra
s.
-algebra for an endofunctor
is an object
of 
together with a 
-morphism
.
In this sense
-algebras are dual to 
-coalgebras.
A homomorphism
from
-algebra 
to 
-algebra 
is a morphism
in
such that
.
Thus the
-algebras constitute a category.
that sends a set 
to 
. Here, Set denotes the category of sets
,
denotes the usual coproduct
given by disjoint union
, and 1 is a terminal object (i.e. any singleton set). Then the set N of natural number
s together with the function
, which is the coproduct of the functions 
(whose image is 0) and 
(which sends an integer n to n+1), is an 
-algebra.
Initial
If the category of 
-algebras for a given endofunctor F has an initial object
, it is called an initial algebra. The algebra
in the above example is an initial algebra. Various finite data structures used in programming, such as lists and trees, can be obtained as initial algebras of specific endofunctors.
Types defined by using least fixed point
construct with functor F can be regarded as an initial
-algebra, provided that parametricity
holds for the type.
See also Universal algebra
.
Terminal
In a dual
way, similar relationship exists between notions of greatest fixed point and terminal
-coalgebra, these can be used for allowing potentially infinite
objects while maintaining strong normalization property
. In the strongly normalizing Charity programming language (i.e. each program terminates in it), coinductive
data types can be used achieving surprising results, e.g. defining lookup
constructs to implement such “strong”
functions like the Ackermann function
.
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
-algebra 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....
. -algebras can be used to represent data structures used in programming, such as lists and trees. Initial -algebras encapsulate an induction principle.-algebras are dual to -coalgebraF-coalgebra
In mathematics, specifically in category theory, an F-coalgebra is a structure defined according to a functor F. For both algebra and coalgebra, a functor is a convenient and general way of organizing a signature...
s.
Definition
An-algebra 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...
.In this sense
-algebras are dual to -coalgebras.A homomorphism
Homomorphism
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
-algebra to -algebra is a morphismin
such that.Thus the
-algebras constitute a category.Example
Consider the functor that sends a set to . Here, Set denotes the category of setsCategory of sets
In the mathematical field of category theory, the category of sets, denoted as Set, is the category whose objects are sets. The arrows or morphisms between sets A and B are all functions from A to B...
,
denotes the usual coproductCoproduct
In category theory, the coproduct, or categorical sum, is the category-theoretic construction which includes the disjoint union of sets and of topological spaces, the free product of groups, and the direct sum of modules and vector spaces. The coproduct of a family of objects is essentially the...
given by disjoint union
Disjoint union
In mathematics, the term disjoint union may refer to one of two different concepts:* In set theory, a disjoint union is a modified union operation that indexes the elements according to which set they originated in; disjoint sets have no element in common.* In probability theory , a disjoint union...
, and 1 is a terminal object (i.e. any singleton set). Then the set N of natural number
Natural number
In mathematics, the natural numbers are the ordinary whole numbers used for counting and ordering . These purposes are related to the linguistic notions of cardinal and ordinal numbers, respectively...
s together with the function
, which is the coproduct of the functions (whose image is 0) and (which sends an integer n to n+1), is an -algebra. Initial 
-algebra
If the category of -algebras for a given endofunctor F has an initial objectInitial object
In category theory, an abstract branch of mathematics, an initial object of a category C is an object I in C such that for every object X in C, there exists precisely one morphism I → X...
, it is called an initial algebra. The algebra
in the above example is an initial algebra. Various finite data structures used in programming, such as lists and trees, can be obtained as initial algebras of specific endofunctors.Types defined by using least fixed point
Least fixed point
In order theory, a branch of mathematics, the least fixed point of a function is the fixed point which is less than or equal to all other fixed points, according to some partial order....
construct with functor F can be regarded as an initial
-algebra, provided that parametricityParametricity
Parametricity is a result in the theory of programming languages in computer science. The principle of parametricity dictates that functions with similar types have similar properties.- Theory of parametricity :...
holds for the type.
See also Universal algebra
Universal algebra
Universal algebra is the field of mathematics that studies algebraic structures themselves, not examples of algebraic structures....
.
Terminal 
-coalgebra
In a dualDuality (mathematics)
In mathematics, a duality, generally speaking, translates concepts, theorems or mathematical structures into other concepts, theorems or structures, in a one-to-one fashion, often by means of an involution operation: if the dual of A is B, then the dual of B is A. As involutions sometimes have...
way, similar relationship exists between notions of greatest fixed point and terminal
-coalgebra, these can be used for allowing potentially infiniteActual infinity
Actual infinity is the idea that numbers, or some other type of mathematical object, can form an actual, completed totality; namely, a set. Hence, in the philosophy of mathematics, the abstraction of actual infinity involves the acceptance of infinite entities, such as the set of all natural...
objects while maintaining strong normalization property
Normalization property (lambda-calculus)
In mathematical logic and theoretical computer science, a rewrite system has the strong normalization property if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form...
. In the strongly normalizing Charity programming language (i.e. each program terminates in it), coinductive
Coinduction
In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects.Coinduction is the mathematical dual to structural induction...
data types can be used achieving surprising results, e.g. defining lookup
Lookup table
In computer science, a lookup table is a data structure, usually an array or associative array, often used to replace a runtime computation with a simpler array indexing operation. The savings in terms of processing time can be significant, since retrieving a value from memory is often faster than...
constructs to implement such “strong”
Computability theory (computer science)
Computability is the ability to solve a problem in an effective manner. It is a key topic of the field of computability theory within mathematical logic and the theory of computation within computer science...
functions like the Ackermann function
Ackermann function
In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive...
.
External links
- Categorical programming with inductive and coinductive types by Varmo Vene
- Philip Wadler: Recursive types for free! University of Glasgow, July 1998. Draft.
- Algebra and coalgebra from CLiki