Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeFeb 4th 2014
    • (edited Feb 4th 2014)

    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.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 10th 2017

    I de-stubbified !-modality with some discussion of the various ways to interpret it categorically.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeDec 22nd 2017

    I added to !-modality some comments about term calculi.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeApr 17th 2018

    Added Hyland-Schalk reference

    diff, v18, current

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 7th 2019

    It seems that !-modality doesn’t render as a link on some pages, e.g., at Fock space. Is there a problem starting with ’!’ ?

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJul 7th 2019

    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.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 7th 2019

    OK, have changed a number of links.

    • CommentRowNumber8.
    • CommentAuthorRichard Williamson
    • CommentTimeJul 7th 2019
    • (edited Jul 7th 2019)

    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?

  1. Other Kleisli article

    Ammar Husain

    diff, v20, current

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 12th 2019

    Added an example: the Chu construction of any cartesian monoidal category has an idempotent !-modality, namely the coreflection into the original category.

    diff, v22, current

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2019

    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?

    • CommentRowNumber12.
    • CommentAuthormaxsnew
    • CommentTimeNov 13th 2019
    • (edited Nov 13th 2019)

    This paper does something like that, though for the closely related “tensor logic” rather than linear I think.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2019

    Thanks. I don’t think that’s the paper I was half-remembering, but it’s useful to have.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2019

    Added the missing nullary condition for a Seely !-modality.

    diff, v24, current

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeNov 13th 2019

    Generalized the example to lift any linear-nonlinear adjunction to a Chu construction.

    diff, v25, current

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeNov 20th 2019

    Added some citations for construction of cofree !-modalities

    diff, v26, current

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeNov 21st 2019

    Clarified relationship between the various definitions.

    diff, v27, current

  2. adding category:logic

    Valeria de Paiva

    diff, v28, current

    • CommentRowNumber19.
    • CommentAuthorvaleriadepaiva
    • CommentTimeNov 7th 2020
    @Mike I think the paper you wanted to remember is Jacobs' https://www.sciencedirect.com/science/article/pii/0168007294900205
    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    Added these pointers:

    A quantum programming language based on this linear/non-linear type theory adunction is QWIRE:

    • Jennifer Paykin, Robert Rand, Steve Zdancewic, QWIRE: a core language for quantum circuits, POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesJanuary 2017 Pages 846–858 (doi:10.1145/3009837.3009894)

    applied to verified programming after implementation in Coq:

    • Robert Rand, Jennifer Paykin, Steve Zdancewic, QWIRE Practice: Formal Verification of Quantum Circuits in Coq, EPTCS 266, 2018, pp. 119-132 (arXiv:1803.00699)

    and using ambient homotopy type theory:

    • Jennifer Paykin, Steve Zdancewic, A HoTT Quantum Equational Theory (arXiv:1904.04371)

    diff, v29, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2021

    also pointer to:

    diff, v30, current

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2022
    • (edited Nov 8th 2022)

    added cross-links by !include-ing the logic symbols – table

    added pointer to:

    • Daniel Mihályi, Valerie Novitzká, Section 2.2 of: What about Linear Logic in Computer Science?, Acta Polytechnica Hungarica 10 4 (2013) 147-160 [pdf]

    diff, v33, current

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022
    • (edited Nov 10th 2022)

    I have fixed and completed this bibitem:

    • Nick Benton, A mixed linear and non-linear logic: Proofs, terms and models, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 [doi:10.1007/BFb0022251, pdf]

    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.)

    diff, v34, current

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022

    also polished up this bibitem:

    diff, v34, current

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022

    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.

    diff, v34, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeNov 11th 2022

    added a section (here) on the realization of the exponential modality in linear homotopy type theory.

    diff, v35, current

    • CommentRowNumber27.
    • CommentAuthorJ-B Vienney
    • CommentTimeNov 11th 2022

    Added dereliction rule

    diff, v36, current

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeAug 20th 2023
    • (edited Aug 20th 2023)

    added a couple of more original references

    [edit: got interrupted, will do more polishing tomorrow…]

    diff, v40, current

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeAug 21st 2023

    added pointer to

    (of which the published BBPH92 seems to be just an abridged version)

    diff, v41, current

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeAug 21st 2023
    • (edited Aug 21st 2023)

    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”.

    diff, v44, current

    • CommentRowNumber31.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 22nd 2023

    Had anyone explicitly looked to connect the !-modality of linear logic to the stabilization adjunction before me here, and then more directly at #62?

    • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeAug 22nd 2023

    It’s been acknowledged in footnote 13 p. 48 here.

    • CommentRowNumber33.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 22nd 2023
    • (edited Aug 22nd 2023)

    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.

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeAug 22nd 2023

    In a discussion of that very premise, no?

    • CommentRowNumber35.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 22nd 2023

    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.

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023

    added a brief remark (here) that pointed classical homotopy types (“spaces”) are comonadic over linear homotopy types (“spectra”), from

    • Jacobson R. Blomquist, John E. Harper, Thm. 1.8 in: Suspension spectra and higher stabilization [arXiv:1612.08623]

    (hat tip to MO:a/333720)

    This deserves being expanded, but I need to interrupt.

    diff, v52, current

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeAug 25th 2023

    this is also Thm. 3.11 in:

    diff, v53, current

    • CommentRowNumber38.
    • CommentAuthornonemenon
    • CommentTimeSep 4th 2023

    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.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2023

    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.

    • CommentRowNumber40.
    • CommentAuthornonemenon
    • CommentTimeSep 4th 2023

    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.

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeSep 4th 2023

    I liked your angle of combining the perspective of sets as affine 𝔽 1\mathbb{F}_1-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.

    • CommentRowNumber42.
    • CommentAuthornonemenon
    • CommentTimeSep 5th 2023
    • (edited Sep 5th 2023)

    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?)

    • CommentRowNumber43.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 5th 2023

    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.