Initial Algebras: Part II

In the last post we looked at functor algebras and properties of morphisms (arrows) between them. In this post we’ll explore initial functor algebras (or initial F-Algebras).

The Cliffhanger

The last episode ended with a question on whether it is always possible to have a consistent morphism from (Int, intAlgebra) to an arbitrary algebra. The answer, it turns out, is no.

This can be illustrated with a very important counter-example, the algebra ([Int], intListAlgebra) with

intListAlgebra :: Func [Int] -> [Int]
intListAlgebra E = []
intListAlgebra (Func x xs) = x:xs

The limitation is actually more general — no Func-algebra of the form (Int, coerce) can have a function to ([Int], intListAlgebra). For an informal proof, think about this (we’ll talk in the terminology introduced in the last post):

Consider the case when the initial Func Int is of the form Func a b. The first path morphs Func a b to frob (coerce (Func a b)) while the second path maps it to a:frob b. Let the data-type Int be able to represent N unique values and let frob map these N unique values to M unique values. In other words, let the cardinality of frob‘s range be M. Then the number of possible values of frob (coerce (Func a b)) is at most M while the number of possible values of a:frob b is N * M. Therefore the two paths can not represent the same mapping — their ranges are different.

Initial Algebras

However, the ([Int], intListAlgebra) algebra is special in a way — we can always find a function from ([Int], intListAlgebra) to any arbitrary Func-algebra. In Haskell, we should be able to implement this function:

createArrow :: (Func c -> c) -> [Int] -> c

The createArrow function is surprisingly easy to create. As earlier, we proceed with the case analysis of the Func [Int] we have to start with. The function we’re looking for is f :: [Int] -> C.

When the initial value is E, we require (f (intListAlgebra E)) = (algC ((fmap f) E)). Using the definition of fmap and intListAlgebra(which we already know), we get f [] = algC E.

When the initial value is Func x y, we require f (intListAlgebra (Func x y))) = (algC ((fmap f) (Func x y))). This simplifies to (again, using the known, fixed definitions) f (x:y) = algC (Func x (f y)).

The above two observations have just given us a nice, recursive, definition of f! 🙂 The definition of createArrow automatically follows:

createArrow algC [] = algC E
createArrow algC (x:xs) = algC (Func x (createArrow algC xs))

Moreover, it looks a lot like a foldr:

createArrow algC xs = foldr (a b -> algC (Func a b)) (algC E) xs

Such F-algebras, which have mappings to all other F-algebras are called initial algebras, and ([Int], intListAlgebra) is one. It also is a terminal co-algebra (co-algebras which have a function from all other co-algebras) but we won’t talk about them now. This dualism exists because Haskell doesn’t differentiate between inductive and co-inductive data structures. I wish it did. 🙂

Lambek’s Lemma

Lambek’s lemma states that if a functor has an initial algebra, the initial algebra is a fixed point of the functor. Above, we can see that [Int] is, indeed, the fixed point of the Func. Alternatively, it says the (Func [Int] -> [Int]) we came up with is an isomorphism — it has an inverse; which is also something apparent from the above example.

Why I find F-algebra’s interesting

I decided to read up a little bit on this topic when I realized that I could use arrows between F-algebras to represent correctness preserving compilations. For instance, consider a simple evaluator for arithmetic expressions:

data Arith a = Add a a | Sub a a | If a a a | Atom Int
-- Define fmap the usual way
data StackLang = PushSL Int | AddSL | SubSL | IfSL

stackAlg :: Arith [StackLang] -> [StackLang]
stackAlg (Add a b) = AddSL:(a ++ b)
stackAlg (Sub a b) = SubSL:(a ++ b)
stackAlg (If a b c) = IfSL:(a ++ b ++ c)
stackAlg (Atom a) = [PushSL a]

runStack :: [StackLang] -> Int
runStack stack = head $ horse stack []
  where horse (PushSL a:r) s = horse r (a:s)
        horse (AddSL:r) (x:y:s) = horse r (x + y:s)
        horse (SubSL:r) (x:y:s) = horse r (x - y:s)
        horse (IfSL:r) (x:t:f:s) =
          horse r ((if x /= 0 then t else f):s)
        horse [] s = s

eval :: Arith Int -> Int
eval a = {- usual -}

Now, if we can show that runStack is an arrow from (Arith [StackLang], stackAlg) to Arith Int, we will have proved that one step of compiling a top level expression to a stack-machine language preserves semantics. By structural induction, we can then prove the whole compilation process semantics-preserving.

We know that we have always have an arrow (rather a unique arrow) from the fixed point of Arith (finite expressions in this toy expression language) to any arbitrary algebra. Specifically, the arrow to eval should tell us something about how we recursively combine results of evaluating sub-trees into a value.

I’m still quite new to all this, but, so far, Category Theory looks rather interesting and I’m probably going to spend some more time on it.

This entry was posted in Computers and tagged , , , , . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s