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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

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

nLab > Latest Changes: graded modality

Bottom of Page

1 to 21 of 21

  1.  
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 20th 2018

    At our workshop yesterday we heard Dominic Orchard speak about “Graded Modal Logic for Linear Dependent Type Theory”/ So I’ve started graded modality.

    Now any connection to Licata-Shulman-Riley?

    v1, current

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 20th 2018

    It would seem so, seeing that LSR speaks about subexponentials in 3.10.

    How about the ♯ n\sharp_n of section 5.2.2 of dcct, or the ℑ n\Im_n mentioned e.g. here? Are these not modalities indexed by the natural numbers with monoid operation given by min? Similarly for truncation modalities.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeJun 20th 2018

    added hyperlink to modality, added hyperlink for bounded linear logic, added plural redirect

    diff, v3, current

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeJun 20th 2018

    I haven’t looked at any of the references, but almost without exception anything like this has a representation using a particular mode theory in LSR; here there would presumably be an infinite family of mode morphisms with 2-cells between them representing the rule structure.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 26th 2018

    Added a couple of references.

    diff, v4, current

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 18th 2018

    Added some earlier philosophical references.

    diff, v6, current

  7. Added a new reference to Fuji et al.’s paper on graded monads.

    Harley Eades III

    diff, v7, current

  8. A few more references, and added links to PDFs.

    Harley Eades III

    diff, v7, current

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 25th 2021

    Added some references

    diff, v15, current

    • CommentRowNumber10.
    • CommentAuthorJ-B Vienney
    • CommentTimeAug 5th 2022
    • (edited Aug 5th 2022)

    Added the reference

    • Flavien Breuvart, Michele Pagani, Modelling Coeffects in the Relational Semantics of Linear Logic, (pdf)

    diff, v16, current

    • CommentRowNumber11.
    • CommentAuthorJ-B Vienney
    • CommentTimeAug 25th 2022
    • (edited Aug 25th 2022)

    Recent variations of linear logic using graded modalities could be named by the expression “graded linear logic”. Bounded linear logic is something quite specific.

    Added a link to a new page graded linear logic.

    Added a link to a new page graded differential linear logic.

    Added a link to a new page homological linear logic.

    I will create these pages later.

    diff, v17, current

    • CommentRowNumber12.
    • CommentAuthorJ-B Vienney
    • CommentTimeAug 25th 2022
    • (edited Aug 25th 2022)

    Added that the homological linear logic would be linked with Koszul complexes.

    diff, v17, current

    • CommentRowNumber13.
    • CommentAuthorJ-B Vienney
    • CommentTimeAug 25th 2022
    • (edited Aug 25th 2022)

    Added also a link to symmetric linear logic which is meant to be a logic of symmetric powers or equivalently a logic of homogeneous polynomials and would be able to differentiate them by respecting the Euler identity.

    I will create this page later.

    diff, v17, current

    • CommentRowNumber14.
    • CommentAuthorJ-B Vienney
    • CommentTimeMar 21st 2023

    Added our preprint Graded Differential Categories and Graded Differential Linear Logic with JS Lemay in the references

    diff, v20, current

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 21st 2023

    Re #14, one of these days, someone’s going to need to work out whether and how this differential linear logic approach relates to the linear differential cohesive approach. I tried to get a conversation going on this over here and Tim Campion provided some useful comparison.

    • CommentRowNumber16.
    • CommentAuthorJ-B Vienney
    • CommentTimeMar 21st 2023
    • (edited Mar 21st 2023)

    The linear differential cohesive approach is far above my head. But if you have some linear HoTT framework (or something else) where there is an exponential modality, then we can maybe try to make this a differential exponential modality which will give a differential linear HoTT (resp. a differential something else).

    • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 21st 2023

    The exponential modality is discussed here.

    • CommentRowNumber18.
    • CommentAuthorJ-B Vienney
    • CommentTimeMar 21st 2023
    • (edited Mar 21st 2023)

    Is Σ + ∞∘Ω ∞\Sigma_{+}^\infty \circ \Omega^\infty a monad or a comonad? Models of linear logic are traditionally with a comonad but in math, you more often have a monad (but then you can still obtain a model of “co”linear logic by reversing all the morphisms in the definition).

    If you want differentiation, you need mainly your Σ + ∞(Ω ∞(A))\Sigma_{+}^\infty(\Omega^\infty(A)) to be bialgebras.

    • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 22nd 2023

    Right adjoint first, so a comonad. I was managing to mix myself up over here, where I was speculating on there being a relevant graded version of the exponential.

  20. Hi! I was wondering if all the work that has been done in the past regarding sub-exponentials in Linear Logic, where modalities are organised using semirings, ordered lattices and etc for capturing epistemic, spacial, temporal behaviours as well as preferences would fit in this discussion?
    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTime4 days ago
    • (edited 4 days ago)

    Hard to reply to such questions.

    Best to just go ahead and add whatever material you feel like adding.

    Once we see it, if we feel it would better fit into another entry, it’s easy to move it.

1 to 21 of 21

  1.