Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: deprecated: Dialectica

Topic: Dialectica and Differential Linear Logic


view this post on Zulip Valeria de Paiva (May 11 2022 at 00:22):

@Abdullah Malik asked me today about "quantum logic, the propositions in linear logic, the categorical logic of symmetric monoidal categories. How far has this work been taken, and what connections to the Dialectica are there, if any?"

I replied that there has been lots of work on that. Peter Selinger is the expert I know on that, he's written lots about it,
e.g. https://www.mathstat.dal.ca/~selinger/papers/papers/qpl.pdf or "A survey of graphical languages for monoidal categories" and there's plenty more in https://www.mscs.dal.ca/~selinger/papers/.

More recently, work has moved to "Differential Linear Logic" instead of traditional Linear Logic

Dialectica categories are good models of Linear Logic, I don't know if they're models of differential linear logic too or not. But I expect they are. (it may be wishful thinking on my part, but Marie Kerjean and Pierre-Marie Pedrot also think they are and have a preprint called "∂ is for Dialectica", which I think is very cool, even if I don't understand most of it.

That dialectica categories are (or not) good models of Differential Linear Logic is not obvious to prove, as people do not seem to have a very consensual idea of what are "good" models of Differential Linear Logic. But it's certainly a very interesting project.

I am repeating this information here, because I want everyone to decide on which kind of problem they want to work on for the MRC, and this is definitely another problem that I find very interesting indeed.

view this post on Zulip Abdullah Malik (May 11 2022 at 03:44):

Thanks, Valeria! This certainly sounds interesting! I'd be up for it, if anyone else is.

I guess a starting point would be here https://arxiv.org/pdf/1311.2290.pdf

Valeria de Paiva said:

Abdullah Malik asked me today about "quantum logic, the propositions in linear logic, the categorical logic of symmetric monoidal categories. How far has this work been taken, and what connections to the Dialectica are there, if any?"

I replied that there has been lots of work on that. Peter Selinger is the expert I know on that, he's written lots about it,
e.g. https://www.mathstat.dal.ca/~selinger/papers/papers/qpl.pdf or "A survey of graphical languages for monoidal categories" and
there's plenty more in https://www.mscs.dal.ca/~selinger/papers/.

More recently, work has moved to "Differential Linear Logic" instead of traditional Linear Logic

Dialectica categories are good models of Linear Logic, I don't know if they're models of differential linear logic too or not. But I expect they are.
(it may be wishful thinking on my part, but Marie Kerjean and Pierre-Marie Pedrot also think they are and have a preprint called "∂ is for Dialectica", which I think is very cool, even if I don't understand most of it.

That dialectica categories are (or not) good models of Differential Linear Logic is not obvious to prove, as people do not seem to have a very consensual idea of what are "good" models of Differential Linear Logic. But it's certainly a very interesting project.

I am repeating this information here, because all want everyone to decide on which kind of problem they want to work on, and this is definitely another problem that I find very interesting indeed.

view this post on Zulip Valeria de Paiva (May 11 2022 at 17:20):

Well, Pagani et al might be a place to start, but this does not seem clear to me. In particular, I do not see any traces of Dialectica categories in this paper and/or in the category CPM. Do you @Abdullah Malik ?