category theory
goodmath | March 11, 2008 Since I mentioned the idea of monoids as a formal models of computations, John
Armstrong made the natural leap ahead, to the connection between monoids and monads - which are
a common feature in programming language semantics, and a prominent language feature in
href="http://scienceblogs.com/goodmath/goodmath/programming/haskell/">Haskell, one of my favorite programming languages.
Monads are a category theoretic construction. If you take a monoid, and use some of the constructions we've seen in the last few posts, we can move build a meta-monoid; that is,
a monoid that's built from…
goodmath | February 28, 2008 By now, we've seen the simple algebraic monoid, which is essentially an
abstract construction of a category. We've also seen the more complicated, but interesting monoidal category - which is, sort of, a meta-category - a category built using categories. The monoidal category is a fairly complicated object - but it's useful.
What does a algebraic monoid look like in category theory? The categorical monoid is a complex object - a monoid built from monoids. If we render the algebraic monoid in terms of a basic category, what do we get? A monoid is, basically, a category with one object. That'…
goodmath | February 18, 2008 In the last post on groups and related stuff, I talked about the algebraic construction of monoids. A monoid is, basically, the algebraic construction of a category - it's based on the same ideas, and has the same properties; just the presentation of it is different.
But you can also see a monoid in categorical terms. It's what we computer scientists would call a bootstrapped definition: we're relying on the fact that we have all of the constructs of category theory, and then using category theory to rebuild its own basic concepts.
The basic idea of the construction is to start pretty much…
goodmath | February 7, 2008 This post started out as a response to a question in the comments of my last post on groupoids. Answering those questions, and thinking more about the answers while sitting on the train during my commute, I realized that I left out some important things that were clear to me from thinking about this stuff as I did the research to write the article, but which I never made clear in my explanations. I'll try to remedy that with this post.
So - in the last post I explained a bit about the categorical viewpoint on why
we should care about groupoids. Every groupoid contains groups. The groups…
goodmath | February 5, 2008 In my introduction to groupoids, I mentioned that if you have a groupoid, you can find
groups within it. Given a groupoid in categorical form, if you take any object in the
groupoid, and collect up the paths through morphisms from that object back to itself, then
that collection will form a group. Today, I'm going to explore a bit more of the relationship
between groupoids and groups.
Before I get into it, I'd like to do two things. First, a mea culpa: this stuff is out on the edge of what I really understand. My category-theory-foo isn't great, and I'm definitely
on thin ice here. I think…
goodmath | January 24, 2008 Today's entry is short, but sweet. I wanted to write something longer, but I'm very busy at work, so this is what you get. I think it's worth posting despite its brevity.
When we look at groups, one of the problems that we can notice is that there are things
that seem to be symmetric, but which don't work as groups. What that means is that despite the
claim that group theory defines symmetry, that's not really entirely true. My favorite example of this is the fifteen puzzle.
The fifteen puzzle is a four-by-four grid filled with 15 tiles, numbered from 1 to 15, and one empty space. You can…
goodmath | January 20, 2008 So far, I've spent some time talking about groups and what they mean. I've also given a
brief look at the structures that can be built by adding properties and operations to groups -
specifically rings and fields.
Now, I'm going to start over, looking at things using category theory. Today, I'll start
with a very quick refresher on category theory, and then I'll give you a category theoretic
presentation of group theory. I did a whole series of articles about category theory right after I moved GM/BM to ScienceBlogs; if you want to read more about category theory than this brief…
goodmath | January 31, 2007 As promised, I'm finally going to get to the theory behind monads. As a quick
review, the basic idea of the monad in Haskell is a hidden transition function - a
monad is, basically, a state transition function.
The theory of monads comes from category theory. I'm going to assume you know
a little bit about category theory - if you have trouble with it, go take a look
at my introductory posts here.
Fundamentally, in category theory a monad is a category with a particular kind of
structure. It's a category with one object. That category has a collection of
arrows which (obviously) are from…
goodmath | December 12, 2006Suppose we've got a topological space. So far, in our discussion of topology, we've
tended to focus either very narrowly on local properties of **T** (as in manifolds, where locally, the space appears euclidean), or on global properties of **T**. We haven't done much to *connect* those two views. How do we get from local properties to global properties?
One of the tools for doing that is a sheaf (plural "sheaves"). A sheaf is a very general kind of structure that provides ways of mapping or relating local information about a topological space to global information about that space. There are…
goodmath | September 25, 2006This is going to be a short but sweet post on topology. Remember way back when I started writing about category theory? I said that the reason for doing that was because it's such a useful tool for talking about other things. Well, today, I'm going to show you a great example of that.
Last friday, I went through a fairly traditional approach to describing the topological product. The traditional approach not *very* difficult, but it's not particularly easy to follow either. The construction isn't really that difficult, but it's not easy to work out just what it all really means.
There is…
goodmath | August 10, 2006This is one of the last posts in my series on category theory; and it's a two parter. What I'm going to do in these two posts is show the correspondence between lambda calculus and the [cartesian closed categories][ccc]. If you're not familiar with lambda calculus, you can take a look at my series of articles on it [here][lambda]. You might also want to follow the CCC link above, to remind yourself about the CCCs. (The short refresher is: a CCC is a category that has an exponent and a product, and is closed over both. The product is an abstract version of cartesian set product; the exponent…
goodmath | August 9, 2006Sorry for the delay in the category theory articles. I've been busy with work, and haven't had time to do the research to be able to properly write up the last major topic that I plan to cover in cat theory. While doing my research on closed cartesian categories and lambda calculus, I came across this little tidbit that I hadn't seen before, and I thought it would be worth taking a brief diversion to look at.
Category theory is sufficiently powerful that you can build all of mathematics from it. This is something that we've known for a long time. But it's not really the easiest thing to…
goodmath | July 31, 2006Today we'll finally get to building the categories that provide the model for
the multiplicative linear logic. Before we jump into that, I want to explain why it is that we separate out the multiplicative part.
Remember from the simply typed lambda calculus, that [we showed that the type system was precisely a subset of intuitionistic logic][lambda-type], and that programs in the lambda calculus corresponded to proofs in the type system. In particular, it was propositional intuitionistic logic using only the "→" operation. Similarly, if you build up a more interesting typed lambda calculus…
goodmath | July 26, 2006Things are a bit busy at work on my real job lately, and I don't have time to put together as detailed a post for today as I'd like. Frankly, looking at it, my cat theory post yesterday was half-baked at best; I should have held off until I could polish it a bit and make it more comprehensible.
So I'm going to avoid that error today. Since we've had an interesting discussion focusing on the number zero, I thought it would be fun to show what zero means in category theory.
There are two zeros it category theory: the zero object, and the zero arrow.
Zero Objects
--------------
The zero object…
goodmath | July 25, 2006So, we're still working towards showing the relationship between linear logic and category theory. As I've already hinted, linear logic has something to do with certain monoidal categories. So today, we'll get one step closer, by talking about just what kind of monoidal category. As I keep complaining, the problem with category theory is that anytime you want to do something interesting, you have to wade through a bunch of definitions to set up your structures. I'll do my best to keep it short and sweet; as short as it is, it'll probably take a bit of time to sink in.
First, we need a…
goodmath | July 19, 2006Time to come back to category theory from out side-trip. Category theory provides a good framework for defining linear logic - and for building a Curry-Howard style type system for describing computations with *state* that evolves over time. Linear logic provides a way of defining a valid *model* for part of linear logic (the multiplicative operators) that aren't tractable using other modeling techniques.
I'm going to show you the relationship between models for linear logic and category theory. It's going to take a couple of days to go through the whole shebang, but even the parts that we…
goodmath | July 18, 2006[Monday][yesterday], I said that I needed to introduce the sequent calculus, because it would be useful for describing things like linear logic. Today we're going to take a quick look at linear logic - in particular, at *propositional* linear logic; you can expand to predicate linear logic in a way very similar to the way we went from propositional logic to first order predicate logic.
So first: what the heck *is* linear logic?
The answer is, basically, logic where statements are treated as *resources*. So using a statement in an inference step in linear logic *consumes* the resource. This is…
goodmath | July 17, 2006*(This post has been modified to correct some errors and add some clarifications in response to comments from alert readers. Thanks for the corrections!)*
Today, we're going to take a brief diversion from category theory to play with
some logic. There are some really neat connections between variant logics and category theory. I'm planning on showing a bit about the connections between category theory and one of those, called *linear logic* . But the easiest way to present things like linear logic is using a mechanism based on sequent calculus.
Sequent calculus is a deduction system for…
goodmath | July 12, 2006One of the questions that a ton of people sent me when I said I was going to write about category theory was "Oh, good, can you please explain what the heck a *monad* is?"
The short version is: a monad is a category with a functor to itself. The way that this works in a programming language is that you can view many things in programming languages in terms of monads. In particular, you can take things that involve *mutable state*, and magically hide the state.
How? Well - the state (the set of bindings of variables to values) is an object in a category, State. The monad is a functor from…
goodmath | July 11, 2006So, at last, we can get to Yoneda's lemma, as I [promised earlier][yoneda-promise]. What Yoneda's lemma does is show us how for many categories (in fact, most of the ones that are interesting) we can take the category C, and understand it using a structure formed from the functors from C to the category of sets. (From now on, we'll call the category of sets **Set**.)
So why is that such a big deal? Because the functors from C to the **Set** define a *structure* formed from sets that represents the properties of C. Since we have a good intuitive understanding of sets, that means that Yoneda's…