Believe It Or Not, GOI is a Model of Classical Linear Logic - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Preprints, Working Papers, ... Year : 2007

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

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.
Fichier principal
Vignette du fichier
rr-lsv-2007-03.pdf (847.41 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03199716 , version 1 (15-04-2021)

Identifiers

  • HAL Id : hal-03199716 , version 1

Cite

Jean Goubault-Larrecq. Believe It Or Not, GOI is a Model of Classical Linear Logic. 2007. ⟨hal-03199716⟩
31 View
108 Download

Share

Gmail Facebook X LinkedIn More