Good Math, Bad Math

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 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, 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.