Archive for: September, 2011

Leading up to Topoi: Getting Back to Categories

Sep 30 2011 Published by under Category Theory

As I mentioned a few posts ago, I recently changed jobs. I left Google, and I'm now working for foursquare. Now that I'm done with the whole job-hunting thing, and things are becoming relatively saner and settling down, I'm trying to get back to blogging.

One thing that I've been wanting to spend some time learning about is Topoi theory. Topoi theory is an approach to building logic and mathematics using category theory as a fundamental basis instead of set theory. I've been reading the textbook Topoi: The Categorial Analysis of Logic (Dover Books on Mathematics), and I'll be blogging my way through it. But before I get started in that, I thought it would be a good idea to revise and rerun my old posts on category theory.

To get started, what is category theory?

Back in grad school, I spent some time working with a thoroughly insane guy named John Case who was the new department chair. When he came to the university, he brought a couple of people with him, to take temporary positions. One of them was a category theorist whose name I have unfortunately forgotten. That was the first I'd ever heard of cat theory. So I asked John what the heck this category theory stuff was. His response was "abstract nonsense". I was astonished; a guy as wacky and out of touch with reality as John called something abstract nonsense? It turned out to be a classic quotation, attributed to one of the founders of category theory, Norman Steenrod. It's silly and sarcastic, but it's also not an entirely bad description. Category theory takes abstraction to an extreme level.

Category theory is one of those fields of mathematics that fascinates me: where you take some fundamental concept, and abstract it down to its bare essentials in order to understand just what it really is, what it really means. Just like group theory takes the idea of an algebraic operation, strip it down to the bare minimum, and discovering the meaning of symmetry; category theory looks at what happens if you take the concept of a function as a mapping from one thing to another, and strip it down to the bare minimum, and see what you can discover?

The fundamental thing in category theory is an arrow, also called a morphism. A morphism is an abstraction of the concept of homomorphism, which I talked about a bit when I was writing about group theory. Category theory takes the concept function mapping from one set of values to another, and strips it down to itsbarest essentials: the basic concept of something that maps from one thing to some other thing.

The obvious starting point for our exploration of category theory is: what the heck is a category?

To be formal, a category \(C\) is a tuple: \((O, M, circ)\), where:

  1. \(O\) (or \(Obj(C)\)) is a set of objects. Objects can be anything, so long as they're distinct, and we can tell them apart. All that we're going to do is talk about mappings between them - so as long as we can identify them, it doesn't matter what they really are. We'll look at categories of sets, of numbers, of topological spaces, and even categories of categories.

  2. \(M\) (or \(Mor(C)\)) is a set of morphisms, also called arrows. Each morphism is a mapping from an object in \(O\) called its source, to an object in \(O\) called its target. Given two objects \(a\) and \(b\) in \(O\), we'll write \(Mor(a,b)\) for the set of morphisms from \(a\) to \(b\). To talk about a specific morphism \(f\) from \(a\) to \(b\), we'll write it as \(f : a rightarrow b\).
  3. \(circ\) is the composition operator: \(dot\) is a binary operation that is the abstraction of function composition; \(circ\); given an arrow \(f in Mor(a,b)\), and an arrow \(g in Mor(b,c)\), \(f circ g in Mor(a,c)\). It's got the basic properties of function composition:

    1. Associativity: \(forall f : a rightarrow b, g : b rightarrow c, h : c =rightarrow d) h circ (g circ f) = (h circ g) circ f\).
    2. Identity: \(forall a,b in O(C): exists 1_a, 1_b in Mor(C): forall f : a rightarrow b: 1_b circ f = f = f circ 1_a\).

One neat little trick to simplify things is that we can actually throw away Obj(C), and replace it with the set of identity morphisms: since there is exactly one identity morphism per object, there's no real need to distinguish between the identity morphism and the object. It's a nice trick because it means that we have nothing but morphisms all the way down; but it's really just a trick. We can talk about \(Obj(C)\); or \(Id(C)\); but we still need to be able to talk about the objects in some way, whether they're just a subset of the morphisms, or something distinct.

Now, we get to something about category theory that I really don't like. Category theory is front-loaded with rather a lot of definitions about different kinds of morphisms and different kinds of categories. The problem with that is that these definitions are very important, but we don't have enough of the theory under our belts to be able to get much of a sense for why we should care about them, or what their intuitive meaning is. But that's the way it goes sometimes; you have to start somewhere. It will make sense eventually, and you'll see why these definitions matter.

There are a lot of special types of morphisms, defined by properties. Here's the basic list:

  • A monomorphism (aka a monic arrow ) is an arrow \(f : a rightarrow b\) such that \(forall g_1, g_2: x rightarrow a: f circ g_1 = f circ g_2 Leftrightarrow g_1 = g_2\). That is, \(f\) is monic if and only if, when composed with other arrows, it always produces different results for different arrows.
  • An epic (or epimorphism) is an arrow \(f : a rightarrow b\) such that \(forall g_1, g_2: b rightarrow x): g_1 circ f = g_2 circ f Leftrightarrow g_1 = g_2\). This is almost the same as a monic, but it's from the other side of the composition; instead of \(f circ g_i\) in the definition, it's \(g_i circ f\); so an arrow is epic if when another arrow is composed with \(f\), it always produces different results for different arrows.
  • An isomorphism is an arrow \(f : a rightarrow b\) such that \(exists g: b rightarrow a: f circ g = 1_b land g circ f = 1_a\) - an isomorphism is, basically, a reversible arrow: there's a morphism that always reverses the action of an iso arrow.
  • An endomorphism is an arrow \(f : a rightarrow b\) where \(a = b\). It's sort of like a weak identity arrow.
  • An automorphism is an arrow that is both an endmorphism and an isomorphism.

One last definition, just because it gives me a chance to point out something useful about category theory. A functor is a morphism in the category of all categories. What that means is that it's a structure-preserving mapping between categories. It's neat in a theoretical way, because it demonstrates that we're already at a point where we're seeing how category theory can make it easier to talk about something complicated: we're using it to describe itself! But the concept of functor also has a lot of applications; in particular, the module system of my favorite programming language makes extensive use of functors.

In Ocaml, a module is something called a structure, which is a set of definitions with constrained types. One of the things you often want to be able to do is to write a piece of code in a way that allows you to make it parametric on some other structure. The way you do that is to write a functor: a "function" from a structure to a structure. For example, to implement a generic binary tree, you need a type of values that you'll put in the tree; and an operation to compare values. The way you do that is to write a functor which takes a structure defining a type and a comparison operator, and mapping it to a structure which is an implementation of a binary tree for that type and comparison.

The Ocaml functor is a category theoretic functor: category theory provides an easy way to talk about the concept of the compile-time "function" from structure to structure.

26 responses so far

A Taste of Specification with Alloy

Sep 24 2011 Published by under Program Specification, Programming

In my last post (which was, alas, a stupidly long time ago!), I talked a bit about software specification, and promised to talk about my favorite dedicated specification tool, Alloy. Alloy is a very cool system, designed at MIT by Daniel Jackson and his students.

Alloy is a language for specification, along with an environment which allows you to test your specifications. In a lot of ways, it looks like a programming language - but it's not. You can't write programs in Alloy. What you can do is write concise, clear, and specific descriptions of how something else works.

I'm not going to try to really teach you Alloy. All that I'm going to do is give you a quick walk-though, to try to show you why it's worth the trouble of learning. If you want to learn it, the Alloy group's website has a really good the official Alloy tutorial. which you should walk through.

Continue Reading »

11 responses so far