nLab catamorphism

 Idea

In the study of recursion schemes, a catamorphism is the simple case of a fold over an inductive data type. In category theoretic terms, this is simply the unique homomorphism out of an initial algebra.

Definition

Given an endofunctor $F$ such that the category of $F$-algebras has an initial object $(\mu F, in)$, the catamorphism for an $F$-algebra $(A, \varphi)$ is the unique homomorphism from the initial $F$-algebra $(\mu F, in)$ to $(A, \varphi)$. The unique morphism between the carriers is also denoted $cata \varphi \colon \mu F \rightarrow A$.

From the commuting square of the homomorphism, we have $(cata \varphi) \circ in = \varphi \circ F (cata \varphi)$. By Lambek's theorem, $\mathit{in}$ has an inverse $\mathit{out}$, so the catamorphism can be recursively defined by $cata \varphi = \varphi \circ F (cata \varphi) \circ out$.

Properties

Fusion law

Lemma

Let $h \colon A \rightarrow B$ be a homomorphism between two $F$-algebras $\varphi \colon F A \rightarrow A$ and $\psi \colon F B \rightarrow B$ so that $h \circ \varphi = \psi \circ F h$. Then $h \circ cata \varphi = cata \psi$.

As a recursion scheme

If $\mu F$ is an inductive type, then the catamorphism is a fold over the type. Some recursive functions can then be implemented in terms of a catamorphism.

Example: Natural numbers

Let $F$ be the functor $F X = 1 + X$ so that the naturals $\mathbb{N} = \mu F$ are represented by the fixed point of $F$ (i.e. the carrier of the initial F-algebra). The recursor for the naturals can then be defined by a catamorphism.

$$\begin{array}{l l} natrec &: \forall A. A \rightarrow (A \rightarrow A) \rightarrow \mathbb{N} \rightarrow A \\ natrec & A z s = cata \varphi, where \\ & \varphi (inl \ast) = z \\ & \varphi (inr n) = s n \end{array}$$

References

• HaskellWiki, Catamorphisms

• Wikipedia, Catamorphism

• Richard Bird, Oege de Moor (1997), Algebra of Programming, Prentice Hall

• Maarten M. Fokkinga (1992), Law and Order in Algorithmics, PhD thesis, University of Twente

• Roland C. Backhouse, Peter J. de Bruin, Ed Voermans, Jaap van der Woude (1991), Relational Catamorphisms, Computing Science Notes, Vol. 9111, Technische Universiteit Eindhoven