The informal notion of webbed semantics covers categorical models of linear logic of the form:
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.
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
with, for and ,
Note that here 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:
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).
We write for the finite multiset consisting of the elements (counted with multiplicity) and .
The structural rules (comonoid structure on ) are interpreted by
The comonad structure on is given by
The co-Kleisli category is cartesian closed; it interprets the non-linear function arrow as . Observe that for an infinite countable set , the function space 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.
Hyland, Martin. "Some Reasons for Generalising Domain Theory". Mathematical Structures in Computer Science 20, nᵒ2 (April 2010): 239‑65. https://doi.org/10.1017/S0960129509990375.
@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}
}
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 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.
Melliès, Paul-André. 2009. ‘Categorical Semantics of Linear Logic’. In Panoramas et Synthèses 27: Interactive Models of Computation and Program Behaviour, edited by Pierre-Louis Curien, Hugo Herbelin, Jean-Louis Krivine, and Paul-André Melliès. Société Mathématique de France. pdf.
@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}
}
However, there is a way to define an exponential modality in Rel with (where 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 between the powerset functor (which sends to and the forgetful functor is in fact a linear-non-linear adjunction, so the comonad is an exponential modality. Computing the counit gives .
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.
The categorified version (Girard's normal functors, APAL 1998) came first and was a source of inspiration in the discovery of linear logic.
Girard, Jean-Yves. "Normal functors, power series and λ-calculus". Annals of Pure and Applied Logic 37, nᵒ2 (February 1988): 129‑77. https://doi.org/10.1016/0168-0072(88)90025-5.
@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}
}
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):
Girard, Jean-Yves. "The system F of variable types, fifteen years later". Theoretical Computer Science 45 (January 1986): 159‑92. https://doi.org/10.1016/0304-3975(86)90044-7.
@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 as and as .
A hypercoherence is a set together with a set whose elements are finite non-empty subsets of ; all singletons are required to be members of . The name comes from the fact that hypercoherences are hypergraphs (whereas coherence spaces are undirected graphs).
A clique of a hypercoherence is a subset of whose finite non-empty subsets all belong to . As usual, the morphisms in the category of hypercoherences are the cliques of (as defined below), whose web is , so they are binary relations; the composition of two cliques in and is indeed a clique in .
The connectives of linear logic act on hypercoherences as follows:
There is also an exponential modality such that consists of finite cliques of . 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.
Ehrhard, Thomas. "Parallel and serial hypercoherences". Theoretical Computer Science 247, nᵒ1 (September 2000): 39‑81. https://doi.org/10.1016/S0304-3975(00)00173-0.
@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}
}
Boudes, Pierre. "Projecting Games on Hypercoherences". ICALP 2004. pdf
@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}
}
Melliès, Paul-André. "Sequential algorithms and strongly stable functions" Theoretical Computer Science, Special issue "Game Theory Meets Theoretical Computer Science", 343, nᵒ1 (October 2005): 237‑81. https://doi.org/10.1016/j.tcs.2005.05.015.
@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 give rise to topological vector spaces, and this construction leads to a vector space model of linear logic.
The main reference is perhaps:
Ehrhard, Thomas. "The Scott model of linear logic is the extensional collapse of its relational model". Theoretical Computer Science 424 (March 2012): 20‑45. https://doi.org/10.1016/j.tcs.2011.11.027.
@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:
Terui, Kazushige. "Semantic Evaluation, Intersection Types and Complexity of Simply Typed Lambda Calculus". RTA 2012. https://doi.org/10.4230/LIPIcs.RTA.2012.323
@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}
}
Grellois, Charles. "Semantics of Linear Logic and Higher-Order Model-Checking". PhD thesis, Université Denis Diderot Paris 7, 2016. archived pdf
@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}
}
Melliès, Paul-André. "Higher-order parity automata". LICS 2017. pdf
@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}
}