|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type/path type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|-||0-truncated higher colimit||quotient inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idempotent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
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 to be duplicated and discarded.
The original definition from Seely, adapted to the intuitionistic case and modernized, is:
Let be an symmetric monoidal category with cartesian products. A Seely comonad on is a comonad that is a strong monoidal functor from the cartesian monoidal structure to the symmetric monoidal structure, i.e. we have and coherently. (There is also an additional coherence axiom that should be imposed; see Mellies, section 7.3.)
(Note that in linear logic, the cartesian monoidal structure is sometimes denoted by .) This implies that the Kleisli category of ! (i.e.\ the category of cofree !-coalgebras) is cartesian monoidal. If is closed symmetric monoidal then the Kleisli category of 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. A different definition that doesn’t require the existence of was given by Benton, Bierman, de Paiva, and Hyland:
Let be a symmetric monoidal category; a linear exponential comonad on is a lax monoidal comonad such that every cofree !-coalgebra naturally carries the structure of a comonoid object in the category of coalgebras (i.e. the cofree-coalgebra functor lifts to the category of comonoids in the category of coalgebras).
It follows automatically that all !-coalgebras are comonoids, and therefore that the category of all !-coalgebras (not just the cofree ones) is cartesian monoidal. 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 linear-nonlinear adjunction is a monoidal adjunction in which is symmetric monoidal and is cartesian monoidal. The induced !-modality is the comonad on .
This includes both of the previous definitions where is taken respectively to be the Kleisli category or the Eilenberg-Moore category of !. Conversely, in any linear-nonlinear adjunction the induced comonad can be shown to be a linear exponential comonad. Moreover, if is a linear exponential comonad on a symmetric monoidal category with finite products, then the cofree !-coalgebra functor is a right adjoint and hence preserves cartesian products; but the cartesian products of coalgebras are the tensor product in , so we have , the Seely condition.
For “classical” linear logic, we want to be not just (closed) symmetric monoidal but -autonomous. If an -autonomous category has a linear exponential comonad one can derive a ? from the ! by de Morgan duality, . The resulting relationship between ! and ? was axiomatized in a way not requiring the de Morgan duality by Blute, Cockett, and Seely:
Let be a linearly distributive category with tensor product and cotensor product . A (!,?)-modality on consists of:
Here a functor is strong with respect to a lax monoidal functor if there is a natural transformation satisfying some natural axioms, and we similarly require compatibility of the monad and comonad structure transformations. BCS showed that if is in fact -autonomous, it follows from the above definition that as expected.
Suppose is a linear-nonlinear adjunction, where is closed symmetric monoidal with finite limits and colimits, and is an object. Then there is an induced linear-nonlinear adjunction where is the Chu construction , which is -autonomous with finite limits and colimits. Hence admits a !-modality.
The embedding of in as is coreflective: the coreflection of is . Moreover, this subcategory is closed under the tensor product of , i.e. the embedding is strong monoidal, hence the adjunction is a monoidal adjunction. Therefore, the composite adjunction is again a linear-nonlinear-adjunction.
Since a Chu construction is -autonomous, this !-modality implies a dual ?-modality.
If is a cartesian closed category with finite limits and colimits and is an object, then there is a linear-nonlinear adjunction , and hence admits a !-modality.
Apply the previous theorem to the identity adjunction .
Note that the !-modality obtained from the corollary is idempotent, while that obtained from the theorem is idempotent if and only if the original one was. Other ways of constructing !-modalities, such as by cofree coalgebras, may produce examples that are not idempotent.
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:
Construction of such comonads based on cofree comonoids can be found in (among other places):
Mellies and Tabareau and Tasson, An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, 28(7), 1253-1286. doi:10.1017/S0960129516000426
Sergey Slavnov, On Banach spaces of sequences and free linear logic exponential modality, Math. Struct. Comp. Sci. 29 (2019) 215-242, arxiv
The relation to Fock space is discussed in:
(in the context of finite quantum mechanics in terms of dagger-compact categories)
The interpretation of as an exponential in the context of Goodwillie calculus is due to
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
and using ambient homotopy type theory: