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.
]]>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?)
]]>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.
]]>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.
]]>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.
]]>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.
]]>this is also Thm. 3.11 in:
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.
]]>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.
]]>In a discussion of that very premise, no?
]]>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.
]]>It’s been acknowledged in footnote 13 p. 48 here.
]]>Had anyone explicitly looked to connect the !-modality of linear logic to the stabilization adjunction before me here, and then more directly at #62?
]]>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”.
]]>added pointer to
(of which the published BBPH92 seems to be just an abridged version)
]]>added a couple of more original references
[edit: got interrupted, will do more polishing tomorrow…]
]]>Added dereliction rule
]]>added a section (here) on the realization of the exponential modality in linear homotopy type theory.
]]>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.
]]>also polished up this bibitem:
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.)
]]>added cross-links by !include
-ing the logic symbols – table
added pointer to:
also pointer to:
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: