[Haskell-cafe] linear logic

[George Kulakowski]

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 <dan.doel at gmail.com> 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
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110222/5614533a/attachment.htm>