Girard on the Limitations of Categories

July 23, 2008

Girard on the Limitations of Categories

Posted by David Corfield

What do people make of Jean-Yves Girard’s entry for CATEGORY in his paper Locus Solum?

Category-theory played an important role in the disclosure of the deep structure of logic : for instance coherent spaces form a categorical model for linear logic, and by the way came from this model, not the other way around. The pregnancy of categories in our area made me style the period 1970-2000 as the time of categories, a period which opened with the Curry-Howard isomorphism. Ludics originates in the category-theoretic approach, but eventually took some distance.

The limitations of categories–insofar as we can judge them from the sole logical viewpoint–lies in their spiritualism, their extreme spiritualism : everything is up to isomorphism. In particular categories cannot explain locative logical constructions such as intersection types–or if you prefer, the categorical viewpoint compelled us to consider these artifacts as non-logical. In the same way, category-theory cannot explain the prenex form of ludics, which are based on equalities and which are definitely impossible to explain by means of isomorphisms.

To sum up, category theory only presents a limited aspect of logic; provided we realise this, it remains a very important tool. (Locus Solum, pp. 96-97)

He has later entries on LOCATIVE LOGIC and on PRENEX FORM.

We were wondering back here whether higher categories met other demands of his.

Posted at July 23, 2008 9:47 AM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1747

11 Comments & 0 Trackbacks

Re: Girard on the Limitations of Categories

I agree that the up to isomorphism aspect of category theory is overstated by category-theoreticians. Allow me to be provocative by in turns stating that many essential categorical structures found in nature are strict anyway: if one is dealing with three systems there is no reason why we should first associate two of these before associating the third one. The natural isos only come in when one wants to model these structures in set-theoretic terms. But this is not necessary if one is happy with a purely diagrammatic formalism, which is inherently strict. So the problem is not category theory but the flavour of it one prefers.

I seem to remember a story of Lawvere punching out Girard. Does anyone have details on this?

Posted by: bob on July 23, 2008 12:55 PM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

$MathML-enabled post (click for more details).$

Bob, tell me you don’t mean that last bit literally.

I agree with you that

the problem is not category theory but the flavour of it one prefers.

Want to consider strict monoidal categories? No problem: they’re monoids in $\mathbf{Cat}$ . The only remotely suspect aspect of that is that it treats $\mathbf{Cat}$ as a 1-category, not a 2-category. But you can treat $\mathbf{Cat}$ as a 1-category, and indeed people do it all the time. There’s nothing that forces you to treat $\mathbf{Cat}$ as a 2-category.

If category theory was really only capable of handling things up to isomorphism, the quest for a theory of (weak) $n$ -categories would presumably have been very easy — we’d have had very little choice about how to proceed. But as it is, we have to think about how to incorporate the weakness satisfactorily. Category theory doesn’t impose a level of strictness on us; we have to choose.

There are other proposed logical systems, e.g. Makkai’s FOLDS, that do impose weakness on the user. (In FOLDS, it’s not possible to assert the equality of two objects of a category.) But category theory itself doesn’t make that imposition.

Posted by: Tom Leinster on July 23, 2008 1:25 PM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

> Bob, tell me you don’t mean that last bit literally.

I do. I heard this from several sources. Lawvere did the same with his head of department at Halifax, and therefore got kicked out. So given Girard’s utterly provocative attitude, and insulting way of phrasing things, not that much of a surprise. I see Mike Wright tomorrow and ask him about this - he should know about these sorts of spicy details.

Posted by: bob on July 23, 2008 1:37 PM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

$MathML-enabled post (click for more details).$

Huh. I confess that I don’t understand what Girard is going on about. In particular, I don’t understand what he means by “locative logical constructions such as intersection types”, let alone “prenex form of ludics”.

Of course I know that one does not speak of the intersection of two objects in a category; rather one speaks of the intersection of two subobjects. But is there a convincing example which shows there is some real logical imposition here?

I did stare at some of his other entries like “locative logic” and “spiritualism” for a few minutes, and came away almost completely unenlightened. The Girardesque style was of course familiar to me (I read a fair amount of Girard while writing my thesis), but here I found it more exasperating than usual, and I begin to wonder what clothes the emperor is wearing now.

Posted by: Todd Trimble on July 23, 2008 3:45 PM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

$MathML-enabled post (click for more details).$

Intersection types $A \wedge B$ are a bit like product types $A \times B$ , but with different introduction and elimination rules. Roughly, a term $e$ has type $A \wedge B$ when it has both types $A$ and $B$ . This is in contrast with product types: a term of type $A \times B$ typically is a pair of terms of types $A$ and $B$ , while for $A \wedge B$ the same term should have both types.

Intersection types have been used, e.g., in lambda-calculus and programming to characterize the strongly normalizing terms, or infer principal typings for programs.

As to Girard’s argument, here is what I understand. Since his early work, which used explicitly typed lambda calculi, Girard now seems to prefer untyped presentations, where types appear as “behaviors”, i.e., sets of realizers, in the sense of Krivine. But, the untyped world is uneasy to turn into a category, since we want one term/morphism $e$ as above to have at least three codomains: $A$ , $B$ , and $A \wedge B$ .

Of course, I am by no means a specialist, and would be interested in reading one on that. For example, is there a well-accepted categorical account of Krivine realizability? Is Robinson and Rosolini’s abstract realizability a good candidate? Are there others?

As a personal bit: I believe Girard is generalizing too much from “there is no categorical approach to untyped realizability – and ludics” to “category theory only presents a limited aspect of logic”. The limitation outlined by Girard is not a limitation of categories as a language for mathematics, but of the paradigm types = objects, programs = morphisms. I happen to have a recent, still sketchy preprint on Multiplicative Additive Linear Logic, which uses categorical language (sheaves, mostly), yet strikingly resembles ludics – to me at least.

Posted by: Tom Hirschowitz on August 5, 2008 10:59 AM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

In the Oxbridge surroundings were game semantics was developed I regularly hear the comment that ludics are a rip-off of game semantics. So you are not the only one to whom categories of games and ludics are very alike.

Posted by: bob on August 5, 2008 12:56 PM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

Right, I sort of agree that ludics is a kind of game semantics. But still, it follows the paradigm type = object (= game) and program = morphism (= strategy).

My point was that it is possible to use categories for computer science outside this paradigm.

Posted by: Tom Hirschowitz on August 5, 2008 1:12 PM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

A more compelling example is perhaps the very active community of directed algebraic topology, lead by Grandis, Raussen, Goubault, etc. They propose a semantics of concurrent programming using (various notions of) directed spaces, and prove directed variants of theorems in algebraic topology, which have a computational meaning.

And their categories have nothing to do with the paradigm Girard seems to keep thinking of.

Posted by: Tom Hirschowitz on August 5, 2008 1:17 PM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

$MathML-enabled post (click for more details).$

Thanks, Tom. Your last paragraph seems a bit more sensible to me than the Girardese I was complaining about.

How would you describe the semantics of this type theory with intersection types? Am I right in thinking that models generally have the flavor of being ccc’s whose objects are subobjects of a suitable model of untyped lambda calculus (= one-object ccc, not including the terminal object), construed as sitting inside an ambient ccc?

Posted by: Todd Trimble on August 5, 2008 6:13 PM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

Don’t know! I’ve never heard of any categorical account of intersection types.
But if you find something that works I’m interested, and probably not the only one.

Posted by: Tom Hirschowitz on August 6, 2008 10:27 AM | Permalink | Reply to this

Re: Girard on the Limitations of Categories

Mauro Piccolo and Claudia Faggian have studied the connection between (a fragment) Ludics and models of computation in detail in the paper
Ludics is a Model for the finitary Linear Pi-Calculus. The close connection between Pi-Calculus and game semantics (see the paper Processes and Games by Honda) can be used to extract a game-theoretic interpretation of Ludics.

Posted by: x3m on August 25, 2008 1:17 PM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

July 23, 2008