Contents

Examples

# Contents

## Idea

In full linear logic [Girard 1987] and more generally in linear type theory there is assumed a (comonadic) modality traditionally denoted “!” whose role is to model the “underlying” classical (intuitionistic) type of a given linear type.

This is alternatively called the “exponential modality” (for good reasons discussed below), or “storage modality” (as it allows to duplicate and hence “store” otherwise linear data) and sometimes pronounced “of course” (intended alongside “necessarily” and “possibly” as used in modal logic) or even “bang” (just in reference to the symbol “!”).

In classical linear logic (meaning with involutive de Morgan duality), the de Morgan dual of “!” is denoted “?” and then sometimes pronounced “why not”.

Today it is understood (cf. Melliès 2009, p. 36) that the exponential modality is best and generally to be thought as as, first of all a comonad on linear types (Seely 1989 §2, dePaiva 1989, Benton, Bierman, de Paiva and Hyland 1992) which, secondly, is induced by an adjunction to classical (meaning here: non-linear intuitionistic) types with special monoidal properties (Seely 1989 §2, Bierman 1994 pp. 157, Benton 1995).

In a most elementary and illuminating example (which may not have received the attention it deserves, cf. the history at quantum logic):

• classical intuitionistic types form (are interpreted in) the category of Sets

$ClaTypes \,\coloneqq\, Set$

• linear types form (are interpreted in) the category of vector spaces (cf. Murfet 2014)

$LinTypes \,\coloneqq\, Vect_{\mathbb{K}}$

and the adjoint functors in question are

• forming the linear span of a set

$\array{ Set &\overset{\mathrm{Q}}{\longrightarrow}& Vect \\ W &\mapsto& \oplus_W \mathbb{1} }$
• forming the underlying set of a vector space:

$\array{ Vect &\overset{\mathrm{C}}{\longrightarrow}& Set \\ \mathscr{V} &\mapsto& Hom(\mathbb{1}, \, \mathscr{V}) }$

in which case the exponential modality acts by sending a vector space to the linear span of its underlying set

$\array{ Vect &\overset{\;\; ! \;\;}{\longrightarrow}& Vect \\ \mathscr{V} &\mapsto& \underset{\mathscr{V}}{\bigoplus} \mathbb{1} \,. }$

One sees that this construction takes (direct) sums to (tensor) products

$!(\mathscr{V} \oplus \mathscr{V}') \;\simeq\; (! \mathscr{V}) \otimes (! \mathscr{V}')$

and zero (objects) to unit (objects)

$! 0 \;\simeq\; \mathbb{1}$

as expected of any exponential map, whence the name “exponential modality”.

This example is the 0-sector of the more famous stabilization ($\infty$-)adjunction $(\Sigma_+^\infty \dashv \Omega_+^\infty)$ between (the homotopy theory of) topological spaces and (the stable homotopy theory of) module spectra equipped with the symmetric smash product of spectra (given by forming suspension spectra $X \mapsto \Sigma_+^\infty X$), which points to a deeper origin of the “exponential modality”, see below and at linear homotopy type theory for more on this.

## Categorical semantics

Following Seely 1989, dePaiva 1989, Benton, Bierman, de Paiva and Hyland 1992 it is common convention that “!” should be a comonad on the type system (and ? should be a monad, see also at monads in computer science), but there is some room in which further axioms to impose. The goal is to capture the syntactic rules allowing assumptions of the form $!A$ to be duplicated and discarded.

### Intuitionistic case

The definition from Seely, adapted to the intuitionistic case and modernized, is:

###### Definition

Let $LinTypes$ be

which in addition carries the structure of

A Seely comonad on $LinTypes$ is a comonad that is a strong monoidal as a functor from cartesian monoidal structure $\times$ to the other monoidal structure $\otimes$:

$(LinTypes, \times) \xrightarrow{ \; ! \; } (LinTypes, \otimes)$

meaning that there are natural transformations of the form

(1)$A,\, B \colon LinTypes \;\;\;\;\;\;\; \vdash \;\;\;\;\;\;\; !(A \times B) \;\cong\; (!A) \otimes (!B)$

and

$! \ast \;\;\simeq\;\; \mathbb{1} \,.$

(There is also an additional coherence axiom that should be imposed; see Melliès 2009, section 7.3.)

###### Remark

(the exponential condition)
In linear logic, the cartesian monoidal structure on linear types is often denoted “$\&$” (“additive conjunction”), in which case the condition (1) reads

$!(A \& B) \;\cong\; (!A) \otimes (!B) \,.$

But in key examples of categories of (the multiplicative fragment of) linear logic (such as Vect, cf. Murfet 2014), the cartesian product is actually a biproduct, hence a direct sum, in which case the condition on the exponential modality is that

it takes (direct) sums to (tensor) products

$!(A \oplus B) \;\cong\; (!A) \otimes (!B)$

it takes zero (objects) to unit (objects)

$! 0 \;\cong\; \mathbb{1}$

as befits any exponential map and may explain the choice of terminology here.

This condition implies that the Kleisli category of $!$ (i.e. the category of cofree !-coalgebras) is cartesian monoidal. If $LinTypes$ 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 $\times$ was given by Benton, Bierman, de Paiva, and Hyland:

###### Definition

Let $LinTypes$ be a symmetric monoidal category; a linear exponential comonad on $LinTypes$ 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 more even-handed approach is the following (see Benton (1995) and Melliès (2009)), based on the observation that both Kleisli and Eilenberg-Moore categories are instances of adjunctions.

###### Definition

A linear-nonlinear adjunction is a monoidal adjunction $F \colon ClaTypes \rightleftarrows LinTypes \colon G$ in which $LinTypes$ is symmetric monoidal and $ClaTypes$ is cartesian monoidal. The induced !-modality is the induced comonad $F G$ on $LinTypes$.

This includes both of the previous definitions where $M$ is taken respectively to be the Kleisli category or the Eilenberg-Moore category of !. Conversely, in any linear-nonlinear adjunction the induced comonad $F G$ can be shown to be a linear exponential comonad. Moreover, if $!$ is a linear exponential comonad on a symmetric monoidal category $LinTypes$ 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 products in $C$, so we have $!(A\times B) \cong !A \otimes !B$, the Seely condition.

### Classical case

For “classical” linear logic, we want $LinTypes$ to be not just (closed) symmetric monoidal but $\ast$-autonomous. If an $\ast$-autonomous category has a linear exponential comonad $!$ one can derive a ? from the ! by de Morgan duality, $?A = \big(!(A^*)\big)^*$. The resulting relationship between ! and ? was axiomatized in a way not requiring the de Morgan duality by Blute, Cockett & Seely (1996):

###### Definition

Let $LinTypes$ be a linearly distributive category with tensor product $\otimes$ and cotensor product $\parr$. A (!,?)-modality on $LinTypes$ consists of:

1. a $\otimes$-monoidal comonad ! and a $\parr$-comonoidal monad ?

2. ? is a !-strong monad, and ! is a ?-strong comonad

3. all free !-coalgebras are naturally commutative $\otimes$-comonoids, and all free ?-algebras are naturally commutative $\parr$-monoids.

Here a functor $F$ is strong with respect to a lax monoidal functor $G$ if there is a natural transformation of the form $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. BCS96 showed that if $LinTypes$ is in fact $\ast$-autonomous, it follows from the above definition that $?A = \big(!(A^*)\big)^*$, as expected.

## Examples

### Relation to Chu construction

###### Theorem

Suppose $F \colon M \rightleftarrows C : G$ is a linear-nonlinear adjunction (Def. ), where $C$ is closed symmetric monoidal with finite limits and colimits, and $\bot\in C$ is an object. Then there is an induced linear-nonlinear adjunction $M \rightleftarrows Chu(C,\bot)$ where $Chu(C,\bot)$ is the Chu construction $Chu(C,\bot)$, which is $\ast$-autonomous with finite limits and colimits. Hence $Chu(C,\bot)$ admits a !-modality.

###### Proof

The embedding of $C$ in $Chu(C,\bot)$ as $A \mapsto (A, [A,\bot], ev)$ is coreflective: the coreflection of $(B^+, B^-, e_B)$ is $(B^+, [B^+,\bot], ev)$. Moreover, this subcategory is closed under the tensor product of $Chu(C,\bot)$, i.e. the embedding $C\hookrightarrow Chu(C,\bot)$ is strong monoidal, hence the adjunction is a monoidal adjunction. Therefore, the composite adjunction $M \rightleftarrows C \rightleftarrows Chu(C,\bot)$ is again a linear-nonlinear-adjunction.

Note that this theorem is a direct consequence of the work of Yves Lafont and Thomas Streicher on game semantics using the Chu construction, together with Benton’s reformulation of linear logic in terms of monoidal adjunctions. Since a Chu construction is $\ast$-autonomous, this !-modality implies a dual ?-modality.

###### Corollary

If $C$ is a cartesian closed category with finite limits and colimits and $\bot\in C$ is an object, then there is a linear-nonlinear adjunction $C \rightleftarrows Chu(C,\bot)$, and hence $Chu(C,\bot)$ admits a !-modality.

###### Proof

Apply the previous theorem to the identity adjunction $C\rightleftarrows C$.

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.

### Realization in linear homotopy type theory

In dependent linear homotopy type theory the “linear-nonlinear adjunction” is naturally identified (Ponto & Shulman (2012), Ex. 4.2, see also Schreiber (2014), Sec. 4.2) with the stabilization adjunction between homotopy types and stable homotopy types (Riley (2022), Prop. 2.1.31), whose left adjoint (forming suspension spectra $\Sigma^\infty_+$) is equivalently given (cf. Riley (2022), Rem. 2.4.13) by sending $B \,\colon\, Type$ to the linear dependent sum $\star_B \mathbb{1} \;\coloneqq\; (p_B)_! (p_B)^\ast \mathbb{1}$ over the monoidal unit in the context $B$. In terms of quantum modal logic this is forming the “linear randomization” of the given classical homotopy type (its “motive”):

(2) 

Curiously, this homotopy-theoretic realization of the exponential modality (beware the little subtlety of whether or not to reflect onto pointed homotopy types)

$\Sigma^\infty \circ \Omega^\infty \;\colon\; Spectra \to Spectra$

has independently been argued to have properties of an exponential map in the context of Goodwillie calculus, see there.

Moreover $\Sigma^\infty \dashv \Omega^\infty$ is a comonadic adjunction on simply connected homotopy types [Blomquist & Harper 2016 Thm. 1.8; Hess & Kedziorek 2017 Thm. 3.11], meaning that simply-connected classical (but pointed) homotopy types are identified with the $\Sigma^\infty \Omega^\infty$-modales among stable homotopy types.

Girard’s original presentation of linear logic involved rules that explicitly assumed the presence of $!$ on hypotheses or on entire contexts, such as dereliction, weakening and contraction:

$\frac{\Gamma, A \vdash B}{\Gamma, !A \vdash B} \qquad \frac{\Gamma \vdash B}{\Gamma, !A\vdash B} \qquad \frac{\Gamma,!A,!A \vdash B}{\Gamma, !A\vdash B}$

and “promotion”:

$\frac{!\Gamma \vdash A}{!\Gamma\vdash !A}$

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 1993 and then developed by Plotkin 1993, Wadler 1993, Benton 1995, Barber 1996.

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

$\phantom{-}$symbol$\phantom{-}$$\phantom{-}$in logic$\phantom{-}$
$\phantom{A}$$\in$$\phantom{A}$element relation
$\phantom{A}$$\,:$$\phantom{A}$typing relation
$\phantom{A}$$=$$\phantom{A}$equality
$\phantom{A}$$\vdash$$\phantom{A}$$\phantom{A}$entailment / sequent$\phantom{A}$
$\phantom{A}$$\top$$\phantom{A}$$\phantom{A}$true / top$\phantom{A}$
$\phantom{A}$$\bot$$\phantom{A}$$\phantom{A}$false / bottom$\phantom{A}$
$\phantom{A}$$\Rightarrow$$\phantom{A}$implication
$\phantom{A}$$\Leftrightarrow$$\phantom{A}$logical equivalence
$\phantom{A}$$\not$$\phantom{A}$negation
$\phantom{A}$$\neq$$\phantom{A}$negation of equality / apartness$\phantom{A}$
$\phantom{A}$$\notin$$\phantom{A}$negation of element relation $\phantom{A}$
$\phantom{A}$$\not \not$$\phantom{A}$negation of negation$\phantom{A}$
$\phantom{A}$$\exists$$\phantom{A}$existential quantification$\phantom{A}$
$\phantom{A}$$\forall$$\phantom{A}$universal quantification$\phantom{A}$
$\phantom{A}$$\wedge$$\phantom{A}$logical conjunction
$\phantom{A}$$\vee$$\phantom{A}$logical disjunction
symbolin type theory (propositions as types)
$\phantom{A}$$\to$$\phantom{A}$function type (implication)
$\phantom{A}$$\times$$\phantom{A}$product type (conjunction)
$\phantom{A}$$+$$\phantom{A}$sum type (disjunction)
$\phantom{A}$$0$$\phantom{A}$empty type (false)
$\phantom{A}$$1$$\phantom{A}$unit type (true)
$\phantom{A}$$=$$\phantom{A}$identity type (equality)
$\phantom{A}$$\simeq$$\phantom{A}$equivalence of types (logical equivalence)
$\phantom{A}$$\sum$$\phantom{A}$dependent sum type (existential quantifier)
$\phantom{A}$$\prod$$\phantom{A}$dependent product type (universal quantifier)
symbolin linear logic
$\phantom{A}$$\multimap$$\phantom{A}$$\phantom{A}$linear implication$\phantom{A}$
$\phantom{A}$$\otimes$$\phantom{A}$$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$$\phantom{A}$additive disjunction$\phantom{A}$
$\phantom{A}$$\&$$\phantom{A}$$\phantom{A}$additive conjunction$\phantom{A}$
$\phantom{A}$$\invamp$$\phantom{A}$$\phantom{A}$multiplicative disjunction$\phantom{A}$
$\phantom{A}$$\;!$$\phantom{A}$$\phantom{A}$exponential conjunction$\phantom{A}$

## References

### General

The notion of the exponential modality originates in linear logic with

A streamlined statement of the inference rules and the observation that these make the exponential a comonad is due to:

Review:

Brief survey in a context of computer science/linear type theory:

• Daniel Mihályi, Valerie Novitzká, Section 2.2 of: What about Linear Logic in Computer Science?, Acta Polytechnica Hungarica 10 4 (2013) 147-160 [pdf, pdf]

Further on the semantics of exponential conjunction as a comonad:

and its resolution by a monoidal adjunction between the linear and a classical (intuitionistic) type system:

Review:

Construction of such comonads based on cofree comonoids:

• 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:1509.03853

The relation to Fock space is discussed in:

The interpretation of $\Omega^\infty \Sigma^\infty_+$ as an exponential in the context of Goodwillie calculus is due to

• Gregory Arone, Marja Kankaanrinta, The Goodwillie tower of the identity is a logarithm, 1995 (web)

based on

On the modal type theory-approach to a term calculus for the $!$-modality:

A quantum programming language based on this linear/non-linear type theory adunction is QWIRE:

theoretical background:

applied to verified programming after implementation in Coq:

and using ambient homotopy type theory:

### In dependent linear type theory

Discussion of the exponential modality via stabilization in dependent linear homotopy type theory:

The $\Omega^\infty \Sigma^\infty$ comonadicity of simply connected pointed spaces over spectra:

category: logic

Last revised on February 8, 2024 at 18:19:24. See the history of this page for a list of all contributions to it.