Re: What about biproducts?
Dear all, To please George (who claimed zero knowledge!) I should say something about the meaning of linear to the linear logic community and, maybe, head off an over-enthusiastic scramble to adopt "linear" :-) ... Of course this does not mean there is anything wrong with the word linear .... in fact, it is a VERY attractive word: so much so that it is (unfortunately) one of those over-used snappy words which I particularly like! First a disclaimer: I do not claim to be a huge expert on what linear logicians actually mean by "linear"!!! Indeed, the meaning of the word -- to linear logicians -- has definitely changed and expanded over time. Indeed as linear logic developed the word "linear" tended to travel with researchers as they focused on their favourite aspects of the logic ... even if it was not, perhaps, the original motivation for using the word (e.g "linear bicategories", "linear functors" etc.). Undoubtedly, a significant motivation for using the word comes from the resource sensitive nature of the multiplicative connectives of linear logic -- Girard (who invented and named the logic) certainly understood the analogy between the behavior of the multiplicatives and that of the tensor product in linear algebra. Thus, the first significant direction in which the word moved was to describe resources which can be neither duplicated nor destroyed. Another important aspect of linear logic was to provide a non-degenerate proof theory for a logic with a negation. Recall that the (standard) proof theory of any boolean logic is necessarily posetal ... which for a proof theorist is a rather disappointing state of affairs. Girard had cleverly by-passed this obstruction by separating the connectives to model "linear behavior" (the multipicative connectives tensor and par) and "classical behavior" (the product and coproduct). He noticed that allowing a "negation" only for the linear connectives then does not cause a collapse of the proof theory. Indeed, as Robert Seely subsequently pointed out, the proof theory can then be modeled perfectly by Barr's *-autonomous categories. However, Girard had also observed that in such settings there is often a way to reintroduce the ability to duplicate and destroy linear resources. This involves introducing a modality into the setting written !(A) and sometimes called "bang". Categorically this is a monoidal comonad with a Seely isomorphism, !(A \x B) = !A \ox !B whose coKleisli category allows the linear resources to be duplicated and destroyed. This was also a key aspect of linear logic. Thus the word "linear" also started to get caught up with the comonad (e.g Hyland and Shalk use the term "linear exponential monad"). Now monads are linked to adjunctions. Thus, it is a natural step to view the comonad as arising from an adjunction between two categories one of which is linear (in the resource sense) and the other "classical" or cartesian. Linear logicians, had stared at this situation, from the linear end, however, one can also stare at it from the "classical" end. On this end there is an (abstract) coKelisli category. Such categories have, sitting inside them, an image of the "linear" maps which can actually be picked out as being the maps which are natural with respect to the liftings of the counit of the adjunction back into the coKleisli "classical" end (which give an unnatural transformation). This ends up being a bit technical but the overall point is that one finishes with a nice "classical" setting (= has products, possibly coproducts and cartesian closed) in which certain maps can be picked out as being special ... and of course they are ofen called the "linear" maps. This situation then itself becomes interesting to study ... and it seems to be a situation which occurs quite frequently in mathematics. Rick Blute, Robert Seely, Geoff Crutwell, Jonathan Gallager and I, for example, are working on categories with a notion of differentiation ("differential categories" of various stripes) these crop up (besides, of course, in calculus) in Computer Science as they are related to various resource calculi. Now if you can differentiate there are immediately certain special maps: namely those whose differential is a constant ... and these are called, well, "linear" maps. Furthermore they also often arise from the situation I described above. Indeed our work was motivated by Thomas Ehrhard who had developed examples of the linear logic end of this story. These settings also have the vestige of a commutative monoid enrichment (we call them "left-additive") and there is a natural subcategory of "additive" maps which form a commutative monoid enriched (= "additive") subcategory (which also has biproducts so is a category with biproducts). Annoyingly, while every linear map lives in this subcategory, not every additive map need be linear! If you are still with me, I hope you begin to see why I commented that linear was not attractive to us as a name for commutative monoid enriched! However, this does not mean "linear" or, as Todd suggested "N-linear", should not be used locally to mean "commutative monoid enriched" it is just a reason why it does not seem to work well in the area where we are working given the terminology which has developed there. -robin (Robin Cockett) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 1/13/2012 11:35 PM, Robin Cockett wrote:
First a disclaimer: I do not claim to be a huge expert on what linear logicians actually mean by "linear"!!! Indeed, the meaning of the word -- to linear logicians -- has definitely changed and expanded over time. Indeed as linear logic developed the word "linear" tended to travel with researchers as they focused on their favourite aspects of the logic ... even if it was not, perhaps, the original motivation for using the word (e.g "linear bicategories", "linear functors" etc.).
While the positive connotation of "linear" is "very straight," the negative connotation is "quadratics and higher not allowed." It's hard to know on whom to blame cartesian closed categories. Cantor maybe? The genius who invented x squared (several millennia earlier)? The diagonal functor is a sine qua non here. The central and unchanging point with "linear" is that you aren't allowed to use the same variable twice in the one expression. Whether you view doing so as the moral equivalent of drawing the last shilling out of your bank account twice, or attempting to apply the diagonal functor when the system protests that it's undefined, it all comes down to the same thing. To duplicate or not to duplicate, that is the only question. (Which may or may not subsume "To be or not to be" depending on whether you prefer to treat zeroary duplication separately.) Vaughan Pratt [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (2)
-
Robin Cockett -
Vaughan Pratt