understanding FF-algebra [math-000E]

2023-10-24 · Lîm Tsú-thuàn

To understand FF-algebra, we will need some observations, the first one is we can summarize an algebra with a signature. For example, monoid has a signature:

{1:1→m⋅:m×m→m\begin{cases} 1 : 1 \to m \\ \cdot : m \times m \to m \end{cases}

or we can say ring is:

{0:1→m1:1→m+:m×m→m×:m×m→m−:m→m\begin{cases} 0 : 1 \to m \\ 1 : 1 \to m \\ + : m \times m \to m \\ \times : m \times m \to m \\ - : m \to m \end{cases}

The next observation is we can consider these mm as objects in a proper category CC, at here is a cartesian closed category. For example

  • monoid is a CC-morphism 1+m×m→m1 + m \times m \to m
  • ring is a CC-morphism 1+1+m×m+m×m+m→m1 + 1 + m \times m + m \times m + m \to m

Now, we generalize algebra's definition.

Definition FF-algebra (algebra for an endofunctor) [math-000F]

2023-10-24

Consider a proper category CC that can encode the signature of F(−)F(-), and an endofunctor F:C→CF : C \to C, the FF-algebra is a triple:

(F,x,α)(F, x, \alpha)

where α:F  x→x\alpha : F \; x \to x is a CC-morphism.

figure tex154132

With the definition of FF-algebra, FF-algebras of a fixed FF form a category

Definition category of FF-algebras [math-000G]

2023-10-24

For a fixed endofunctor FF in a proper category CC (below notations omit fixed FF),

  1. the F-algebras (x,α)(x, \alpha) form the objects of the category,
  2. morphisms are homomorphisms of objects (x,α)→F  m(y,β)(x, \alpha) \xrightarrow{F\;m} (y, \beta), composition is given by functor laws.

A homomorphism is a CC-morphism mm makes below diagram commutes.

figure tex154555

We can extra check identity indeed works.

figure tex154556

There is a theorem about the initial object of the category.

Theorem Lambek's [math-000H]

2023-10-24

The evaluator jj of an initial algebra (F,i,j)(F, i, j) is an isomorphism.

Proof [local-0]

Let F  iF\;i be an initial in the FF-algebra category, the following diagram commutes for any CC-object aa

figure tex154979

Now, replace aa with F  iF\;i, we have commute diagram

figure tex154980

Then we consider a trivial commute diagram by duplicating the path F  i→iF\;i \to i

figure tex154981

Combine two diagrams, then we get another commute diagram

figure tex154982

By definition now we know j∘mj \circ m is a homomorphism, and since F  iF\;i is an initial, we must have

F  j∘F  m=1FiF\;j \circ F\;m = 1_{Fi}

Therefore, we also have

j∘m=1ij \circ m = 1_i

so mm is the inverse of jj, proves jj is an isomorphism.

catamorphism [math-000I]

2023-10-24

The theorem actually proves the corresponding CC-object ii of initial algebra (F,i,j)(F, i, j) is a fixed point of FF. By reversing jj with its inverse, we get a commute diagram below.

figure tex155405

In Haskell, we are able to define initial algebra

newtype Fix f = Fix (f (Fix f))

unFix :: Fix f -> f (Fix f)
unFix (Fix x) = x

View jj as constructor Fix, j−1j^{-1} as unFix, then we can define m = alg . fmap m . unFix. Since m :: Fix f -> a, we have definition of catamorphism.

cata :: Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . fmap (cata alg) . unFix

An usual example is foldr, a convenient specialization of catamorphism.

anamorphism [math-000J]

2023-10-24

As a dual concept, we can draw coalgebra diagram

figure tex155828

and define anamorphism as well.

ana :: Functor f => (a -> f a) -> a -> Fix f
ana coalg = Fix . fmap (ana coalg) . coalg

I mostly learn F-algebras from Category Theory for Programmers, and take a while to express the core idea in details with my voice with a lot practicing. The article answered some questions, but we always with more. What's an algebra of monad? What's an algebra of a programming language (usually has a recursive syntax tree)? Hope you also understand it well through the article and practicing.