Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Believe It Or Not, GOI is a Model of Classical Linear Logic

Jean Goubault-Larrecq 1
1 SECSI - Security of information systems
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We introduce the Danos-Régnier category $DR(M)$ of a linear inverse monoid $M$, a categorical description of geometries of interaction (GOI). The usual setting for GOI is that of a weakly Cantorian linear inverse monoid. It is well-known that GOI is perfectly suited to describe the multiplicative fragment of linear logic, and indeed $DR(M)$ will be a ∗-autonomous category in this case. It is also wellknown that the categorical interpretation of the other linear connectives conflicts with GOI interpretations. We make this precise, and show that $DR(M)$ has no terminal object, no cartesian product, and no exponential—whatever M is, unless M is trivial. However, a form of coherence completion of $DR(M)$ à la Hu-Joyal provides a model of full classical linear logic, as soon as $M$ is weakly Cantorian.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal.inria.fr/hal-03199716
Contributor : Jean Goubault-Larrecq <>
Submitted on : Thursday, April 15, 2021 - 8:47:06 PM
Last modification on : Saturday, May 1, 2021 - 3:41:29 AM

File

rr-lsv-2007-03.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03199716, version 1

Citation

Jean Goubault-Larrecq. Believe It Or Not, GOI is a Model of Classical Linear Logic. 2021. ⟨hal-03199716⟩

Share

Metrics

Record views

8

Files downloads

108