The relational model of linear logic and its variants ("webbed semantics")

The informal notion of webbed semantics covers categorical models of linear logic of the form:

• objects: a set endowed with some additional structure; the underlying set of an object X is called the web of X and traditionally denoted by |X| (not to be confused with the cardinality of X…);
• morphisms X \to Y: binary relations between |X| and |Y| that are compatible in some sense with the structure on X and Y.

They tend to have forgetful functors to the relational model (which is the case without any additional structure), that preserve the connectives of MALL, but generally not the exponentials.

The "vanilla" relational model

See also the LLwiki page.

Arguably the simplest denotational semantics of linear logic is the category Rel of sets and relations. Its compact closed structure is

A \otimes B = A \times B \qquad A^\perp = A

with, for R \subseteq A \times B and S \subseteq B \times C,

R \otimes S = \{((x,y),(x',y')) \mid (x,x') \in R,\, (y,y') \in S\} \qquad R^\perp = \{(y,x) \mid (x,y) \in R\}

Note that here \times the cartesian product of sets, which is not a categorical product on Rel. That said, Rel does admit a product, which is also a coproduct, namely the disjoint union of relations:

A \& B = A \oplus B = A + B

For the exponential modality there are multiple possibilities, although the "standard" choice is the one based on finite multisets (thus providing the simplest example of a quantitative semantics of linear logic).

Usual multiset-based exponential

We write [a_1,\dots,a_n] for the finite multiset consisting of the elements a_1,\dots,a_n (counted with multiplicity) and [a_1,\dots,a_n]+[a_{n+1},\dots,a_m] = [a_1,\dots,a_m].

!A = \{[a_1,\dots,a_n] \mid n \in \mathbb{N},\, (a_1,\dots,a_n) \in A^n\}

The structural rules (comonoid structure on !A) are interpreted by

\mathrm{contraction}_A = \{(M+N, (M,N)) \mid M, N \in\; !A\} \subseteq\; !A \multimap !A \otimes !A

\mathrm{weakening}_A = \{([], *)\} \subseteq\; !A \multimap 1 =\; !A \times \{*\}

The comonad structure on !(-) is given by

\varepsilon^!_A = \{([a],a)\mid a \in A\} \subseteq\; !A \multimap A

\delta^!_A = \{(M_1 + \dots + M_n, [M_1,\dots,M_n]) \mid M_1,\dots,M_n \in\; !A\} \subseteq\; !A \multimap\; !!A

The co-Kleisli category is cartesian closed; it interprets the non-linear function arrow as A \Rightarrow B =\; !A \multimap B = (\text{finite multisets of}\ A) \times B. Observe that for an infinite countable set D, the function space D \Rightarrow D is then also countable. By taking a bijection between the two, one gets a model of the untyped λ-calculus. Hyland has argued that this is simpler than the usual domain-theoretic construction:

In the early 1970s it seemed as if domain theory had been invented primarily in order to enable one to construct genuinely mathematical models of the pure lambda calculus. But knowing what we do now, domain theory is not at all the most natural and obvious place to find such models. Rather, the easiest construction takes place using the relational model, which is the fundamental degenerate model for linear logic.

@article{DBLP:journals/mscs/Hyland10,
  author    = {Martin Hyland},
  title     = {Some reasons for generalising domain theory},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {20},
  number    = {2},
  pages     = {239--265},
  year      = {2010},
  url       = {https://doi.org/10.1017/S0960129509990375},
  doi       = {10.1017/S0960129509990375},
  timestamp = {Wed, 01 Apr 2020 08:48:36 +0200},
  biburl    = {https://dblp.org/rec/journals/mscs/Hyland10.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

The naive set-based exponential doesn't work

One could be tempted to copy the set-based exponential of coherence spaces or hypercoherences (see below) in the obvious way (consider finite subsets instead of finite cliques). However, Ehrhard discovered that this does not satisfy the categorical axiomatics: if one defines the counit as \varepsilon_A = \{(\{a\},a)\mid a \in A\} then it is not a natural transformation. To quote Melliès 2009:

This lack of commutation was somewhat unexpected the first time it was noticed. It convinced people that every coherence diagram should be checked extremely carefully every time a new model is introduced. This also propelled the search for alternative categorical axiomatics of linear logic, more conceptual and easier to check than the existing ones.

@incollection{mellies_2009,
	title = {Categorical {Semantics} of {Linear} {Logic}},
	isbn = {978-2-85629-273-0},
	url = {http://www.pps.univ-paris-diderot.fr/~mellies/papers/panorama.pdf},
	booktitle = {Panoramas et synthèses 27: {Interactive} models of computation and program behaviour},
	publisher = {Société Mathématique de France},
	author = {Melliès, Paul-André},
	editor = {Curien, Pierre-Louis and Herbelin, Hugo and Krivine, Jean-Louis and Melliès, Paul-André},
	year = {2009}
}

Exotic set-based exponential (linearization of Set)

However, there is a way to define an exponential modality in Rel with !A = \mathcal{P}(A) (where \mathcal{P} denotes the powerset: we take all subsets, not just finite ones). This seems to have been well-known folklore in the 1990s, although it is less known nowadays.

The basic idea is that the adjunction \mathcal{P} \dashv U between the powerset functor \mathcal{P} : \mathrm{Rel \to Set} (which sends R \subseteq A \times B to S \mapsto \{b \in B \mid \exists a \in S.\, (a,b) \in R\} and the forgetful functor U : \mathrm{Set \to Rel} is in fact a linear-non-linear adjunction, so the comonad ! = U \circ \mathcal{P} is an exponential modality. Computing the counit gives \varepsilon_A = \{(S,x) \mid x \in S \subseteq A\}.

The co-Kleisli category of this comonad is automatically a cartesian closed category; observe that it is equivalent to the full subcategory of Set whose objects are powersets. Thus, the relational model with this exponential modality can be seen as a linearization of the usual set-theoretic semantics of the simply typed λ-calculus.

Quantitative relational model (matrices)

The categorified version (Girard's normal functors, APAL 1998) came first and was a source of inspiration in the discovery of linear logic.

@article{DBLP:journals/apal/Girard88,
  author    = {Jean{-}Yves Girard},
  title     = {Normal functors, power series and {\(\lambda\)}-calculus},
  journal   = {Annals of Pure and Applied Logic},
  volume    = {37},
  number    = {2},
  pages     = {129--177},
  year      = {1988},
  url       = {https://doi.org/10.1016/0168-0072(88)90025-5},
  doi       = {10.1016/0168-0072(88)90025-5},
  timestamp = {Fri, 21 Feb 2020 21:18:39 +0100},
  biburl    = {https://dblp.org/rec/journals/apal/Girard88.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

Coherence spaces

LLwiki page

The denotational semantics introduced in Girard's original paper on linear logic.

Coherence spaces are a simplification of qualitative domains, one of the first domain-theoretic semantics for System F. Qualitative domains were introduced in the following paper (whose Appendix C describes coherence spaces):

@article{DBLP:journals/tcs/Girard86,
  author    = {Jean{-}Yves Girard},
  title     = {The System {F} of Variable Types, Fifteen Years Later},
  journal   = {Theoretical Computer Science},
  volume    = {45},
  number    = {2},
  pages     = {159--192},
  year      = {1986},
  url       = {https://doi.org/10.1016/0304-3975(86)90044-7},
  doi       = {10.1016/0304-3975(86)90044-7},
  timestamp = {Wed, 17 Feb 2021 21:58:37 +0100},
  biburl    = {https://dblp.org/rec/journals/tcs/Girard86.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

This model of system F was a decisive influence in the discovery of linear logic; to quote the Linear Logic 1987 paper:

Linear logic first appeared after the author had been challenged by Berry and Curien to extend the coherent semantics (at the time: qualitative semantics) to the sum of types, their claim being that it was necessary to reintroduce complications that are typical for Scott domains. The answer is reproduced in an appendix of Girard APAL 1998, and (except for the notations which are absent) one can recognize (semantically) the decomposition of the type A \Rightarrow B as !A \multimap B and A \lor B as !A\oplus!B.

Hypercoherences

A hypercoherence X is a set |X| together with a set \Gamma(X) whose elements are finite non-empty subsets of |X|; all singletons are required to be members of \Gamma(X). The name comes from the fact that hypercoherences are hypergraphs (whereas coherence spaces are undirected graphs).

A clique of a hypercoherence X is a subset of |X| whose finite non-empty subsets all belong to \Gamma(X). As usual, the morphisms X \to Y in the category of hypercoherences are the cliques of X \multimap Y = (X \otimes Y^\perp)^\perp (as defined below), whose web is |X| \times |Y|, so they are binary relations; the composition of two cliques in X \multimap Y and Y \multimap Z is indeed a clique in X \multimap Z.

The connectives of linear logic act on hypercoherences as follows:

|X^\perp| = |X| \qquad |X \otimes Y| = |X| \times |Y| \qquad |X \oplus Y| = |X| + |Y|

\Gamma(X^\perp) = \{S \subseteq |X| \mid S\ \text{finite non-empty}, S \notin \Gamma(X)\ \text{or}\ S\ \text{singleton}\}

\Gamma(X_1 \otimes X_2) = \{ S \subseteq |X| \mid \forall i \in \{1,2\},\; \pi_i(S) \in \Gamma(X_i) \}

\Gamma(X \oplus Y) = \mathsf{inl}(\Gamma(X)) \cup \mathsf{inr}(\Gamma(Y))

There is also an exponential modality such that |!X| consists of finite cliques of X. The morphisms in its co-Kleisli category are strongly stable functions in the sense of domain theory.

Ehrhard, Boudes and Melliès have investigated connections between hypercoherences and game semantics. The basic idea (which is not explicitly stated in this way) is that hypercoherences are a sort of positional quotient of Blass games, making the latter into an actual model of linear logic.

@article{DBLP:journals/tcs/Ehrhard00,
  author    = {Thomas Ehrhard},
  title     = {Parallel and serial hypercoherences},
  journal   = {Theoretical Computer Science},
  volume    = {247},
  number    = {1-2},
  pages     = {39--81},
  year      = {2000},
  url       = {https://doi.org/10.1016/S0304-3975(00)00173-0},
  doi       = {10.1016/S0304-3975(00)00173-0},
  timestamp = {Wed, 17 Feb 2021 21:58:34 +0100},
  biburl    = {https://dblp.org/rec/journals/tcs/Ehrhard00.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/icalp/Boudes04,
  author    = {Pierre Boudes},
  editor    = {Josep D{\'{\i}}az and
               Juhani Karhum{\"{a}}ki and
               Arto Lepist{\"{o}} and
               Donald Sannella},
  title     = {Projecting Games on Hypercoherences},
  booktitle = {Automata, Languages and Programming: 31st International Colloquium,
               {ICALP} 2004, Turku, Finland, July 12-16, 2004. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {3142},
  pages     = {257--268},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/978-3-540-27836-8\_24},
  doi       = {10.1007/978-3-540-27836-8\_24},
  timestamp = {Tue, 14 May 2019 10:00:44 +0200},
  biburl    = {https://dblp.org/rec/conf/icalp/Boudes04.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/tcs/Mellies05,
  author    = {Paul{-}Andr{\'{e}} Melli{\`{e}}s},
  title     = {Sequential algorithms and strongly stable functions},
  journal   = {Theoretical Computer Science},
  volume    = {343},
  number    = {1-2},
  pages     = {237--281},
  year      = {2005},
  url       = {https://doi.org/10.1016/j.tcs.2005.05.015},
  doi       = {10.1016/j.tcs.2005.05.015},
  timestamp = {Wed, 17 Feb 2021 22:00:50 +0100},
  biburl    = {https://dblp.org/rec/journals/tcs/Mellies05.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

Finiteness spaces

LLwiki page

Finiteness spaces give rise to topological vector spaces, and this construction leads to a vector space model of linear logic.

Linearized Scott domains (prime-algebraic lattices)

The main reference is perhaps:

@article{DBLP:journals/tcs/Ehrhard12,
  author    = {Thomas Ehrhard},
  title     = {The Scott model of linear logic is the extensional collapse of its
               relational model},
  journal   = {Theoretical Computer Science},
  volume    = {424},
  pages     = {20--45},
  year      = {2012},
  url       = {https://doi.org/10.1016/j.tcs.2011.11.027},
  doi       = {10.1016/j.tcs.2011.11.027},
  timestamp = {Wed, 17 Feb 2021 22:00:42 +0100},
  biburl    = {https://dblp.org/rec/journals/tcs/Ehrhard12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

Interestingly this model has applications outside of linear logic:

• computational complexity in the simply typed λ-calculus Terui 2012;
• higher-order model checking (Grellois & Melliès).

@inproceedings{DBLP:conf/rta/Terui12,
  author    = {Kazushige Terui},
  editor    = {Ashish Tiwari},
  title     = {Semantic Evaluation, Intersection Types and Complexity of Simply Typed
               Lambda Calculus},
  booktitle = {23rd International Conference on Rewriting Techniques and Applications
               (RTA'12) , {RTA} 2012, May 28 - June 2, 2012, Nagoya, Japan},
  series    = {LIPIcs},
  volume    = {15},
  pages     = {323--338},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year      = {2012},
  url       = {https://doi.org/10.4230/LIPIcs.RTA.2012.323},
  doi       = {10.4230/LIPIcs.RTA.2012.323},
  timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
  biburl    = {https://dblp.org/rec/conf/rta/Terui12.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@phdthesis{DBLP:phd/hal/Grellois16,
  author    = {Charles Grellois},
  title     = {Semantics of linear logic and higher-order model-checking. (S{\'{e}}mantique
               de la logique lin{\'{e}}aire et "model-checking" d'ordre sup{\'{e}}rieur)},
  school    = {Paris Diderot University, France},
  year      = {2016},
  url       = {https://tel.archives-ouvertes.fr/tel-01311150},
  timestamp = {Tue, 21 Jul 2020 00:40:56 +0200},
  biburl    = {https://dblp.org/rec/phd/hal/Grellois16.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/lics/Mellies17,
  author    = {Paul{-}Andr{\'{e}} Melli{\`{e}}s},
  title     = {Higher-order parity automata},
  booktitle = {32nd Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
               2017, Reykjavik, Iceland, June 20-23, 2017},
  pages     = {1--12},
  publisher = {{IEEE} Computer Society},
  year      = {2017},
  url       = {https://doi.org/10.1109/LICS.2017.8005077},
  doi       = {10.1109/LICS.2017.8005077},
  timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
  biburl    = {https://dblp.org/rec/conf/lics/Mellies17.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}