In
mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
, an initial algebra is an
initial object
In category theory, a branch of mathematics, an initial object of a category is an object in such that for every object in , there exists precisely one morphism .
The dual notion is that of a terminal object (also called terminal element): ...
in the
category
Category, plural categories, may refer to:
Philosophy and general uses
* Categorization, categories in cognitive science, information science and generally
*Category of being
* ''Categories'' (Aristotle)
*Category (Kant)
*Categories (Peirce)
* ...
of
-algebras for a given
endofunctor
In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) are associated to topological spaces, and ma ...
. This initiality provides a general framework for
induction
Induction, Inducible or Inductive may refer to:
Biology and medicine
* Labor induction (birth/pregnancy)
* Induction chemotherapy, in medicine
* Induced stem cells, stem cells derived from somatic, reproductive, pluripotent or other cell t ...
and
recursion
Recursion (adjective: ''recursive'') occurs when a thing is defined in terms of itself or of its type. Recursion is used in a variety of disciplines ranging from linguistics to logic. The most common application of recursion is in mathematics ...
.
Examples
Functor
Consider the endofunctor sending to , where is the one-point (
singleton
Singleton may refer to:
Sciences, technology Mathematics
* Singleton (mathematics), a set with exactly one element
* Singleton field, used in conformal field theory Computing
* Singleton pattern, a design pattern that allows only one instance o ...
)
set
Set, The Set, SET or SETS may refer to:
Science, technology, and mathematics Mathematics
*Set (mathematics), a collection of elements
*Category of sets, the category whose objects and morphisms are sets and total functions, respectively
Electro ...
, the
terminal object
In category theory, a branch of mathematics, an initial object of a category is an object in such that for every object in , there exists precisely one morphism .
The dual notion is that of a terminal object (also called terminal element): ...
in the category. An algebra for this endofunctor is a set (called the ''carrier'' of the algebra) together with a
function
Function or functionality may refer to:
Computing
* Function key, a type of key on computer keyboards
* Function model, a structured representation of processes in a system
* Function object or functor or functionoid, a concept of object-oriente ...
. Defining such a function amounts to defining a point
and a function .
Define
:
and
:
Then the set of natural numbers together with the function is an initial -algebra. The initiality (the
universal property
In mathematics, more specifically in category theory, a universal property is a property that characterizes up to an isomorphism the result of some constructions. Thus, universal properties can be used for defining some objects independently fro ...
for this case) is not hard to establish; the unique
homomorphism
In algebra, a homomorphism is a structure-preserving map between two algebraic structures of the same type (such as two groups, two rings, or two vector spaces). The word ''homomorphism'' comes from the Ancient Greek language: () meaning "same" ...
to an arbitrary -algebra , for an element of and a function on , is the function sending the natural number to , that is, , the -fold application of to .
The set of
natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''Cardinal n ...
s is the carrier of an initial algebra for this functor: the point is zero and the function is the
successor function
In mathematics, the successor function or successor operation sends a natural number to the next one. The successor function is denoted by ''S'', so ''S''(''n'') = ''n'' +1. For example, ''S''(1) = 2 and ''S''(2) = 3. The successor functio ...
.
Functor
For a second example, consider the endofunctor on the category of sets, where is the set of natural numbers. An algebra for this endofunctor is a set together with a function . To define such a function, we need a point
and a function . The set of finite
list
A ''list'' is any set of items in a row. List or lists may also refer to:
People
* List (surname)
Organizations
* List College, an undergraduate division of the Jewish Theological Seminary of America
* SC Germania List, German rugby union ...
s of natural numbers is an initial algebra for this functor. The point is the empty list, and the function is
cons
In computer programming, ( or ) is a fundamental function in most dialects of the Lisp programming language. ''constructs'' memory objects which hold two values or pointers to two values. These objects are referred to as (cons) cells, conses, ...
, taking a number and a finite list, and returning a new finite list with the number at the head.
In categories with binary
coproduct
In category theory, the coproduct, or categorical sum, is a construction which includes as examples the disjoint union of sets and of topological spaces, the free product of groups, and the direct sum of modules and vector spaces. The coprodu ...
s, the definitions just given are equivalent to the usual definitions of a
natural number object In category theory, a natural numbers object (NNO) is an object endowed with a recursive structure similar to natural numbers. More precisely, in a category E with a terminal object 1, an NNO ''N'' is given by:
# a global element ''z'' : 1 → ''N ...
and a
list object, respectively.
Final coalgebra
Dually Dually may refer to:
*Dualla, County Tipperary, a village in Ireland
*A pickup truck with dual wheels on the rear axle
* DUALLy, s platform for architectural languages interoperability
* Dual-processor
See also
* Dual (disambiguation)
Dual or ...
, a final coalgebra is a
terminal object
In category theory, a branch of mathematics, an initial object of a category is an object in such that for every object in , there exists precisely one morphism .
The dual notion is that of a terminal object (also called terminal element): ...
in the category of
-coalgebras. The finality provides a general framework for
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. Coinductively defined types are known as codata and ...
and
corecursion
In computer science, corecursion is a type of operation that is dual to recursion. Whereas recursion works analytically, starting on data further from a base case and breaking it down into smaller data and repeating until one reaches a base case, ...
.
For example, using the same
functor
In mathematics, specifically category theory, a functor is a Map (mathematics), mapping between Category (mathematics), categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) ar ...
as before, a coalgebra is defined as a set together with a function . Defining such a function amounts to defining a
partial function
In mathematics, a partial function from a set to a set is a function from a subset of (possibly itself) to . The subset , that is, the domain of viewed as a function, is called the domain of definition of . If equals , that is, if is de ...
whose
domain
Domain may refer to:
Mathematics
*Domain of a function, the set of input values for which the (total) function is defined
**Domain of definition of a partial function
**Natural domain of a partial function
**Domain of holomorphy of a function
* Do ...
is formed by those
for which belongs to . Such a structure can be viewed as a chain of sets, on which is not defined, which elements map into by , which elements map into by , etc., and containing the remaining elements of . With this in view, the set
consisting of the set of natural numbers extended with a new element is the carrier of the final coalgebra in the category, where
is the predecessor function (the
inverse of the successor function) on the positive naturals, but acts like the
identity
Identity may refer to:
* Identity document
* Identity (philosophy)
* Identity (social science)
* Identity (mathematics)
Arts and entertainment Film and television
* ''Identity'' (1987 film), an Iranian film
* ''Identity'' (2003 film), ...
on the new element : , . This set
that is the carrier of the final coalgebra of is known as the set of conatural numbers.
For a second example, consider the same functor as before. In this case the carrier of the final coalgebra consists of all lists of natural numbers, finite as well as
infinite
Infinite may refer to:
Mathematics
*Infinite set, a set that is not a finite set
*Infinity, an abstract concept describing something without any limit
Music
* Infinite (group), a South Korean boy band
*''Infinite'' (EP), debut EP of American m ...
. The operations are a test function testing whether a list is empty, and a deconstruction function defined on non-empty lists returning a pair consisting of the head and the tail of the input list.
Theorems
* Initial algebras are minimal (i.e., have no proper subalgebra).
* Final coalgebras are
simple
Simple or SIMPLE may refer to:
*Simplicity, the state or quality of being simple
Arts and entertainment
* ''Simple'' (album), by Andy Yorke, 2008, and its title track
* "Simple" (Florida Georgia Line song), 2018
* "Simple", a song by Johnn ...
(i.e., have no proper quotients).
Use in computer science
Various finite
data structures
In computer science, a data structure is a data organization, management, and storage format that is usually chosen for efficient access to data. More precisely, a data structure is a collection of data values, the relationships among them, a ...
used in
programming, such as
list
A ''list'' is any set of items in a row. List or lists may also refer to:
People
* List (surname)
Organizations
* List College, an undergraduate division of the Jewish Theological Seminary of America
* SC Germania List, German rugby union ...
s and
tree
In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, including only woody plants with secondary growth, plants that are ...
s, can be obtained as initial algebras of specific endofunctors.
While there may be several initial algebras for a given endofunctor, they are
unique up to Two Mathematical object, mathematical objects ''a'' and ''b'' are called equal up to an equivalence relation ''R''
* if ''a'' and ''b'' are related by ''R'', that is,
* if ''aRb'' holds, that is,
* if the equivalence classes of ''a'' and ''b'' wi ...
isomorphism
In mathematics, an isomorphism is a structure-preserving mapping between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between them. The word is ...
, which informally means that the "observable" properties of a data structure can be adequately captured by defining it as an initial algebra.
To obtain the
type of lists whose elements are members of set , consider that the list-forming operations are:
*
*
Combined into one function, they give:
*
which makes this an -algebra for the endofunctor sending to . It is, in fact, ''the'' initial -algebra. Initiality is established by the function known as ''
foldr'' in
functional
Functional may refer to:
* Movements in architecture:
** Functionalism (architecture)
** Form follows function
* Functional group, combination of atoms within molecules
* Medical conditions without currently visible organic basis:
** Functional sy ...
programming language
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.
The description of a programming ...
s such as
Haskell
Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lang ...
and
ML.
Likewise,
binary tree
In computer science, a binary tree is a k-ary k = 2 tree data structure in which each node has at most two children, which are referred to as the ' and the '. A recursive definition using just set theory notions is that a (non-empty) binary t ...
s with elements at the leaves can be obtained as the initial algebra
*
Types obtained this way are known as
algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., t ...
s.
Types defined by using
least fixed point
In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set to itself is the fixed point which is less than each other fixed point, according to the o ...
construct with functor can be regarded as an initial -algebra, provided that
parametricity In programming language theory, parametricity is an abstract uniformity property enjoyed by parametrically polymorphic functions, which captures the intuition that all instances of a polymorphic function act the same way.
Idea
Consider this exa ...
holds for the type.
[Philip Wadler]
Recursive types for free!
University of Glasgow, July 1998. Draft.
In a dual way, similar relationship exists between notions of
greatest fixed point
In order theory, a branch of mathematics, the least fixed point (lfp or LFP, sometimes also smallest fixed point) of a function from a partially ordered set to itself is the fixed point which is less than each other fixed point, according to the o ...
and terminal {{mvar, F-coalgebra, with applications to
coinductive
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. Coinductively defined types are known as codata and ...
types. These can be used for allowing
potentially infinite objects while maintaining
strong normalization property.
[ In the strongly normalizing (each program terminates) Charity programming language, coinductive data types can be used for achieving surprising results, e.g. defining ]lookup
In computer science, a lookup table (LUT) is an array that replaces runtime computation with a simpler array indexing operation. The process is termed as "direct addressing" and LUTs differ from hash tables in a way that, to retrieve a value v wi ...
constructs to implement such “strong” functions like the 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. All primitive recursive functions are total ...
.[Robin Cockett: Charitable Thoughts]
ps.gz
See also
* Algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., t ...
* Catamorphism
In category theory, the concept of catamorphism (from the Ancient Greek: "downwards" and "form, shape") denotes the unique homomorphism from an initial algebra into some other algebra.
In functional programming, catamorphisms provide generalizat ...
* Anamorphism
In computer programming, an anamorphism is a function that generates a sequence by repeated application of the function to its previous result. You begin with some value A and apply a function f to it to get B. Then you apply f to B to get C, and ...
Notes
External links
Categorical programming with inductive and coinductive types
by Varmo Vene
Recursive types for free!
by Philip Wadler, University of Glasgow, 1990-2014.
by J.J.M.M. Rutten and D. Turi
from CLiki
Typed Tagless Final Interpreters
by Oleg Kiselyov
Category theory
Functional programming
Type theory