Resumen Técnico: Mónadas y Leyes Distributivas en Contextos Subestructurales

1. Enunciado del Problema

En la semántica de programas y el modelado de sistemas, las mónadas sirven como una interfaz uniforme para efectos computacionales (por ejemplo, no determinismo, probabilidad, excepciones). Un desafío central es combinar dos efectos distintos modelados por mónadas $S$ y $T$. Matemáticamente, esto requiere una ley distributiva $\delta: ST \to TS$, que dota al funtor compuesto $TS$ de una estructura de mónada.

Aunque existen muchas leyes distributivas, los teoremas de "no-go" (por ejemplo, la observación de Plotkin respecto a la mónada de probabilidad $D$ y la mónada del conjunto potencia $P$) demuestran que las leyes distributivas no siempre existen. Los enfoques anteriores para este problema han incluido:

1. Leyes distributivas débiles: Relajar la compatibilidad con las unidades, modificando a menudo la mónada objetivo $T$.
2. Refinamiento: Modificar la mónada fuente $S$ eliminando axiomas equacionales "problemáticos" que impiden la existencia de $\delta$.

El problema específico abordado en este artículo es la falta de un marco unificado, categórico e independiente de la presentación para el enfoque de "refinamiento". El trabajo existente ha identificado el papel de las reglas estructurales (intercambio, debilitamiento, contracción) en el fracaso o éxito de las leyes distributivas, pero estas observaciones han sido específicas de contextos particulares en lugar de formalizarse de manera general.

2. Metodología

Los autores desarrollan una teoría categórica parametrizada por categorías verbales (introducidas por Tronin), que modelan contextos subestructurales restringiendo las reglas estructurales sobre los contextos de variables.

2.1 Categorías Verbales ($W$)

El marco utiliza categorías verbales, definidas como subcategorías amplias de $\mathcal{F}$ (la categoría de ordinales finitos y funciones) cerradas bajo una operación de "sustitución verbal". Estas categorías corresponden a combinaciones específicas de reglas estructurales:

• $F_{id}$: Sin reglas estructurales.
• $F_{bij}$: Solo intercambio (simétrico).
• $F_{surj}$: Intercambio y contracción.
• $F_{inj}$: Intercambio y debilitamiento.
• $F$: Todas las reglas estructurales.

2.2 Mónadas $W$-Operádicas

El artículo introduce mónadas $W$-operádicas. Una mónada $S$ es $W$-operádica si es inducida por una $W$-operada mediante una extensión de Kan izquierda a lo largo de la inclusión $J: W \to \mathbf{Set}$.

• Intuitivamente, una $W$-operada codifica una teoría algebraica donde los términos están sujetos solo a las reglas estructurales permitidas en $W$.
• Los ejemplos incluyen:
  • Las mónadas $F_{id}$-operádicas corresponden a operadas no simétricas (por ejemplo, la mónada de listas).
  • Las mónadas $F_{bij}$-operádicas corresponden a operadas simétricas (por ejemplo, mónadas de multiconjuntos).
  • Las mónadas $F_{surj}$-operádicas corresponden a operadas regulares (por ejemplo, la mónada de distribuciones de probabilidad).

2.3 Mónadas $W$-Conmutativas

Para construir una ley distributiva, la mónada objetivo $T$ debe satisfacer una condición relativa a $W$. Los autores definen mónadas $W$-conmutativas utilizando una estructura monoidal laxa derivada de las fuerzas únicas de $T$.

• Una mónada $T$ es $W$-conmutativa si su estructura monoidal laxa $\psi$ es compatible con los morfismos en $W$.
• Esto unifica propiedades conocidas:
  • $F_{bij}$-conmutativa $\iff$ Conmutatividad ordinaria.
  • $F_{inj}$-conmutativa $\iff$ Conmutativa y Afín.
  • $F_{surj}$-conmutativa $\iff$ Conmutativa y Relevante.

2.4 La Estrategia de Construcción

La estrategia central consiste en encontrar una categoría verbal $W$ tal que:

1. $S$ sea $W$-operádica (definida usando reglas en $W$).
2. $T$ sea $W$-conmutativa (invariante bajo reglas en $W$).

Si la intersección del "conjunto superior" de la operadicidad de $S$ y el "conjunto inferior" de la conmutatividad de $T$ no está vacía, se puede construir una ley distributiva canónica. Si la intersección está vacía, los autores proponen el refinamiento $W$-operádico para modificar $S$.

3. Contribuciones Clave

3.1 Construcción de Ley Distributiva Canónica (Teorema 42)

El artículo presenta una construcción general de una ley distributiva $\delta: ST \to TS$ para:

• $S$: Una mónada $W$-operádica.
• $T$: Una mónada $W$-conmutativa.

La construcción es categórica y canónica, definida a través de la descripción de coextremo de la extensión de Kan izquierda utilizada para definir $S$.

• Compatibilidad: $\delta$ es compatible con la unidad y la multiplicación de $S$ y la unidad de $T$ incondicionalmente.
• Compatibilidad de Multiplicación: $\delta$ es compatible con la multiplicación de $T$ ($\mu_T$) si se cumple cualquiera de las siguientes:
  1. $T$ es conmutativa (sentido ordinario), o
  2. $S$ es generada por operaciones de aridad $\le 1$ (por ejemplo, $W = F_{id}$).

3.2 Refinamiento $W$-Operádico (Sección 6)

Cuando una mónada $S$ falla en ser $W$-operádica para una $W$ requerida, los autores introducen el refinamiento $W$-operádico, denotado $Rf_W(S)$.

• Definición: $Rf_W(S) = \text{Mnd}(W\text{-Opd}(S))$, donde $W\text{-Opd}(S)$ es la $W$-operada inducida al restringir $S$ a $W$.
• Propiedad: Esta es una construcción universal (un comónada en la categoría de mónadas) que fuerza a $S$ a convertirse en $W$-operádica eliminando axiomas equacionales que violan las reglas estructurales de $W$.
• Significado: Proporciona un mecanismo formal e independiente de la presentación para el enfoque de "refinamiento" utilizado anteriormente de manera ad hoc.

3.3 Unificación de Resultados Conocidos

El marco unifica varios resultados específicos de la literatura (por ejemplo, [11, 51, 52, 30, 32, 20]) bajo una única teoría operádica. Aclara por qué ciertas combinaciones de efectos (como probabilidad y no determinismo) fallan y cómo pueden corregirse refinando la mónada fuente.

4. Resultados y Aplicaciones

4.1 Resolución de la Mónada de Valoración Indexada

El artículo revisa la mónada de valoración indexada $IV$ introducida por Varacca y Winskel [68] para modelar la combinación de probabilidad y no determinismo.

• Problema: La mónada de valoración estándar $V$ y la mónada del conjunto potencia finito no vacío $P^+_{fin}$ no admiten una ley distributiva.
• Resultado: Los autores demuestran que $IV$ es isomorfa al refinamiento $F_{inj}$-operádico de $V$ ($Rf_{F_{inj}}(V)$).
• Implicación: La ley distributiva $IV P^+_{fin} \to P^+_{fin} IV$ construida en [68] es exactamente la ley distributiva canónica proporcionada por el Teorema 42 cuando $S = Rf_{F_{inj}}(V)$ y $T = P^+_{fin}$.

4.2 Nuevas Leyes Distributivas

El marco genera nuevas leyes distributivas forzando la $W$-operadicidad:

• Ejemplo 50: Una ley distributiva entre la mónada de valoración indexada $IV$ y la mónada de distribuciones de probabilidad $D$ ($IV D \to DIV$). Esto resuelve un mal comportamiento categórico en una familia de morfismos $\lambda: DD \to DD$ utilizada en [67] para la semántica de MDP.
• Ejemplo 66: Una ley distributiva entre la mónada de conjunto potencia finito refinada y una mónada de escritor, modelando procesos donde los efectos secundarios se acumulan independientemente de si la salida se utiliza.

4.3 Detección de "No-Go"

El marco proporciona una manera sistemática de detectar la posible no existencia de leyes distributivas. Si la intersección de la operadicidad de $S$ y la conmutatividad de $T$ está vacía para todas las $W$ relevantes, la construcción canónica falla. Aunque esto no prueba un teorema de "no-go" (podrían existir leyes no canónicas), sirve como una sólida "bandera roja" (por ejemplo, para el par $(D, P_{fin})$).

5. Significado y Afirmaciones

El artículo afirma proporcionar una imagen categórica unificadora para la interacción entre reglas estructurales y leyes distributivas.

• Uniformidad: Avanza más allá de ejemplos específicos hacia una teoría parametrizada por categorías verbales, haciendo explícito y uniforme el papel del intercambio, el debilitamiento y la contracción.
• Independencia de la Presentación: A diferencia de los enfoques de refinamiento anteriores que dependían de presentaciones equacionales específicas, el refinamiento $W$-operádico es una construcción universal independiente de cómo se presenta la mónada.
• Fundamento Operádico: Establece que la existencia de leyes distributivas está fundamentalmente ligada a la naturaleza operádica de la mónada fuente y a las propiedades de conmutatividad de la mónada objetivo en relación con el mismo contexto estructural.

Los autores señalan que, aunque la teoría se desarrolla para mónadas sobre $\mathbf{Set}$, la extensión a otras categorías base y la acomodación de enfoques de "modificar $T$" son direcciones futuras naturales. La teoría se presenta como un paso fundamental hacia la comprensión de la combinación de efectos en la semántica de programas y la verificación de modelos.