La bicatégorie cartésienne close des spans fins
Date(s) : 21/09/2023 iCal
11h00 - 12h30
Dans le modèle Rel de la logique linéaire, les types sont interprétés par des ensembles, et les preuves/programmes par des relations. Une idée naturelle pour avoir un modèle quantitatif, ou proof-relevant (c’est à dire que le modèle garde distinctes les différentes exécutions donnant lieu au même résultat observable), est d’utiliser des spans au lieu de relations. En effet la (bi)catégorie Span, dont les morphismes sont les spans d’ensembles composés par pullback, peut-être vue comme un analogue “proof-relevant”: là où une relation entre A et B ne garde qu’une information binaire (si a et b sont en relation), un span associe à tous a et b un ensemble de témoins, ou de “preuves” qu’ils sont en relation. Malheureusement, une adaptation naïve de l’exponentielle sur Rel ne fonctionne pas sur Span.
D’autres travaux, comme ceux sur les espèces de structure généralisées, fournissent des modèles proof-relevant, mais où la composition nécessite un quotient complexe des témoins, ne présentant ainsi pas l’aspect “concret” du pullback. Bien qu’un quotient semble inévitable, un autre modèle, celui des “jeux concurrents fins”, fait intervenir une composition concrète, sans quotient.
Adaptant les techniques utilisées dans ce dernier modèle, ce travail donne de bons résultats dans la direction d’un modèle de spans de LL, où la composition se fait par des pullbacks classiques. On montre notamment que, pour une pseudocomonade adéquate sur les spans, on obtient une bicatégorie de co-Kleisli cartésienne close.
Ceci est un travail en commun avec Pierre Clairambault.
Catégories
