Initial algebra

Last updated

In mathematics, an initial algebra is an initial object in the category of F-algebras for a given endofunctor F. This initiality provides a general framework for induction and recursion.

Contents

Examples

Functor

Consider the endofunctor F : SetSet sending X to 1 + X, where 1 is a one-point (singleton) set, a terminal object in the category. An algebra for this endofunctor is a set X (called the carrier of the algebra) together with a function f : (1 + X) → X. Defining such a function amounts to defining a point and a function XX. Define

and

Then the set N of natural numbers together with the function [zero,succ]: 1 + NN is an initial F-algebra. The initiality (the universal property for this case) is not hard to establish; the unique homomorphism to an arbitrary F-algebra (A, [e, f]), for e: 1 → A an element of A and f: AA a function on A, is the function sending the natural number n to fn(e), that is, f(f(…(f(e))…)), the n-fold application of f to e.

The set of natural numbers is the carrier of an initial algebra for this functor: the point is zero and the function is the successor function.

Functor 1 + N × (−)

For a second example, consider the endofunctor 1 + N × (−) on the category of sets, where N is the set of natural numbers. An algebra for this endofunctor is a set X together with a function 1 + N × XX. To define such a function, we need a point and a function N × XX. The set of finite lists of natural numbers is an initial algebra for this functor. The point is the empty list, and the function is cons, taking a number and a finite list, and returning a new finite list with the number at the head.

In categories with binary coproducts, the definitions just given are equivalent to the usual definitions of a natural number object and a list object, respectively.

Final coalgebra

Dually, a final coalgebra is a terminal object in the category of F-coalgebras. The finality provides a general framework for coinduction and corecursion.

For example, using the same functor 1 + (−) as before, a coalgebra is defined as a set X together with a function f : X → (1 + X). Defining such a function amounts to defining a partial function f': XX whose domain is formed by those for which f(x) do not belongs to 1. Having such a structure, we can define a chain of sets: X0 being a subset of X on which f is not defined, X1 which elements map into X0 by f, X2 which elements map into X1 by f, etc., and Xω containing the remaining elements of X. 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, where is the predecessor function (the inverse of the successor function) on the positive naturals, but acts like the identity on the new element ω: f(n + 1) = n, f(ω) = ω. This set that is the carrier of the final coalgebra of 1 + (−) is known as the set of conatural numbers.

For a second example, consider the same functor 1 + N × (−) as before. In this case the carrier of the final coalgebra consists of all lists of natural numbers, finite as well as infinite. 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

Use in computer science

Various finite data structures used in programming, such as lists and trees, 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 isomorphism, 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 List(A) of lists whose elements are members of set A, consider that the list-forming operations are:

Combined into one function, they give:

which makes this an F-algebra for the endofunctor F sending X to 1 + (A × X). It is, in fact, the initial F-algebra. Initiality is established by the function known as foldr in functional programming languages such as Haskell and ML.

Likewise, binary trees with elements at the leaves can be obtained as the initial algebra

Types obtained this way are known as algebraic data types.

Types defined by using least fixed point construct with functor F can be regarded as an initial F-algebra, provided that parametricity holds for the type. [1]

In a dual way, similar relationship exists between notions of greatest fixed point and terminal F-coalgebra, with applications to coinductive types. These can be used for allowing potentially infinite objects while maintaining strong normalization property. [1] In the strongly normalizing (each program terminates) Charity programming language, coinductive data types can be used for achieving surprising results, e.g. defining lookup constructs to implement such “strong” functions like the Ackermann function. [2]

See also

Notes

  1. 1 2 Philip Wadler: Recursive types for free! University of Glasgow, July 1998. Draft.
  2. Robin Cockett: Charitable Thoughts (ps.gz)

Related Research Articles

In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects are associated to topological spaces, and maps between these algebraic objects are associated to continuous maps between spaces. Nowadays, functors are used throughout modern mathematics to relate various categories. Thus, functors are important in all areas within mathematics to which category theory is applied.

In mathematics, the Yoneda lemma is a fundamental result in category theory. It is an abstract result on functors of the type morphisms into a fixed object. It is a vast generalisation of Cayley's theorem from group theory. It allows the embedding of any locally small category into a category of functors defined on that category. It also clarifies how the embedded category, of representable functors and their natural transformations, relates to the other objects in the larger functor category. It is an important tool that underlies several modern developments in algebraic geometry and representation theory. It is named after Nobuo Yoneda.

In category theory, a branch of mathematics, a natural transformation provides a way of transforming one functor into another while respecting the internal structure of the categories involved. Hence, a natural transformation can be considered to be a "morphism of functors". Informally, the notion of a natural transformation states that a particular map between functors can be done consistently over an entire category.

In mathematics, coalgebras or cogebras are structures that are dual to unital associative algebras. The axioms of unital associative algebras can be formulated in terms of commutative diagrams. Turning all arrows around, one obtains the axioms of coalgebras. Every coalgebra, by duality, gives rise to an algebra, but not in general the other way. In finite dimensions, this duality goes in both directions.

In mathematics, a monoidal category is a category equipped with a bifunctor

In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. Informally, a free object over a set A can be thought of as being a "generic" algebraic structure over A: the only equations that hold between elements of the free object are those that follow from the defining axioms of the algebraic structure. Examples include free groups, tensor algebras, or free lattices.

In category theory, a branch of mathematics, a monad is a monoid in the category of endofunctors of some fixed category. An endofunctor is a functor mapping a category to itself, and a monad is an endofunctor together with two natural transformations required to fulfill certain coherence conditions. Monads are used in the theory of pairs of adjoint functors, and they generalize closure operators on partially ordered sets to arbitrary categories. Monads are also useful in the theory of datatypes, the denotational semantics of imperative programming languages, and in functional programming languages, allowing languages without mutable state to do things such as simulate for-loops; see Monad.

<span class="mw-page-title-main">Pontryagin duality</span> Duality for locally compact abelian groups

In mathematics, Pontryagin duality is a duality between locally compact abelian groups that allows generalizing Fourier transform to all such groups, which include the circle group, the finite abelian groups, and the additive group of the integers, the real numbers, and every finite-dimensional vector space over the reals or a p-adic field.

In category theory, a branch of abstract mathematics, an equivalence of categories is a relation between two categories that establishes that these categories are "essentially the same". There are numerous examples of categorical equivalences from many areas of mathematics. Establishing an equivalence involves demonstrating strong similarities between the mathematical structures concerned. In some cases, these structures may appear to be unrelated at a superficial or intuitive level, making the notion fairly powerful: it creates the opportunity to "translate" theorems between different kinds of mathematical structures, knowing that the essential meaning of those theorems is preserved under the translation.

In mathematics, specifically in category theory, an -coalgebra is a structure defined according to a functor , with specific properties as defined below. For both algebras and coalgebras, a functor is a convenient and general way of organizing a signature. This has applications in computer science: examples of coalgebras include lazy evaluation, infinite data structures, such as streams, and also transition systems.

<i>F</i>-algebra

In mathematics, specifically in category theory, F-algebras generalize the notion of algebraic structure. Rewriting the algebraic laws in terms of morphisms eliminates all references to quantified elements from the axioms, and these algebraic laws may then be glued together in terms of a single functor F, the signature.

In mathematics, specifically in category theory, an exponential object or map object is the categorical generalization of a function space in set theory. Categories with all finite products and exponential objects are called cartesian closed categories. Categories without adjoined products may still have an exponential law.

This is a glossary of properties and concepts in category theory in mathematics.

In functional programming, the concept of catamorphism denotes the unique homomorphism from an initial algebra into some other algebra.

In mathematics a Lie coalgebra is the dual structure to a Lie algebra.

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 so on until some terminating condition is reached. The anamorphism is the function that generates the list of A, B, C, etc. You can think of the anamorphism as unfolding the initial value into a sequence.

In computer science, coinduction is a technique for defining and proving properties of systems of concurrent interacting objects.

In mathematics, the cotangent complex is a common generalisation of the cotangent sheaf, normal bundle and virtual tangent bundle of a map of geometric spaces such as manifolds or schemes. If is a morphism of geometric or algebraic objects, the corresponding cotangent complex can be thought of as a universal "linearization" of it, which serves to control the deformation theory of . It is constructed as an object in a certain derived category of sheaves on using the methods of homotopical algebra.

In representation theory, the stable module category is a category in which projectives are "factored out."

In type theory, a system has inductive types if it has facilities for creating a new type from constants and functions that create terms of that type. The feature serves a role similar to data structures in a programming language and allows a type theory to add concepts like numbers, relations, and trees. As the name suggests, inductive types can be self-referential, but usually only in a way that permits structural recursion.