linear logic

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

linear logic

Vasili I. Galchin
Hello,

       What is the category that is used to interpret linear logic in
a categorical logic sense?

Thank you,


Vasili

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: linear logic

Doralicio
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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: linear logic

Luke Palmer-2
On Tue, Feb 22, 2011 at 4:23 PM, Nick Rudnick <[hidden email]> 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
>> [hidden email]
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: linear logic

Dan Doel
In reply to this post by Vasili I. Galchin
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe