Added to Favorites

${pType}

Definitions

Nearby Words

In mathematics, specifically in category theory, an $F$-algebra for an endofunctor ## Example

## Initial F-algebra

## Terminal F-coalgebra

## See also

## Notes

## External links

- $F\; :\; mathbf\{C\}longrightarrow\; mathbf\{C\}$

is an object $A$ of $mathbf\{C\}$ together with a $mathbf\{C\}$-morphism

- $alpha\; :\; FA\; longrightarrow\; A$.

In this sense F-algebras are dual to F-coalgebras.

A homomorphism from $F$-algebra $(A,\; alpha)$ to $F$-algebra $(B,\; beta)$ is a morphism

- $f:Alongrightarrow\; B$

in $mathbf\{C\}$ such that

- $fcirc\; alpha\; =\; beta\; circ\; Ff$.

Thus the $F$-algebras constitute a category.

Consider the functor $F:\; mathbf\{Set\}\; tomathbf\{Set\}$ that sends a set $X$ to $1+X$. 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 numbers together with the function $[mathrm\{zero\},mathrm\{succ\}]\; :\; 1+Nto\; N$, which is the coproduct of the functions $mathrm\{zero\}\; :\; 1\; to\; N$ (whose image is 0) and $mathrm\{succ\}\; :\; N\; to\; N$ (which sends an integer n to n+1), is an $F$-algebra.

If the category of $F$-algebras for a given endofunctor F has an initial object, it is called an initial algebra. The algebra $(N,\; [mathrm\{zero\},mathrm\{succ\}])$ 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 F-algebra, provided that parametricity holds for the type.

See also Universal algebra.

In a dual way, similar relationship exists between notions of greatest fixed point and terminal F-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.

- 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

Wikipedia, the free encyclopedia © 2001-2006 Wikipedia contributors (Disclaimer)

This article is licensed under the GNU Free Documentation License.

Last updated on Sunday January 20, 2008 at 11:56:15 PST (GMT -0800)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

This article is licensed under the GNU Free Documentation License.

Last updated on Sunday January 20, 2008 at 11:56:15 PST (GMT -0800)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

Copyright © 2014 Dictionary.com, LLC. All rights reserved.