natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
logic | category theory | type theory |
---|---|---|
true | terminal object/(-2)-truncated object | h-level 0-type/unit type |
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language
</table>
In full linear logic/linear type theory there is assumed a (comonadic) modality denoted “!” and called the exponential modality, whose role is, roughly, to give linear types also a non-linear interpretation. This is also called the “of course”-modality or the storage modality, and sometimes the “bang”-operation.
In classical linear logic (meaning with involutive de Morgan duality), the de Morgan dual of “!” is denoted “?” and called the “why not”-modality.
In categorical semantics of linear type theory the !-modality typically appears as a kind of Fock space construction. If one views linear logic as quantum logic (as discussed there), then this means that the !-modality produces free second quantization.
Everyone agrees that ! should be a comonad (and ? should be a monad), but there are different ways to proceed from there. The goal is to capture the syntactic rules allowing assumptions of the form $!A$ to be duplicated and discarded. The original definition from Seely was:
Let $C$ be an $\ast$-autonomous category with cartesian products. A Seely !-modality on $C$ is a comonad that is a strong monoidal functor from the cartesian monoidal structure to the $\ast$-autonomous monoidal structure, i.e. we have $!(A\times B)\cong !A \otimes !B$ coherently. (There is also a coherence axiom that should be imposed; see Mellies, section 7.3.)
(Note that in linear logic, the cartesian monoidal structure $\times$ is sometimes denoted by $\&$.) This implies that the Kleisli category of ! is a cartesian closed category, which is a categorical version of the translation of intuitionistic logic into linear logic.
Of course, the above definition depends on the existence of the cartesian product, and relies on the self-duality of an $\ast$-autonomous category to derive the rules for ? from the rules for !. A different definition that doesn’t require the existence of $\times$ was given by Benton, Bierman, de Paiva, and Hyland:
Let $C$ be a closed symmetric monoidal category; a !-modality on $C$ is a lax monoidal comonad such that every !-coalgebra naturally carries the structure of a comonoid object in the category of coalgebras, such that coalgebra maps are comonoid maps.
This definition implies that the category of all !-coalgebras (not just the free ones, i.e. its Kleisli category) is cartesian closed. Note that for a comonad on a poset, every coalgebra is free; thus the world of pure propositional “logic” doesn’t tell us whether to consider the Kleisli category or the Eilenberg-Moore category for the translation. A more even-handed approach is the following (see Mellies):
A linear-nonlinear adjunction is a monoidal adjunction $F : M \rightleftarrows L : G$ in which $L$ is symmetric monoidal and $M$ is cartesian monoidal. The induced !-modality is the comonad $F G$ on $L$.
This includes both of the previous definitions where $M$ is taken respectively to be the Kleisli category or the Eilenberg-Moore category of !.
On the other hand, the last two definitions are given only for “intuitionistic” linear logic, though in the $\ast$-autonomous case one could derive a ? from the ! by de Morgan duality. A definition not requiring the de Morgan duality and describing ! and ? together was given by Blute, Cockett, and Seely:
Let $C$ be a linearly distributive category with tensor product $\otimes$ and cotensor product $\parr$. A (!,?)-modality on $C$ consists of:
Here a functor $F$ is strong with respect to a lax monoidal functor $G$ if there is a natural transformation $F A \otimes G B \to F(A\otimes G B)$ satisfying some natural axioms, and we similarly require compatibility of the monad and comonad structure transformations.
Girard’s original presentation of linear logic involved rules that explicitly assumed the presence of $!$ on hypotheses or on entire contexts, such as weakening and contraction:
and “promotion”:
If this is translated into a natural deduction style term calculus, the resulting rules are more complicated than those of most type formers. This can be avoided using adjoint type theory with two context zones, one “nonlinear” one where contraction and weakening are permitted (and admissible) and one “linear” one where they are not, with $!$ as a modality relating the two zones.
Such a “modal” presentation of linear logic was first introduced by Girard in his work on LU? and then developed by a number of other people such as Plotkin, Wadler, Benton, and Barber. See the references for details.
This presentation also generalizes naturally to dependent linear type theory, with the nonlinear type theory being dependent, and the linear types depending on the nonlinear ones but nothing depending on linear types. In this context, the $!$-modality decomposes into “context extension” and a “dependent sum”.
The semantics of ! as a comonad is discussed in:
R. A. G. Seely, Linear logic, $\ast$-autonomous categories and cofree coalgebras, Contemporary Mathematics 92, 1989. (pdf, ps.gz)
Nick Benton, Gavin Bierman, Valeria de Paiva, Martin Hyland, Linear lambda-Calculus and Categorical Models Revisited (1992), citeseer
R. F. Blute , J. R. B. Cockett and R. A. G. Seely. ! and ? – Storage as tensorial strength doi, pdf
Paul-André Melliès, Categorical semantics of linear logic, 2009. pdf
Martin Hyland and Andreas Schalk?, Glueing and orthogonality for models of linear logic, pdf
The relation to Fock space is discussed in:
Richard Blute, Prakash Panangaden, R. A. G. Seely, Fock Space: A Model of Linear Exponential Types (1994) (web, pdf)
Marcelo Fiore, Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic, Lecture Notes in Computer Science Volume 4583, 2007, pp 163-177 (pdf)
Jamie Vicary, A categorical framework for the quantum harmonic oscillator, International Journal of Theoretical Physics December 2008, Volume 47, Issue 12, pp 3408-3447 (arXiv:0706.0711)
(in the context of finite quantum mechanics in terms of dagger-compact categories)
The interpretation of $\Omega^\infty \Sigma^\infty_+$ as an exponential in the context of Goodwillie calculus is due to
based on
The modal approach to a term calculus for the $!$-modality can be found in:
Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201-217, 1993.
G. Plotkin. Type theory and recursion. In Proceedings of the Eigth Symposium of Logic in Computer Science, Montreal , page 374. IEEE Computer Society Press, 1993.
N. Benton. A mixed linear and non-linear logic; proofs, terms and models. In Proceedings of Computer Science Logic ‘94, number 933 in LNCS. Verlag, June 1995.
Philip Wadler. A syntax for linear logic. In Ninth International Coference on the Mathematical Foundations of Programming Semantics , volume 802 of LNCS . Springer Verlag, April 1993
Andrew Barber, Dual Intuitionistic Linear Logic, Technical Report ECS-LFCS-96-347, University of Edinburgh, Edinburgh (1996), web
Last revised on April 17, 2018 at 19:14:57. See the history of this page for a list of all contributions to it.