Re: [Haskell-cafe] linear logic
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 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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] linear logic
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] linear logic
On Tue, Feb 22, 2011 at 4:23 PM, Nick Rudnick wrote: > Hi Vasili, > > not understanding clearly «in a categorical logic sense» -- but I can be > sure you already checked out coherent spaces, which might be regarded as > underlying Girard's original works in this sense?? I have a faint idea about > improvements, but I don't have them present at the moment. > > Curiously -- is it allowed to ask about the motivation? Insofar as "I'm curious" is allowed as a legitimate response, yes. Luke > Cheers, Nick > > On 02/22/2011 09:13 PM, Vasili I. Galchin wrote: >> >> Hello, >> >> What is the category that is used to interpret linear logic in >> a categorical logic sense? >> >> Thank you, >> >> >> Vasili >> >> ___ >> Haskell-Cafe mailing list >> Haskell-Cafe@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> > > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] linear logic
Hi Vasili, not understanding clearly «in a categorical logic sense» -- but I can be sure you already checked out coherent spaces, which might be regarded as underlying Girard's original works in this sense?? I have a faint idea about improvements, but I don't have them present at the moment. Curiously -- is it allowed to ask about the motivation? Cheers, Nick On 02/22/2011 09:13 PM, Vasili I. Galchin wrote: Hello, What is the category that is used to interpret linear logic in a categorical logic sense? Thank you, Vasili ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] linear logic
Hello, What is the category that is used to interpret linear logic in a categorical logic sense? Thank you, Vasili ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
