1. goodmath
  2. The Category Structure for Linear Logic

The Category Structure for Linear Logic

By goodmath on July 25, 2006.

So, 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 symmetry property. A monoidal category C (with terminal object t, tensor ⊗, and natural isomorphisms λ, ρ) is *symmetric* if/f for all objects a and b in C, there is a natural isomorphism γa,b : (a ⊗ b) → (b ⊗ a); and the categories monoidal natural isomorphism ρ = λb º γb,t : (b ⊗ t) → b.

In other words, if you reverse the arrows, but leave everything else the same, you still wind up with a monoidal category.

In a similar vein: regular functors are also sometimes called *covariant* functors. If you take a functor and *reverse* the directions of all the arrows, you get what's known an a *contravariant* functor, or *cofunctor*.

We also need a *closure* property. Suppose C is a symmetric monoidal category. C is *monoidally closed* if/f there is a functor ⇒ : C × C → C, such that for every object b in C, there is an isomorphism Λ : (a⊗b → c) → (a → (b ⇒ c)), and Λ is a natural transformation for a and c. (Remember that a and c are categories here; this is a natural transformation from category to category.)

Basically, this just says that the tensor stays cleanly in the monoid, and there's always a natural transformation corresponding to any use of tensor.

So what these two really do is pull up some of the basic category properties (closure with respect to composition, symmetry) and apply them to categories and natural transformations themselves.

Finally, we need to be able to talk about what it means for a *functor* to be closed. So suppose we have a monoidally closed category, with the usual components, up to and including the Λ natural transformation. A functor F : C → C is *closed* if, for all a,b in C, there is an arrow fa,b : ba → F(b)F(a) such that for all g : a → b, fa,b º Λ(gº λa) = Λ(F(g) º λF(a)).

In simple english, what a closed functor is is a functor that can be *represented by* an arrow in the category itself. That's what all of that gobbledygook really means.

So... as a quick preview, to give you an idea of why we just waded through all of this gunk: if you take a monoidally closed category of the appropriate type, then collections of resources are going to be categories; ⊗ is the tensor to join collections of resources; and "-o" implications are the closed functors "⇒".

Tags
category theory
goodmath
Logic

More like this

This is getting fun! On to Monoidal Categories.
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…
More Category Theory: Getting into Functors
Let's talk a bit about functors. Functors are fun! What's a functor? I already gave the short definition: a structure-preserving mapping between categories. Let's be a bit more formal. What does the structure-preserving property mean? A functor F from category C to category D is a mapping from C…
Category Theory: Natural Transformations and Structure
The thing that I think is most interesting about category theory is that what it's really fundamentally about is structure. The abstractions of category theory let you talk about structures in an elegant way; and category diagrams let you illustrate structures in a simple visual way. Morphisms…
Big to Small, Small to Big: Topological Properties through Sheaves (part 1)
Suppose 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.…

I don't think cofunctor is standard. Functors come in two types contravariant ( what you called cofunctor) and covariant (what you called functor). A contravariant functor is a functor from the opposite category.

If C is a category the opposite of C, C^{op} is the category with the same objects, but with all the arrows turned around.

That is if A,B in C then Hom_{C^{op}}(A,B) = Hom_C(B,A)

The opposite category is one of the more useful ideas in Category theory. For example if C is an abelian category then so is C^op. (Abelian means that Hom(A,B) is an abelian group among other things)
This allows dualizing proofs.
Kernels products, and limits correspond to Cokernels coproducts colimits in the opposite category and visa verse.
So for example a theorem about limits becomes a theorem about colimits, provide the opposite category also satisfies the hypothesis of the theorem.

elspi:

Unless I'm seriously mis-remembering something, there's a reason why the functors and the cofunctors are different. The cofunctors are functors in the dual category, but with respect to the category that you're looking at, contravariant functors are *not* functors, in that they do not respect composition rules correctly. Covariant functors, aka "normal" functors, are the ones that are "well-behaved" with respect to the morphisms in the category and compositions.

yeh
A contravariant functor is a convarient functor with "domain" the oposite category. That is $f: C->D $ is contravariant means that $f:C^{op} ->D$ is a covarariant functor.

In standard usage, functor means both covariant and contravariant.

WARING: I am not a Category theorist, I just am forced to do homological algebra now and then.