Stone Duality for Monads

1. Problématique et Contexte

L'article s'attaque à la question fondamentale de la sémantique des effets de calcul (computation effects). Selon la théorie de Moggi, les notions de calcul sont décrites par des monades sur la catégorie des ensembles ($\mathbf{Set}$). Plus tard, Plotkin et Power ont raffiné cette vision en reliant les monades aux théories algébriques (opérations et équations).

Cependant, une question persiste : que signifie réellement qu'un terme « calcule » ? Une réponse courante est que le calcul est une interaction entre un programme et une réalité externe (un état, un environnement). Les équations algébriques ne seraient alors que des « ombres » de cette interaction. Les auteurs cherchent à décrire ces « réalités possibles » (les modèles de comportement) de manière intrinsèque, sans dépendre d'une monade spécifique $T$ donnée.

Le défi principal est de reconstruire la monade $T$ à partir de sa description comportementale. Pour les monades finitaires, la catégorie de comportement topologique $B_T$ (introduite par Garner) permet une reconstruction partielle, mais elle échoue pour les monades infinitaires ou pour des cas pathologiques (comme des états mémoire avec des contraintes d'injectivité impossibles à satisfaire globalement mais vérifiables localement). De plus, la reconstruction naïve $T \to B_T \to \Gamma(B_T)$ introduit des « calculs non raisonnables » qui consultent une information infinie instantanément.

2. Méthodologie

Les auteurs proposent une approche basée sur la dualité de Stone généralisée, en passant des espaces topologiques aux locales (l'approche « sans points » de la topologie).

• Catégorie de Comportement Localique ($LB_T$) : Au lieu d'utiliser des espaces topologiques, ils construisent une catégorie interne dans la catégorie des locales ($\mathbf{Loc}$).
  • Objets ($LB_0 T$) : Le locale des objets est défini comme le comodèle localique terminal de $T$. Ses ouverts sont générés par des conditions de comportement (ex: « le terme $t$ retourne $a$ »), soumis à des relations d'équivalence issues de la structure de la monade.
  • Morphismes ($LB_1 T$) : Le locale des transitions est construit via une faisceau (ou plus précisément un ensemble $B_J$-set) sur $LB_0 T$. Les sections globales de ce faisceau correspondent aux calculs « raisonnables » (continus), évitant ainsi les calculs qui nécessiteraient une information infinie non accessible.
• Foncteurs d'Adjonction :
  • Le foncteur gauche $LB$ associe à une monade $T$ sa catégorie de comportement localique $LB_T$. Les morphismes entre catégories localiques sont des rétrofoncteurs (internal retrofunctors), qui modélisent des simulations de systèmes de transition.
  • Le foncteur droit $\Gamma$ associe à une catégorie localique $LC$ une monade $\Gamma_{LC}$ dont les calculs sont les sections globales de la carte source de $LC$.
• Topologie de l'Information Finie : L'utilisation des locales permet de capturer la topologie de l'information finie, essentielle pour distinguer les calculs finis des calculs infinitaires pathologiques.

3. Contributions Clés

1. Construction de la Catégorie de Comportement Localique ($LB_T$) :
   Les auteurs définissent rigoureusement $LB_T$ pour toute monade rangée. Ils montrent que pour les monades finitaires, $LB_T$ est la version localique sous-jacente de la catégorie de comportement topologique classique $B_T$. Pour les monades infinitaires, $LB_T$ est strictement plus expressif et corrige les défauts de l'approche topologique (ex: exemple de l'état mémoire avec injectivité impossible).

2. L'Adjonction de Stone pour les Monades :
   Ils établissent une adjonction contravariante et idempotente :
   $$LB : \mathbf{Mnd}_r(\mathbf{Set}) \rightleftarrows \mathbf{LocRetro}^{op} : \Gamma$$
   où $\mathbf{Mnd}_r(\mathbf{Set})$ est la catégorie des monades rangées et $\mathbf{LocRetro}$ celle des catégories internes et rétrofoncteurs dans les locales.

3. Caractérisation des Points Fixes (Dualité) :
   L'article caractérise les objets fixes de cette adjonction :

   • Côté Monades : Les monades hyper-affines unaires (hyperaffine-unary monads). Ce sont des monades où chaque terme $t$ admet une opération « prédictive » (ou « scrying ») qui permet de connaître le résultat de $t$ sans exécuter ses effets de bord (rollback). Ces monades sont exactement celles dont la catégorie d'Eilenberg-Moore est cartésienne fermée.
   • Côté Catégories : Les catégories localiques amples (ample localic categories), définies par le fait que leur carte source est un homéomorphisme local et que leur locale d'objets est fortement de dimension zéro (ultraparacompact).

4. Généralisation de la Dualité de Stone Classique :
   L'article démontre que cette équivalence généralise la dualité de Stone classique entre les algèbres de Boole et les espaces de Stone. Une algèbre de Boole $B$ est vue comme une monade de partitions, et l'espace de Stone correspondant comme une catégorie localique avec uniquement des morphismes identité.

4. Résultats Principaux

• Théorème 4.4 : L'adjonction entre les monades rangées et les catégories localiques amples via les rétrofoncteurs est bien définie.
• Théorème 5.8 : L'adjonction est idempotente. Elle induit une équivalence de catégories entre :
  • La sous-catégorie pleine des monades hyper-affines unaires ($\mathbf{HUMnd}_r$).
  • La sous-catégorie pleine des catégories localiques amples ($\mathbf{AmpLocRetro}$).
• Cas Finitaire : Pour les monades finitaires, cette dualité se restreint à une équivalence entre les monades hyper-affines unaires finitaires et les catégories topologiques amples (sur des espaces de Stone).
• Correction des Défauts : L'approche localique résout le problème de la reconstruction de monades infinitaires où la sémantique topologique échoue (ex: le cas des cellules mémoire injectives sur un ensemble infini). Le locale d'objets $LB_0 T$ devient non trivial (sans points mais avec une structure riche), permettant de retrouver la monade originale via $\Gamma$.

5. Signification et Perspectives

• Sémantique des Programmes : Ce travail fournit un cadre mathématique robuste pour comprendre les effets de calcul non pas comme des opérations abstraites, mais comme des interactions avec un environnement structuré topologiquement. L'introduction des « opérations prédictives » (scrying) offre une nouvelle perspective sur la complétude des catégories d'Eilenberg-Moore.
• Logique des Programmes : Les auteurs suggèrent que cette dualité peut servir de fondement à une logique pour les programmes monadiques (type logique dynamique propositionnelle - PDL). La catégorie de comportement $LB_T$ agit comme un modèle de Kripke où les propositions sont des ouverts clopens.
• Théorie des Schémas pour les Monades : L'article ouvre la voie à une « théorie des schémas pour les monades », analogue à la géométrie algébrique. L'idée est de considérer des catégories localiques qui ressemblent localement à des catégories de comportement, permettant de modéliser des effets dont la syntaxe varie continûment (ex: un état local).
• Extensions Futures : Les auteurs envisagent d'appliquer cette dualité aux modèles résiduels (comodels résiduels) pour gérer la non-termination, et de généraliser la construction au-delà de $\mathbf{Set}$ vers des catégories de restriction.

En résumé, cet article établit une dualité de Stone pour les monades, reliant l'algèbre des calculs (monades) à la géométrie des états (catégories localiques), en résolvant des problèmes d'infinité et de reconstruction sémantique grâce à la puissance des locales et des rétrofoncteurs.