Time 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 need to go through to get there are fun.
The first step is to define a *monoidal category*, also known as a *tensor* category. We've already done most of that when we built [monads][monads] earlier this week; a monad is a kind of monoidal category.
A monoidal category is a category C with one object t, and a *binary functor* ⊗ : C × C → C. This binary functor is called *tensor*. Tensor has three required properties defined using *natural isomorphisms*, called α, λ, and ρ.
α says that tensor must be associative: α(A,B,C) : (A ⊗ B) ⊗ C → A ⊗ (B ⊗ C).
λ says that tensor has a *left identity*: λA : (I ⊗ λ) → A.
ρ says that tensor has a *right identity*, which is the same as the left identity: ρA : (ρ ⊗ 1) → A;.
And finally, the natural transformations need to make the following diagrams commute for all values of A, B, and C. These are known as the *coherence conditions* for the monoidal natural transformations.
A monoidal category is said to be *strict* if α, λ, and ρ are all identities. It turns out that for every monoidal category, there is an *equivalent* (in the sense of natural isomorphism) to a struct monoidal category.
And now, here comes an example of just why category theory is useful. In some of the [detailed models of quantum physics][quantum-condense], they try to describe the structure of different kinds of matter using what they call *topological orders*. The standard theory for describing the topological orders to different states of matter is called *Landau* theory. It turns out that Landau theory doesn't describe the topological order of high temperature semiconductors or very-low-temperature condensate states. Category theory - in particular, the theory surrounding strict monoidal categories does a better job of describing the topological order of the different states of matter than any other mathematical approach that's been tried so far.
[monads]: http://scienceblogs.com/goodmath/2006/07/monads_and_programming_languag…
[quantum-condense]: http://dao.mit.edu/~wen/pub/qorder.html
- Log in to post comments
I'm not really qualified to judge these matters seriously, but perusing Wikipedia it seems to verify my feeling that phase transitions and symmetry breakings are a diverse and active field. There are a lot of pointers from Landau theory onwards.
But what I wanted to do was to raise a flag about spin and string nets condensed matter approaches to gauge theories, which are large users of category theory. My feeling is that the main group of string theorists doesn't believe in these approaches much. But what do I know. One paper references Susskind as working on spin nets earlier. And even if true it shouldn't be taken as invalidating category theory for use in theoretical physics.
I'm sure we could make a great deal of progress understanding complex systems if we moved from renormalization groups to renormalization categories instead. (-;
It makes sence to me:)