Résumé technique : Monades et lois de distribution dans des contextes sous-structuraux

1. Énoncé du problème

En sémantique des programmes et en modélisation de systèmes, les monades servent d'interface uniforme pour les effets computationnels (par exemple, la non-déterminisme, la probabilité, les exceptions). Un défi central consiste à combiner deux effets distincts modélisés par des monades $S$ et $T$. Mathématiquement, cela nécessite une loi de distribution $\delta: ST \to TS$, qui équipe le foncteur composé $TS$ d'une structure de monade.

Bien que de nombreuses lois de distribution existent, des théorèmes de « non-existence » (par exemple, l'observation de Plotkin concernant la monade de probabilité $D$ et la monade des ensembles de parties $P$) démontrent que les lois de distribution n'existent pas toujours. Les approches précédentes à ce problème ont inclus :

1. Lois de distribution faibles : Assouplir la compatibilité avec les unités, modifiant souvent la monade cible $T$.
2. Raffinement : Modifier la monade source $S$ en supprimant les axiomes équationnels « problématiques » qui empêchent l'existence de $\delta$.

Le problème spécifique abordé dans cet article est l'absence d'un cadre unifié, catégoriel et indépendant de la présentation pour l'approche de « raffinement ». Les travaux existants ont identifié le rôle des règles structurelles (échange, affaiblissement, contraction) dans l'échec ou le succès des lois de distribution, mais ces observations étaient spécifiques à des contextes particuliers plutôt que formalisées de manière générale.

2. Méthodologie

Les auteurs développent une théorie catégorielle paramétrée par des catégories verbales (introduites par Tronin), qui modélisent des contextes sous-structuraux en restreignant les règles structurelles sur les contextes de variables.

2.1 Catégories verbales ($W$)

Le cadre utilise des catégories verbales, définies comme des sous-catégories larges de $\mathcal{F}$ (la catégorie des ordinaux finis et des fonctions) closes sous une opération de « substitution verbale ». Ces catégories correspondent à des combinaisons spécifiques de règles structurelles :

• $F_{id}$ : Aucune règle structurelle.
• $F_{bij}$ : Échange uniquement (symétrique).
• $F_{surj}$ : Échange et contraction.
• $F_{inj}$ : Échange et affaiblissement.
• $F$ : Toutes les règles structurelles.

2.2 Monades $W$-opéradiques

L'article introduit les monades $W$-opéradiques. Une monade $S$ est $W$-opéradique si elle est induite par une $W$-opérade via une extension de Kan le long de l'inclusion $J: W \to \mathbf{Set}$.

• Intuitivement, une $W$-opérade encode une théorie algébrique où les termes sont soumis uniquement aux règles structurelles autorisées dans $W$.
• Les exemples incluent :
  • Les monades $F_{id}$-opéradiques correspondent aux opérades non symétriques (par exemple, la monade liste).
  • Les monades $F_{bij}$-opéradiques correspondent aux opérades symétriques (par exemple, les monades d'ensembles multiples).
  • Les monades $F_{surj}$-opéradiques correspondent aux opérades régulières (par exemple, la monade des distributions de probabilité).

2.3 Monades $W$-commutatives

Pour construire une loi de distribution, la monade cible $T$ doit satisfaire une condition par rapport à $W$. Les auteurs définissent les monades $W$-commutatives en utilisant une structure monoïdale lax dérivée des forces uniques de $T$.

• Une monade $T$ est $W$-commutative si sa structure monoïdale lax $\psi$ est compatible avec les morphismes de $W$.
• Cela unifie des propriétés connues :
  • $F_{bij}$-commutatif $\iff$ Commutativité ordinaire.
  • $F_{inj}$-commutatif $\iff$ Commutatif et Affine.
  • $F_{surj}$-commutatif $\iff$ Commutatif et Pertinent.

2.4 Stratégie de construction

La stratégie centrale consiste à trouver une catégorie verbale $W$ telle que :

1. $S$ soit $W$-opéradique (définie en utilisant les règles de $W$).
2. $T$ soit $W$-commutative (invariante sous les règles de $W$).

Si l'intersection de l'« ensemble supérieur » de l'opéradicité de $S$ et de l'« ensemble inférieur » de la commutativité de $T$ est non vide, une loi de distribution canonique peut être construite. Si l'intersection est vide, les auteurs proposent un raffinement $W$-opéradique pour modifier $S$.

3. Contributions clés

3.1 Construction de loi de distribution canonique (Théorème 42)

L'article présente une construction générale d'une loi de distribution $\delta: ST \to TS$ pour :

• $S$ : Une monade $W$-opéradique.
• $T$ : Une monade $W$-commutative.

La construction est catégorielle et canonique, définie via la description par co-end de l'extension de Kan utilisée pour définir $S$.

• Compatibilité : $\delta$ est compatible avec l'unité et la multiplication de $S$ et l'unité de $T$ sans condition.
• Compatibilité de la multiplication : $\delta$ est compatible avec la multiplication de $T$ ($\mu_T$) si l'une des conditions suivantes est remplie :
  1. $T$ est commutative (sens ordinaire), ou
  2. $S$ est générée par des opérations d'arité $\le 1$ (par exemple, $W = F_{id}$).

3.2 Raffinement $W$-opéradique (Section 6)

Lorsqu'une monade $S$ n'est pas $W$-opéradique pour un $W$ requis, les auteurs introduisent le raffinement $W$-opéradique, noté $Rf_W(S)$.

• Définition : $Rf_W(S) = \text{Mnd}(W\text{-Opd}(S))$, où $W\text{-Opd}(S)$ est la $W$-opérade induite en restreignant $S$ à $W$.
• Propriété : Il s'agit d'une construction universelle (un comonade sur la catégorie des monades) qui force $S$ à devenir $W$-opéradique en supprimant les axiomes équationnels qui violent les règles structurelles de $W$.
• Signification : Cela fournit un mécanisme formel et indépendant de la présentation pour l'approche de « raffinement » précédemment utilisée de manière ad hoc.

3.3 Unification des résultats connus

Le cadre unifie divers résultats spécifiques de la littérature (par exemple, [11, 51, 52, 30, 32, 20]) sous une seule théorie opéradique. Il clarifie pourquoi certaines combinaisons d'effets (comme la probabilité et le non-déterminisme) échouent et comment elles peuvent être corrigées en raffinant la monade source.

4. Résultats et applications

4.1 Résolution de la monade de valuation indexée

L'article réexamine la monade de valuation indexée $IV$ introduite par Varacca et Winskel [68] pour modéliser la combinaison de la probabilité et du non-déterminisme.

• Problème : La monade de valuation standard $V$ et la monade des ensembles de parties finis non vides $P^+_{fin}$ n'admettent pas de loi de distribution.
• Résultat : Les auteurs prouvent que $IV$ est isomorphe au raffinement $F_{inj}$-opéradique de $V$ ($Rf_{F_{inj}}(V)$).
• Implication : La loi de distribution $IV P^+_{fin} \to P^+_{fin} IV$ construite dans [68] est exactement la loi de distribution canonique fournie par le Théorème 42 lorsque $S = Rf_{F_{inj}}(V)$ et $T = P^+_{fin}$.

4.2 Nouvelles lois de distribution

Le cadre génère de nouvelles lois de distribution en imposant l'opéradicité $W$ :

• Exemple 50 : Une loi de distribution entre la monade de valuation indexée $IV$ et la monade de distribution de probabilité $D$ ($IV D \to DIV$). Cela résout un mauvais comportement catégoriel dans une famille de morphismes $\lambda: DD \to DD$ utilisée dans [67] pour la sémantique des MDP.
• Exemple 66 : Une loi de distribution entre la monade des ensembles de parties finis raffinée et une monade d'écriture, modélisant des processus où les effets secondaires sont accumulés indépendamment du fait que la sortie soit utilisée.

4.3 Détection de « non-existence »

Le cadre fournit un moyen systématique de détecter une éventuelle non-existence de lois de distribution. Si l'intersection de l'opéradicité de $S$ et de la commutativité de $T$ est vide pour tous les $W$ pertinents, la construction canonique échoue. Bien que cela ne prouve pas un théorème de « non-existence » (des lois non canoniques pourraient exister), cela sert d'« alarme rouge » robuste (par exemple, pour le couple $(D, P_{fin})$).

5. Signification et affirmations

L'article prétend fournir une image catégorielle unificatrice pour l'interaction entre les règles structurelles et les lois de distribution.

• Uniformité : Il va au-delà d'exemples spécifiques pour une théorie paramétrée par des catégories verbales, rendant le rôle de l'échange, de l'affaiblissement et de la contraction explicite et uniforme.
• Indépendance de la présentation : Contrairement aux approches de raffinement précédentes qui reposaient sur des présentations équationnelles spécifiques, le raffinement $W$-opéradique est une construction universelle indépendante de la manière dont la monade est présentée.
• Fondement opéradique : Il établit que l'existence de lois de distribution est fondamentalement liée à la nature opéradique de la monade source et aux propriétés de commutativité de la monade cible par rapport au même contexte structurel.

Les auteurs notent que, bien que la théorie soit développée pour les monades sur $\mathbf{Set}$, l'extension à d'autres catégories de base et l'adaptation des approches de « modification de $T$ » sont des directions naturelles pour l'avenir. La théorie est présentée comme une étape fondamentale vers la compréhension de la combinaison d'effets en sémantique des programmes et en vérification de modèles.