There seem to be at least two ways to model linear logic using vector spaces.
The finite-dimensional vector spaces over a finite field form a model of (intuitionistic?) Linear Logic. Because everything in sight is finite, we sometimes call this model the finite vector spaces.
It is important that the underlying field is finite; otherwise the exponential is not easy to define. This observation seems to be folklore. The earliest it can be traced is in an email of Vaughan Pratt to the TYPES mailing list on 25 Feb 1992:
Now when is a finite field, vector spaces admit freezing: the space (where the object is the -dimensional space ) is the space of dimension . Binary relations on the other hand do not admit freezing without some work. What makes vector spaces freezable is that they are closed under addition, which turns out to be just right. If they only had scalar multiplication this would be too little. If they had multiplication as well as addition to make them a ring, like the ring of integers, this would err too far on the other side.
This model is presented in a bit more detail in the paper [Valiron and Zdancewic 2014, §4], and also in this set of slides (coauthored by Jennifer Paykin; a slightly different version can be found here).
The Valiron/Zdancewic/Paykin slides (but not the paper!) mention that transposition/taking the dual space makes this model extend to Classical Linear Logic. It is well-known that finite-dimensional vector spaces are a compact closed category, and hence a star-autonomous category. [Barr 1991, §5] sketches the construction of a cofree counitary coassociative cocommutative coalgebra (wow) in every compact closed category with enough equalizers; he then proceeds to contradict himself by saying that of all the categories in the paper only that of relations is closed (while he also mentions finite-dimensional vector spaces, which he also claims is compact through the usual natural isomorphism between a v.s. and its dual).
Research question: Is this well-understood? Does Barr's construction work for ? See also [Melliès, Tabareau, Tasson 2018].
In the case of a finite field of characteristic 2, [Hyland and Schalk 2003] give another construction, where is interpreted by the exterior algebra.
Research question: how is this related to the folk structure given above?
The category of (infinite-dimensional!) vector spaces over a field also forms a model of intuitionistic Linear Logic.
The most difficult part of the construction is again the exponential. It is sketched in [Hyland and Schalk 2003, §2.4]. A lot more detail is expanded in the survey [Murfet 2017].
Modelling Classical Linear Logic is much more difficult in the infinite-dimensional setting. A model that uses topological vector spaces for this purpose is given by [Kerjean 2016].
Barr, Michael. 1991. ‘*-Autonomous Categories and Linear Logic’. Mathematical Structures in Computer Science 1 (2): 159–78. https://doi.org/10.1017/S0960129500001274.
@article{barr_1991,
title = {{\ast}-{Autonomous} categories and linear logic},
volume = {1},
doi = {10.1017/S0960129500001274},
number = {2},
journal = {Mathematical Structures in Computer Science},
author = {Barr, Michael},
year = {1991},
pages = {159--178}
}
Valiron, Benoit, and Steve Zdancewic. 2014. ‘Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces’. Scientific Annals of Computer Science 24 (2): 325–68. https://doi.org/10.7561/SACS.2014.2.325. [pdf]
@article{valiron_2014,
title = {Modeling {Simply}-{Typed} {Lambda} {Calculi} in the {Category} of {Finite} {Vector} {Spaces}},
volume = {24},
doi = {10.7561/SACS.2014.2.325},
number = {2},
journal = {Scientific Annals of Computer Science},
author = {Valiron, Benoit and Zdancewic, Steve},
year = {2014},
pages = {325--368}
}
Hyland, Martin, and Andrea Schalk. 2003. ‘Glueing and Orthogonality for Models of Linear Logic’. Theoretical Computer Science 294 (1–2): 183–231. https://doi.org/10.1016/S0304-3975(01)00241-9. [pdf]
@article{hyland_glueing_2003,
title = {Glueing and orthogonality for models of linear logic},
volume = {294},
doi = {10.1016/S0304-3975(01)00241-9},
language = {en},
number = {1-2},
journal = {Theoretical Computer Science},
author = {Hyland, Martin and Schalk, Andrea},
year = {2003},
pages = {183--231}
}
Kerjean, Marie. 2016. ‘Weak Topologies for Linear Logic’. Logical Methods in Computer Science 12 (1): 3. https://doi.org/10.2168/LMCS-12(1:3)2016.
@article{kerjean_weak_2016,
title = {Weak topologies for {Linear} {Logic}},
volume = {12},
doi = {10.2168/LMCS-12(1:3)2016},
number = {1},
journal = {Logical Methods in Computer Science},
author = {Kerjean, Marie},
editor = {Abramsky, Samson},
year = {2016},
pages = {3},
file = {Kerjean - 2016 - Weak topologies for Linear Logic.pdf:C\:\\Users\\tz20861\\Zotero\\storage\\YPZL4MXS\\Kerjean - 2016 - Weak topologies for Linear Logic.pdf:application/pdf}
}
Murfet, Daniel. 2017. ‘Logic and Linear Algebra: An Introduction’. https://arxiv.org/abs/1407.2650.
Melliès, Paul-André, Nicolas Tabareau, and Christine Tasson. 2018. ‘An Explicit Formula for the Free Exponential Modality of Linear Logic’. Mathematical Structures in Computer Science 28 (7): 1253–86. https://doi.org/10.1017/S0960129516000426.
@article{mellies_explicit_2018,
title = {An explicit formula for the free exponential modality of linear logic},
volume = {28},
doi = {10.1017/S0960129516000426},
number = {7},
journal = {Mathematical Structures in Computer Science},
author = {Melliès, Paul-André and Tabareau, Nicolas and Tasson, Christine},
year = {2018},
pages = {1253--1286}
}