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/ ]