nLab
graded modality

Contents

Contents

Idea

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 ! n!_n indexed by the natural numbers (the reuse bound).

References

  • 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, (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)

A formal framework for type theories with a collection of modalities is in

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: 323-334.

  • Kit Fine, 1972. In so many possible worlds. Notre Dame Journal of Formal Logics 13: 516–520.

  • David Lewis, 1973. Counterfactuals. Oxford: Blackwell

Last revised on July 16, 2019 at 06:27:59. See the history of this page for a list of all contributions to it.