[Haskell-cafe] linear logic

[Dan Doel]

On Tuesday 22 February 2011 3:13:32 PM Vasili I. Galchin wrote:
>        What is the category that is used to interpret linear logic in
> a categorical logic sense?

This is rather a guess on my part, but I'd wager that symmetric monoidal 
closed categories, or something close, would be to linear logic as Cartesian 
closed categories are to intuitionistic logic. There's a tensor M (x) N, and a 
unit (up to isomorphism) I of the tensor. And there's an adjunction:

  M (x) N |- O  <=> M |- N -o O

suggestively named, hopefully. There's no diagonal A |- A (x) A like there is 
for products, and I is not terminal, so no A |- I in general. Those two should 
probably take care of the no-contraction, no-weakening rules. Symmetric 
monoidal categories mean A (x) B ~= B (x) A, though, so you still get the 
exchange rule.

Obviously a lot of connectives are missing above, but I don't know the 
categorical analogues off the top of my head. Searching for 'closed monoidal' 
or 'symmetric monoidal closed' along with linear logic may be fruitful, 
though.

-- Dan