<p>Recently, I read on the nLab that <a href="https://ncatlab.org/nlab/show/Banach+space" rel="noreferrer">the category of Banach spaces and linear contractions</a> is small complete, small cocomplete, and monoidal closed. </p>

<p>This means that Banach spaces and short linear maps form a model of intuitionistic multiplicative-additive linear logic, and the fact that it is small (co)complete seems to suggest that the construction of Melliès, Tabareau
and Tasson in <a href="https://hal.archives-ouvertes.fr/hal-00391714/document" rel="noreferrer"><em>An explicit formula for the free exponential
modality of linear logic</em></a> would go through in this category, supplying an interpretation of the exponential as well. </p>

<p>I found this quite surprising, since interpreting linear logic in infinite-dimensional vector spaces seems to have prompted an awful lot of work over the last two decades. </p>

<ol>
<li><p>Does this model for ILL with an exponential actually work? I haven't seen it before in the literature, so maybe it fails for some obvious reason that I am overlooking...</p></li>
<li><p>If so, what is the motivation for placing so much emphasis on finding  models of specifically <em>classical</em> linear logic in (some restriction of) infinite-dimensional vector spaces? </p></li>
</ol>

CC BY-SA 4.0
2018-09-20T11:21:54.660Z
Hi Neel!  Are you sure that the category in question is monoidal closed?  The nLab page is quite confusing because it talks about closure of the category $\mathbf{Ban}$ after the definition of bounded operator, but then it defines $\mathbf{Ban}$ as the category whose morphisms are linear contractions.  The latter category does not seem closed to me: the set of linear contractions on a space is not even a vector space (the identity $\mathsf I$ is a linear contraction, $\mathsf I+\mathsf I$ is not).  Am I missing something?
Damiano Mazza
CC BY-SA 4.0
2018-09-20T12:41:48.983Z
Ah, ok, I see what's going on, it's explained further down the article and then at the [internal hom](https://ncatlab.org/nlab/show/internal+hom) page.  My first reaction then would be that Melliès, Tabareau and Tasson's construction won't work because the underlying limit does not commute with the tensor.  But I don't know, I'm just saying this because, like you say, finding a TVS model of linear logic is not easy, in particular because the Kleisli category will give you a "convenient" category of vector spaces (e.g. cartesian closed), which is rare and would have not gone unnoticed...
Damiano Mazza
CC BY-SA 4.0
2018-09-20T21:16:52.047Z
Oh yeah, I forgot that you have to check the limit commutes with the tensor. That gives a natural next thing to check. I had a vague assumption that the big problem with TVS models was that the double-dual didn't work the way you want, and this webpage made me wonder "why not look at ILL?"
Neel Krishnaswami
CC BY-SA 4.0
2018-09-26T06:47:06.683Z
Quick update: I've been discussing this with people much more knowledgeable than me on the topic, so far it seems that there is no obstruction to $\mathbf{Ban}$ being a model of ILL.  In particular, the fact that the tensor commutes with the projective limit required in MTT's construction seems to be a well-known fact (c.f. Theorem 15.4.2 in Hans Jarchow's book *Locally Convex Spaces*).  So it may actually be a model after all!  As soon as I'll have collected more precise and definitive evidence (if not a proof), I'll write an answer.
Damiano Mazza
CC BY-SA 4.0
2018-09-28T12:17:25.433Z
I'm looking forward to this!
Neel Krishnaswami
<lo.logic><linear-algebra><ct.category-theory><topology><linear-logic>
Do Banach spaces and linear contraction maps form a model of ILL with an exponential?
Neel Krishnaswami
# Do Banach spaces and linear contraction maps form a model of ILL with an exponential?

(Asked by: username_0 on 2018-09-19)

Recently, I read on the nLab that [the category of Banach spaces and linear contractions](https://ncatlab.org/nlab/show/Banach+space) is small complete, small cocomplete, and monoidal closed.

This means that Banach spaces and short linear maps form a model of intuitionistic multiplicative-additive linear logic, and the fact that it is small (co)complete seems to suggest that the construction of Melliès, Tabareau
and Tasson in [*An explicit formula for the free exponential
modality of linear logic*](https://hal.archives-ouvertes.fr/hal-00391714/document) would go through in this category, supplying an interpretation of the exponential as well.

I found this quite surprising, since interpreting linear logic in infinite-dimensional vector spaces seems to have prompted an awful lot of work over the last two decades.

1. Does this model for ILL with an exponential actually work? I haven't seen it before in the literature, so maybe it fails for some obvious reason that I am overlooking...
2. If so, what is the motivation for placing so much emphasis on finding models of specifically *classical* linear logic in (some restriction of) infinite-dimensional vector spaces?

**Tags:** lo.logic, linear-algebra, ct.category-theory, topology, linear-logic

> **Comments:**
> **username_1**: Hi Neel!  Are you sure that the category in question is monoidal closed?  The nLab page is quite confusing because it talks about closure of the category $\mathbf{Ban}$ after the definition of bounded operator, but then it defines $\mathbf{Ban}$ as the category whose morphisms are linear contractions.  The latter category does not seem closed to me: the set of linear contractions on a space is not even a vector space (the identity $\mathsf I$ is a linear contraction, $\mathsf I+\mathsf I$ is not).  Am I missing something?  
> **username_1**: Ah, ok, I see what's going on, it's explained further down the article and then at the [internal hom](https://ncatlab.org/nlab/show/internal+hom) page.  My first reaction then would be that Melliès, Tabareau and Tasson's construction won't work because the underlying limit does not commute with the tensor.  But I don't know, I'm just saying this because, like you say, finding a TVS model of linear logic is not easy, in particular because the Kleisli category will give you a "convenient" category of vector spaces (e.g. cartesian closed), which is rare and would have not gone unnoticed...  
> **username_0**: Oh yeah, I forgot that you have to check the limit commutes with the tensor. That gives a natural next thing to check. I had a vague assumption that the big problem with TVS models was that the double-dual didn't work the way you want, and this webpage made me wonder "why not look at ILL?"  
> **username_1**: Quick update: I've been discussing this with people much more knowledgeable than me on the topic, so far it seems that there is no obstruction to $\mathbf{Ban}$ being a model of ILL.  In particular, the fact that the tensor commutes with the projective limit required in MTT's construction seems to be a well-known fact (c.f. Theorem 15.4.2 in Hans Jarchow's book *Locally Convex Spaces*).  So it may actually be a model after all!  As soon as I'll have collected more precise and definitive evidence (if not a proof), I'll write an answer.  
> **username_0**: I'm looking forward to this!  

---

## 0 answers

