What category would you place that in?

I’ve decided to spent some time reading up on denotational semantics and concurrency and as a prelude I thought it would be a great idea to read up on some category theory. Despite studying some algebraic topology at college, the course didn’t cover any category theory. I picked up the nice and slim Basic Category Theory For Computer Scientists by Benjamin Pierce which turned out to be a good introduction to the subject. Of course, the only way to get really familiar with the material is to work through the exercises, and as part of that I really needed a way to look at some examples.
 
The obvious answer is to use F# to look at some simple categories. The REPL (read-eval-print loop) makes it easy to take arrows from the category and study their properties in order to find counter-examples. This should be not surprise – ML was originally invented as the implementation language of  the LCF theorem proving system. Theorems could be represented as instances of abstract datatypes within the language, and the datatypes could expose functionality that allowed only valid theorems to be constructed. There is a book which I have just started reading, Computational Category Theory for which the source is available here, which covers some implementation of category theory in ML.
 
A category is basically a collection of objects and arrows with a means for finding the start and end objects of a given arrow, together with a means for getting the identity arrow corresponding to any object and a means of composing the arrows. Of course, there are constraints on these various functions which we cannot express in the type system.
 
type Category<‘arrow, ‘ob> =
  { Start : ‘arrow -> ‘ob; End : ‘arrow -> ‘ob; Identity : ‘ob -> ‘arrow; Compose : ‘arrow -> ‘arrow -> ‘arrow  }
 
We can then define a type representing an arrow, and define a function that generates one of the standard finite categories, that of a preorder on a list of elements where each element is < than the elements to the right of it in a list.
 
type Arrow<‘a> = { From : ‘a; To : ‘a}
 
let GenerateOrderCategory elements =
  let startfn x = x.From
  let endfn x = x.To
  let check x =
    if not (List.mem x elements)
    then failwith "Invalid element for generating identity arrow"
    else x
  let identity x =
    { From = check x; To = x}
  let compose arrow1 arrow2 =
    if check(arrow1.To) = arrow2.From
    then { From =  check arrow1.From; To= check arrow2.To }
    else failwith "Invalid composition"
  { Start = startfn; End=endfn; Identity= identity; Compose=compose }
 
let OrderCategoryArrows elements =
  let rec generate a b sofar =
    if b = []
    then if a = []
         then sofar
         else generate (List.tl a) (List.tl a) sofar
    else generate a (List.tl b) ({ From = List.hd a; To = List.hd b } :: sofar)
  Set.of_seq(generate elements elements [])
 
A finite category can be expressed as a collection of functions representing the category, together with a Set of the arrows.
 
type FiniteCategory<‘arrow, ‘ob> =
  { Category : Category<‘arrow, ‘ob>; Arrows : Set<‘arrow> }
 
We can then define the finite category over a finite set of elements.
 
let OrderCategory elements =
  { Category = GenerateOrderCategory elements; Arrows =  OrderCategoryArrows elements}
 
let cat1 = OrderCategory [1]
let cat2 = OrderCategory [1;2]
let cat3 = OrderCategory [1;2;3]
 
We cannot express the constraints on the fucntions representing the category in the type system, but for a finite category we can loop across all of the arrows to validate that the rules hold.
 
let canCompose category arrow1 arrow2 =
  category.End arrow1 = category.Start arrow2
 
let CheckFiniteCategory finiteCategory =
  let arrows = finiteCategory.Arrows
  let category = finiteCategory.Category
  let mutable objs = Set.empty
  for arrow in arrows do objs <- Set.add (category.Start arrow) objs
  for arrow in arrows do objs <- Set.add (category.End arrow) objs
  // Identities
  for ob in objs do
    let id = category.Identity ob
    if not (Set.mem id arrows && category.Start id = ob && category.End id = ob)
    then failwith "No identity"
  // Well defined
  for a1 in arrows do
    for a2 in arrows do
      if canCompose category a1 a2
      then
        let result = category.Compose a1 a2
        if not (Set.mem result arrows && category.Start result = category.Start a1 && category.End result = category.End a2)
        then failwith "Invalid composition"
  // Associative
  for a1 in arrows do
    for a2 in arrows do
      for a3 in arrows do
        if canCompose category a1 a2 && canCompose category a2 a3
        then
          let r1 = category.Compose (category.Compose a1 a2) a3
          let r2 = category.Compose a1 (category.Compose a2 a3)
          if r1 <> r2 then failwith "Not associative"
  // Check identity composes with f to give f
  for ob in objs do
    let id = category.Identity ob
    for arrow in arrows do
      if canCompose category id arrow && category.Compose id arrow <> arrow
      then failwith "Composing identity and arrow"
      if canCompose category arrow id && category.Compose arrow id <> arrow
      then failwith "Composing arrow and identity"
 
We can then check the categories we have defined.
 
CheckFiniteCategory cat1
CheckFiniteCategory cat2
CheckFiniteCategory cat3
 
For the finite case, we can validate that certain arrows are epi- and mono- morphisms.
 
let isMonomorphism arrow finiteCategory =
  let arrows = finiteCategory.Arrows
  let category = finiteCategory.Category
  Seq.for_all
    (fun g ->
       Seq.for_all
         (fun h ->
           if category.Start g = category.Start h && category.End g = category.End h
           then if canCompose category g arrow
                then if category.Compose g arrow = category.Compose h arrow
                     then g = h
                     else false
                else true
           else true)
         arrows)
    arrows
 
let isEpimorphism arrow finiteCategory =
  let arrows = finiteCategory.Arrows
  let category = finiteCategory.Category
  Seq.for_all
    (fun g ->
       Seq.for_all
         (fun h ->
           if category.Start g = category.Start h && category.End g = category.End h
           then if canCompose category arrow g
                then if category.Compose arrow g = category.Compose arrow h
                     then g = h
                     else false
                else true
           else true)
         arrows)
    arrows
 
isMonomorphism {From=1;To=3} cat3
isEpimorphism {From=1;To=3} cat3;;
 
Another standard example is that of representing a group using arrows and a single object. We can construct it like so.
 
type GroupElement = Element
 
let CycleGroupProduct n =
  let startfn _ = Element
  let endfn _ = Element
  let identity Element = (0,0)
  let compose (a,b) (c,d) = ((a + c) % n, (b+d) % n)
  let category =
    { Start=startfn; End=endfn; Identity=identity; Compose=compose }
  let arrows =
    seq {
          for i in 0 .. n-1 do
          for j in 0 .. n-1 do
          yield (i,j)
        }
  { Category = category; Arrows = Set.of_seq arrows}
 
We can then define the Klein four group as a category and validate the representation.
 
let V4 = CycleGroupProduct 2
CheckFiniteCategory V4
isMonomorphism (0,0) V4
isMonomorphism (1,0) V4
isMonomorphism (1,1) V4
 
There’s much more to do, but at least we have a start.
 
 
Advertisements
This entry was posted in Books. Bookmark the permalink.

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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