Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
initial_algebra [2014/09/25 15:38] nikolaj |
initial_algebra [2014/09/28 17:37] nikolaj |
||
|---|---|---|---|
| Line 9: | Line 9: | ||
| 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. | 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. | ||
| - | 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]]. | + | Initial algebras for categories of countable sets and types always exists. |
| === Examples === | === Examples === | ||
| - | In the following, $\{\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. | + | 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. | * 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. | ||
| - | |||
| - | <code/Haskell> | ||
| - | {- This first example is academic, because every language already has Nat | ||
| - | in one way or the other. The Tree example below is less obvious. -} | ||
| - | |||
| - | {- Consider the functor F mapping x to "{Nothing} + CopyOf x". | ||
| - | A "StepAlgebra" is a pair (x, [toNil, next]), | ||
| - | where 'toNil Nothing = Nil' and 'next :: CopyOf x -> x'. | ||
| - | Below in the code, we encode (x, [toNil, next]) just via (Nil, next) -} | ||
| - | type StepAlgebra x = (x, x->x) | ||
| - | |||
| - | {- We can define the initial object (Nat, [toZero, Succ]), which is | ||
| - | the most generic StepAlgebra with Zero :: Nat and Succ :: Nat -> Nat -} | ||
| - | data Nat = Zero | Succ Nat | ||
| - | |||
| - | -- For any StepAlgebra (x, [toNil, next]), which we'll encode as (Nil, next), | ||
| - | -- we have the catamorphism 'foldSteps (nil, next)' given by | ||
| - | foldSteps :: StepAlgebra x -> Nat -> x | ||
| - | foldSteps (nil, next) Zero = nil | ||
| - | foldSteps (nil, next) (Succ n) = next $ foldSteps (nil, next) n | ||
| - | |||
| - | -- e.g. iter (7,\x->x+100) (Succ(Succ(Succ(Zero)))) is 307 | ||
| - | </code> | ||
| * 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. | * 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. | ||
| - | |||
| - | <code/Haskell> | ||
| - | {- For any 'a', consider the functor F mapping x to "Nothing + Container a x". | ||
| - | A "ContainerAlgebra" is a pair (x, [toNil, merge]), | ||
| - | where 'toNil Nothing = Nil' and 'merge :: (Container a x) -> x' | ||
| - | Again, in the code we capture (x,[toNil, merge]) via (Nil, merge) -} | ||
| - | type ContainerAlgebra a x = (x, a -> x -> x) | ||
| - | |||
| - | {- We can define the initial object, | ||
| - | which is the most generic Container algebra (List a, [toNil, Cons]), | ||
| - | with Cons :: Container a (List a) -> List a -} | ||
| - | data List a = Nil | Cons a (List a) | ||
| - | |||
| - | -- The catamorphisms 'foldrList (nil, merge)' for a ContainerAlgebra is given by | ||
| - | foldrList :: ContainerAlgebra a x -> List a -> x | ||
| - | foldrList (nil, merge) Nil = nil | ||
| - | foldrList (nil, merge) (Cons v vs) = merge v $ listFoldr (nil, merge) vs | ||
| - | |||
| - | -- e.g. listFoldr (3,\x -> \y -> x*y) (Cons 10 (Cons 100 (Cons 1000 Nil))) is 3000000 | ||
| - | </code> | ||
| * $FX:=A+(X\times X)$ gives trees of $A$'s. Consider "$A+(X\times X)=X$". | * $FX:=A+(X\times X)$ gives trees of $A$'s. Consider "$A+(X\times X)=X$". | ||
| - | <code/Haskell> | + | * Initial algebras for categories of countable sets and types always exists. |
| - | {- For any 'a', consider the functor F mapping 'x' to 'a | MyBranch x x'. | + | |
| - | A "TreeAlgebra" is a pair (x,[f,g]), where f :: a -> x and g :: (MyBranch x x) -> x. | + | |
| - | Below, (x,[f,g]) is encoded as the (f,g), while 'x' is part of the type annotation -} | + | |
| - | + | ||
| - | type TreeAlgebra a x = (a -> x, x -> x -> x) | + | |
| - | + | ||
| - | -- Examples: | + | |
| - | + | ||
| - | treeDepth :: TreeAlgebra a Integer | + | |
| - | treeDepth = (const 1, \i j -> 1 + max i j) | + | |
| - | + | ||
| - | treeSum :: (Num a) => TreeAlgebra a a | + | |
| - | treeSum = (id, (+)) | + | |
| - | + | ||
| - | {- We define the initial object, the most generic tree algebra (Tree a, [Leaf, Branch]), | + | |
| - | with Leaf :: a -> (Tree a) and Branch :: (Tree a) -> (Tree a) -> (Tree a) -} | + | |
| - | + | ||
| - | data Tree a = Leaf a | Branch (Tree a) (Tree a) | + | |
| - | + | ||
| - | {- Finally, 'foldTree (f, g)' is the catamorphism from Tree a to a tree algebra (x, [f, g]) | + | |
| - | This scheme turns any 'TreeAlgebra a x' to a function from Tree a, | + | |
| - | e.g. foldTree treeDepth, foldTree treeSum, ... -} | + | |
| - | + | ||
| - | foldTree :: TreeAlgebra a x -> Tree a -> x | + | |
| - | foldTree (f, g) (Leaf x) = f x | + | |
| - | foldTree (f, g) (Branch left right) = g (foldTree (f, g) left) (foldTree (f, g) right) | + | |
| - | </code> | + | |
| - | + | ||
| - | * More generally, let's abstract the functor $F$ and define the initial algebra as the fixed point 'X=Fix f' in 'f X = X'. The f's come with term constructors for new term of 'f (Fix f)' and 'Iso' maps them back to 'Fix f' | + | |
| - | + | ||
| - | <code/Haskell> | + | |
| - | type Algebra f a = f a -> a -- f-algebra | + | |
| - | newtype Fix f = Iso { invIso :: f (Fix f) } -- fixed point of functor = initial algebra | + | |
| - | cata :: Functor f => (Algebra f a) -> (Fix f -> a) | + | |
| - | cata alg = alg . fmap (cata alg) . invIso | + | |
| - | + | ||
| - | {- Example: For any type 'a', we have 'Nothing :: Maybe a'. Hence | + | |
| - | + | ||
| - | Nothing :: Maybe (Fix Maybe) | + | |
| - | Iso Nothing :: (Fix Maybe) | + | |
| - | (Just . Iso) Nothing :: Maybe (Fix Maybe) | + | |
| - | (Iso . Just . Iso) Nothing :: (Fix Maybe) | + | |
| - | etc. -} | + | |
| - | type Nat = Fix Maybe | + | |
| - | z :: Nat | + | |
| - | z = Iso Nothing | + | |
| - | s :: Nat -> Nat | + | |
| - | s = Iso . Just | + | |
| - | + | ||
| - | alg :: Algebra Maybe String -- example ... recursion on strings | + | |
| - | alg (Just string) = string ++ " + one" | + | |
| - | alg Nothing = "zero" | + | |
| - | + | ||
| - | {- | + | |
| - | cata alg ((s.s) z) | + | |
| - | alg . fmap (cata alg) . invIso $ ((s.s) z) | + | |
| - | alg . fmap (cata alg) . Just $ (s z) | + | |
| - | alg . Just . (cata alg) $ (s z) | + | |
| - | alg . Just . alg . fmap (cata alg) . invIso $ (s z) | + | |
| - | alg . Just . alg . fmap (cata alg) . Just $ z | + | |
| - | alg . Just . alg . Just . (cata alg) $ z | + | |
| - | alg . Just . alg . Just . alg . fmap (cata alg) . invIso $ z | + | |
| - | alg . Just . alg . Just . alg . fmap (cata alg) $ Nothing | + | |
| - | alg . Just . alg . Just . alg $ Nothing | + | |
| - | alg . Just . alg . Just $ "zero" | + | |
| - | alg . Just $ "zero + one" | + | |
| - | "zero + one + one" | + | |
| - | -} | + | |
| - | </code> | + | |
| === Reference === | === Reference === | ||
