Believe It Or Not, GOI is a Model of Classical Linear Logic - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2007

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

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

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

Identifiants

  • HAL Id : hal-03199716 , version 1

Citer

Jean Goubault-Larrecq. Believe It Or Not, GOI is a Model of Classical Linear Logic. 2007. ⟨hal-03199716⟩
25 Consultations
108 Téléchargements

Partager

Gmail Facebook X LinkedIn More