Initial algebra

Collection

context ${\bf A}$ … category of $F$-algebras
definition $\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 haskellwiki/Catamorphisms. I've also translated the examples and the general case Haskell code on 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.

Reference

Wikipedia: Initial algbera, Catamorphism, Fold

Haskellwiki: Catamorphisms

Parents

Context*

Category of F-algebras

Requirements

Initial object