I think http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf might be useful. And John Baez and Matt Stay's math.ucr.edu/home/baez/rosetta.pdf (where I found the citation for the first paper) has a fair amount about this sort of question.
On Tue, Feb 22, 2011 at 7:55 PM, Dan Doel <[email protected]> wrote: > 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 > > _______________________________________________ > Haskell-Cafe mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
