===== Initial algebra =====
==== Collection ====
| @#55CCEE: context     | @#55CCEE: ${\bf A}$ ... category of $F$-algebras |
| @#FF9944: definition  | @#FF9944: $\langle I,i\rangle$ ... initial object of ${\bf A}$ |

==== Discussion ====
It can be shown that $\langle FI, F(i)\rangle$ is isomorphic to $\langle I,i\rangle$ and so one can view the initial algebra as fixed point of $F$. It is, then, the most generic and encompassing algebra for which an operation $\alpha:FA\to A$ can make sense. Initial algebras are the categorical semantics for inductive types in type theory.

By definition, the initial $F$-algebra $\langle I,i\rangle$ can in a unique way be mapped into each other $F$-algebra $\langle A,\alpha\rangle$. These unique arrows are called //catamorphisms//. In the examples below, we see how it encodes recursion schemes involving the $\alpha$'s of the respective codomain.

Initial algebras for categories of countable sets and types always exists. 

=== Examples ===
In the following, we give some examples. Note that one can "automatize" some of repeating features of the discussed catamorphisms, see [[http://www.haskell.org/haskellwiki/Catamorphisms|haskellwiki/Catamorphisms]]. I've also translated the examples and the general case Haskell code on [[http://en.wikipedia.org/wiki/Catamorphism|wikipedia/Catamorphism]]. 

$\{\text{Nothing}\}$ is any fixed singleton/unit type, $L+R$ denotes the disjoint union/sum type of $L$ and $R$ and "[left,right]" is notation for a conditional function on $L+R$. Instead of ${\bf Set}$, any category with terminal object, sums and products will do.

  * Consider the [[Maybe]] functor given by $MX:=\{\text{Nothing}\}+X$ and $M(f):=[\_,f]$, where $\_$ just passes the $\text{Nothing}$ from $F(f)$'s domain to the $\text{Nothing}$ of it's codomain. For $M$-algebras, initiality says that for any algebra $\langle A,[e,\mu]\rangle$, there is exactly one arrow $\langle cata\rangle:\langle I,[i_l,i_r]\rangle\to\langle A,[e,\mu]\rangle$. The general condition for arrows in the category of $M$-algebras $cata\circ [i_l,i_r]=[e,\mu]\circ [\mathrm{id},cata]$ implies $cata\circ i_l=e$ and $cata\circ i_r^m=\mu^m\circ cata$. One can show that this is just the definition of the [[Natural numbers object]] of the category. Indeed, the initial algebra turns out to be $\langle \mathbb N,[nil, succ]\rangle$, where $nil(\text{Nothing}):=0$ and $succ(n):=n+1$ and the catamorphism to any algebra is $cata(n):=\mu^n(e)$, so that indeed, $cata(n+m):=\mu^m(cata(n))$. Note how $\mathbb N$ is the most generic solution for "$\{\text{Nothing}\}+X=X$". In fact this is the characterization of the natural numbers in the sense of ordinals: Take the empty set and, step by step, add a new element to the set until you have the countable infinity. 

  * For fixed $A$, the object map $FX:=\{\text{Nothing}\}+(A\times X)$ gives us lists of $A$'s: $\langle \mathrm{List}(A),[nil, cons]\rangle$, where $nil(\text{Nothing}):=\langle\rangle$ and $cons(a,\langle b,c,\dots,z\rangle):=\langle a,b,c,\dots,z\rangle$. Again, note how $\mathrm{List}(A)$ is the fixed point of "$\{\text{Nothing}\}+(A\times X)=X$". Tongue-in-cheek the solution is $X=\frac{1}{1-A}=1+A+A\times A+A\times A\times A+\dots$, which is the set of $A$-lists of arbitrary size.

  * $FX:=A+(X\times X)$ gives trees of $A$'s. Consider "$A+(X\times X)=X$". 

  * Initial algebras for categories of countable sets and types always exists. 

=== Reference ===
Wikipedia: 
[[http://en.wikipedia.org/wiki/Initial_algebra|Initial algbera]],
[[http://en.wikipedia.org/wiki/Catamorphism|Catamorphism]],
[[http://en.wikipedia.org/wiki/Fold_%28higher-order_function%29|Fold]]

Haskellwiki: 
[[http://www.haskell.org/haskellwiki/Catamorphisms|Catamorphisms]]
==== Parents ====
=== Context* ===
[[Category of F-algebras]]
=== Requirements ===
[[Initial object]]