 | This article needs additional citations for verification .(December 2017) |
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.
Consider the endofunctor F : Set → Set sending X to 1 + X, where 1 is the one-point (singleton) set, the 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 X → X. Define
and
Then the set N of natural numbers together with the function [zero,succ]: 1 + N → N 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: A → A 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.
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 × X → X. To define such a function, we need a point and a function N × X → X. 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.
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': X ⇸ Y whose domain is formed by those for which f(x) belongs to 1. Such a structure can be viewed as a chain of sets, X0 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 in the category, 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.
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]
In mathematics, an associative algebraA is an algebraic structure with compatible operations of addition, multiplication, and a scalar multiplication by elements in some field K. The addition and multiplication operations together give A the structure of a ring; the addition and scalar multiplication operations together give A the structure of a vector space over K. In this article we will also use the term K-algebra to mean an associative algebra over the field K. A standard first example of a K-algebra is a ring of square matrices over a field K, with the usual matrix multiplication.
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 inverse limit is a construction that allows one to "glue together" several related objects, the precise gluing process being specified by morphisms between the objects. Thus, inverse limits can be defined in any category although their existence depends on the category that is considered. They are a special case of the concept of limit in category theory.
In mathematics, the Yoneda lemma is arguably the most important 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 with non-mutable states to do things such as simulate for-loops; see Monad.
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.
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 category theory, the concept of catamorphism denotes the unique homomorphism from an initial algebra into some other 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 representation theory, the stable module category is a category in which projectives are "factored out."
In mathematics, a topos is a category that behaves like the category of sheaves of sets on a topological space. Topoi behave much like the category of sets and possess a notion of localization; they are a direct generalization of point-set topology. The Grothendieck topoi find applications in algebraic geometry; the more general elementary topoi are used in logic.
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.
