Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
collected some references on the interpretation of the !-modality as the Fock space construction at !-modality.
Cross-linked briefly with he stub entries_Fock space_ and second quantization.
I de-stubbified !-modality with some discussion of the various ways to interpret it categorically.
I added to !-modality some comments about term calculi.
It seems that !-modality doesn’t render as a link on some pages, e.g., at Fock space. Is there a problem starting with ’!’ ?
Thanks for the alert. I am fixing it in the entries. “exponential modality” is a better link word, anyway.
But of course there remains a bug which would be good to fix in any case. So I have moved the non-rendering “!-modality”-link to the Sandbox.
OK, have changed a number of links.
I’m currently on holiday, and unfortunately will not be able to look at the bug for at least a week. Would it be possible to create a single thread ’Bugs and feature requests’ where all bugs and feature requests are registered (and maybe a note could be added to the HowTo to this effect)? It is then much less likely that I will forget about or overlook something. To keep it easy to get an overview, maybe discussion can be avoided in that thread, and instead when registering the bug one can link to a thread where one can discuss it?
I have a vague memory of reading a paper that decomposed the !-modality into two separate modalities, one that allows only contraction and another that allows only weakening. Does anyone know a reference doing something like that?
This paper does something like that, though for the closely related “tensor logic” rather than linear I think.
Thanks. I don’t think that’s the paper I was half-remembering, but it’s useful to have.
Added these pointers:
A quantum programming language based on this linear/non-linear type theory adunction is QWIRE:
applied to verified programming after implementation in Coq:
and using ambient homotopy type theory:
also pointer to:
added cross-links by !include-ing the logic symbols – table
added pointer to:
I have fixed and completed this bibitem:
here and in a couple of other entries.
(It also appears at linear-non-linear logic and still needs to be reformatted there, but that entry is suffering from some bug which prevents it from being edited. I have contacted the technical team about it.)
also polished up this bibitem:
I have recovered this reference here via the WaybackMachine:
Unfortunately, the pdf is just a tad larger than the upload limit for the nLab server. I have tried to compress it a little, but couldn’t quite bring it below the threshold.
So for the time being the pdf is sitting in my Dropbox.
added pointer to
(of which the published BBPH92 seems to be just an abridged version)
Am trying to bring parts of this entry into better shape.
Have adjusted the wording in the Idea section (here) for streamlining
and expanded by quickly indicating, right in the Idea-section, what I think is the most fundamental elementary example (sending a vector space to the linear span of its underlying set) – this in to give up-front more of an idea of what the exponential modality is about.
In particular I highlighted in the idea-section and also further below in a numbered remark (here) what is exponential about the “exponential modality”.
Had anyone explicitly looked to connect the !-modality of linear logic to the stabilization adjunction before me here, and then more directly at #62?
It’s been acknowledged in footnote 13 p. 48 here.
Well that’s referring to an existing observation from 1995 by Arone and Kankaanrinta relating a construction in homotopy theory to the exponential function. I meant the explicit thought to relate linear logic to homotopy theory.
I guess all I was doing was applying transitivity to the ’is like’ relation: linear logic is like linear algebra, linear algebra is like stable homotopy theory.
In a discussion of that very premise, no?
I doubt the reader would pick up the scope of the footnote as being the broader ongoing discussion rather than the specific point of the paragraph. But it wasn’t an issue of receiving due acknowledgement. I was simply interested if anyone before had directly said that there should be a linear logic-stable homotopy theory connection.
added a brief remark (here) that pointed classical homotopy types (“spaces”) are comonadic over linear homotopy types (“spectra”), from
(hat tip to MO:a/333720)
This deserves being expanded, but I need to interrupt.
this is also Thm. 3.11 in:
I am curious about the parallel drawn between Set and Vect in the Idea section. “Morally”, sets are affine spaces over the field on one element, with pointed sets as its vector spaces. How do affine logics tie into this? Conceptually, I think of a category of pointed types as the “type of terms” or “type of proofs” for a type theory, especially seen as a type indexed by Type and displayed by the identity functor on Type. Can anyone elaborate on how this conceptualization extends to linear and affine types? I haven’t studied much about affine type theories; I just know that they drop contraction, and I don’t understand its semantics in relation to the semantics of linear or dependent type theories.
On your first question I suppose there is the trivial answer by observing that classical (intuitionistic) logic is a form of affine logic: If we just forget that sets satisfy a contraction rule, then what remains is their affine logic.
While I don’t know if it is relevant for your concern, just to notice that exponential modalities in the context of affine logic are discussed in Shulman 22.
Thank you. I started digging into that paper shortly after my post here, so right now I am digesting the dual roles played by refutations and demonstrations.
I liked your angle of combining the perspective of sets as affine -modules with the idea of them being models of affine logic. There may be more to this, but I am just not sure if the exponential modality is the place to see this at work.
My gut says this has something to do with Goodwillie derivatives of monoidal structures. While I have not verified it yet, I have heard that the symmetric smash product of spectra may be defined as the (total?) Goodwillie derivative of the cartesian product bifunctor. If anyone has a reference that elaborates on this, I would be very appreciative. The exponential modality interacts harmoniously with the Goodwillie calculus, and I wonder about the broader potential for “Goodwillie smoothness” to help us understand the big picture. (I’m wondering if I should just start a conversation about all this in some other thread, in case it is slightly tangential (haha) here?)
The exponential modality interacts harmoniously with the Goodwillie calculus
That’s what I was sensing too. If you can make something out of the vague ideas mentioned here and below that, I’d love to hear.
1 to 43 of 43