11
$\begingroup$

Recently, I read on the nLab that the category of Banach spaces and linear contractions 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 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?

Improve this question
$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$
    – Damiano Mazza
    Sep 20, 2018 at 11:21
  • 1
    $\begingroup$ Ah, ok, I see what's going on, it's explained further down the article and then at the 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... $\endgroup$
    – Damiano Mazza
    Sep 20, 2018 at 12:41
  • $\begingroup$ 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?" $\endgroup$
    – Neel Krishnaswami
    Sep 20, 2018 at 21:16
  • $\begingroup$ 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. $\endgroup$
    – Damiano Mazza
    Sep 26, 2018 at 6:47
  • $\begingroup$ I'm looking forward to this! $\endgroup$
    – Neel Krishnaswami
    Sep 28, 2018 at 12:17

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.