Classic modalities are defined in absolute terms, so that, for instance, necessity and possibility are understood in terms of a state of affairs obtaining in all or some world. Some philosophers in the early 1970s looked to generalize these to graded versions so that a proposition may be said to be, say, quite likely, highly likely, and so on. Since then, linguists and computer scientists have developed these ideas, the latter expanding the topic to include those modalities relating to resources and side effects.
A graded modality is an indexed family of modalities with some additional structure on the indices which mirrors the structure of the axioms/proof rules. A graded modality is a graded monad with idempotent components.
For example, the exponential modality of linear logic has a graded counterpart in bounded linear logic, where is replaced with a family of modalities indexed by the natural numbers (the reuse bound).
More recent variations of linear logic which use graded modalities, where is replaced with a family of modalities indexed by a semi-ring could be designated by the name graded linear logic?.
Differential linear logic and graded linear logic? seem to be mixable under the form of a graded differential linear logic?. Such a logic would be a refinement of differential linear logic able to deal with differentiable functions which have a grade such as the degree of a polynomial or the number of times the function is differentiable. A more specific system would be a symmetric linear logic? which deal specifically with symmetric powers and thus homogeneous polynomials. It seems possible to adapt the idea to an anticommutative? setting giving an homological linear logic?. Such a logic would be probably able to give a syntax for at least Koszul complexes.
Brunel, Aloïs and Gaboardi, Marco and Mazza, Damiano and Zdancewic, Steve, A Core Quantitative Coeffect Calculus, (doi) (pdf)
Dan R. Ghica and Alex I. Smith, Bounded Linear Types in a Resource Semiring, (doi) (pdf)
Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III, Quantitative Program Reasoning with Graded Modal Types, (pdf)
Dominic Orchard, Vilem-Benjamin Liepelt, Gram: A linear functional language with graded modal types, (extended abstract)
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu, Combining effects and coeffects via grading, ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (2016) 476–489 [doi:10.1145/2951913.2951939, talk abstract, video rec]
Flavien Breuvart, Michele Pagani, Modelling Coeffects in the Relational Semantics of Linear Logic, (pdf)
Shin-ya Katsumata, A Double Category Theoretic Analysis of Graded Linear Exponential Comonads, (doi)
Soichiro Fujii, Shin-ya Katsumata, Paul-André Melliès, Towards a Formal Theory of Graded Monads, (doi) (pdf)
Jean-Baptiste Vienney, Jean-Simon Pacaud Lemay, Graded Differential Categories and Graded Differential Linear Logic, 2023, arXiv
A formal framework for type theories with a collection of modalities is in
On dependent linear types and graded modalities:
For discussion in philosophy and linguistics, see
Patrick Grosz, Grading Modality: A New Approach to Modal Concord and its Relatives, (paper)
Daniel Lassiter, Graded modality, (paper)
Daniel Lassiter, Graded Modality: Qualitative and Quantitative Perspectives, OUP, (website)
Earlier work in philosophy includes
Lou Goble, 1970. Grades Of Modality. Logique Et Analyse 13, pp. 323-334, (paper).
David Kaplan, S5 with multiple possibility, The Journal of Symbolic Logic, 35:355–356, 1970.
Kit Fine, 1972. In so many possible worlds. Notre Dame Journal of Formal Logics 13: 516–520.
David Lewis, 1973. Counterfactuals. Oxford: Blackwell
M. Fattorosi-Barnaba and F. de Caro. Graded modalities I. Studia Logica, 44:197–221,1985
Last revised on October 8, 2023 at 15:25:35. See the history of this page for a list of all contributions to it.