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.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)