<div dir="ltr"><div>I think <a href="http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf">http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf</a> might be useful. And John Baez and Matt Stay's <a href="http://math.ucr.edu/home/baez/rosetta.pdf">math.ucr.edu/home/baez/rosetta.pdf</a> (where I found the citation for the first paper) has a fair amount about this sort of question.</div>
<br><div class="gmail_quote">On Tue, Feb 22, 2011 at 7:55 PM, Dan Doel <span dir="ltr"><<a href="mailto:dan.doel@gmail.com">dan.doel@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">On Tuesday 22 February 2011 3:13:32 PM Vasili I. Galchin wrote:<br>
> What is the category that is used to interpret linear logic in<br>
> a categorical logic sense?<br>
<br>
</div>This is rather a guess on my part, but I'd wager that symmetric monoidal<br>
closed categories, or something close, would be to linear logic as Cartesian<br>
closed categories are to intuitionistic logic. There's a tensor M (x) N, and a<br>
unit (up to isomorphism) I of the tensor. And there's an adjunction:<br>
<br>
M (x) N |- O <=> M |- N -o O<br>
<br>
suggestively named, hopefully. There's no diagonal A |- A (x) A like there is<br>
for products, and I is not terminal, so no A |- I in general. Those two should<br>
probably take care of the no-contraction, no-weakening rules. Symmetric<br>
monoidal categories mean A (x) B ~= B (x) A, though, so you still get the<br>
exchange rule.<br>
<br>
Obviously a lot of connectives are missing above, but I don't know the<br>
categorical analogues off the top of my head. Searching for 'closed monoidal'<br>
or 'symmetric monoidal closed' along with linear logic may be fruitful,<br>
though.<br>
<font color="#888888"><br>
-- Dan<br>
</font><div><div></div><div class="h5"><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div>