Resumo Técnico: Monadas e Leis Distributivas em Contextos Subestruturais

1. Declaração do Problema

Na semântica de programas e na modelagem de sistemas, as monadas servem como uma interface uniforme para efeitos computacionais (por exemplo, não-determinismo, probabilidade, exceções). Um desafio central é combinar dois efeitos distintos modelados por monadas $S$ e $T$. Matematicamente, isso requer uma lei distributiva $\delta: ST \to TS$, que equipa o funtor composto $TS$ com uma estrutura de monada.

Embora muitas leis distributivas existam, teoremas de "não-existência" (por exemplo, a observação de Plotkin sobre a monada de probabilidade $D$ e a monada do conjunto das partes $P$) demonstram que leis distributivas nem sempre existem. Abordagens anteriores para este problema incluíram:

1. Leis distributivas fracas: Relaxar a compatibilidade com unidades, frequentemente modificando a monada alvo $T$.
2. Refinamento: Modificar a monada fonte $S$ removendo axiomas equacionais "problemáticos" que impedem a existência de $\delta$.

O problema específico abordado neste artigo é a falta de um framework unificado, categórico e independente de apresentação para a abordagem de "refinamento". Trabalhos anteriores identificaram o papel das regras estruturais (troca, enfraquecimento, contração) no fracasso ou sucesso de leis distributivas, mas essas observações foram específicas a contextos particulares em vez de formalizadas de maneira geral.

2. Metodologia

Os autores desenvolvem uma teoria categórica parametrizada por categorias verbais (introduzidas por Tronin), que modelam contextos subestruturais restringindo regras estruturais em contextos de variáveis.

2.1 Categorias Verbais ($W$)

O framework utiliza categorias verbais, definidas como subcategorias amplas de $\mathcal{F}$ (a categoria dos ordinais finitos e funções) fechadas sob uma operação de "substituição verbal". Essas categorias correspondem a combinações específicas de regras estruturais:

• $F_{id}$: Nenhuma regra estrutural.
• $F_{bij}$: Apenas troca (simétrica).
• $F_{surj}$: Troca e contração.
• $F_{inj}$: Troca e enfraquecimento.
• $F$: Todas as regras estruturais.

2.2 Monadas $W$-Operádicas

O artigo introduz monadas $W$-operádicas. Uma monada $S$ é $W$-operádica se for induzida por uma $W$-operádia via uma extensão de Kan à esquerda ao longo da inclusão $J: W \to \mathbf{Set}$.

• Intuitivamente, uma $W$-operádia codifica uma teoria algébrica onde os termos estão sujeitos apenas às regras estruturais permitidas em $W$.
• Exemplos incluem:
  • Monadas $F_{id}$-operádicas correspondem a operádias não-simétricas (por exemplo, monada de listas).
  • Monadas $F_{bij}$-operádicas correspondem a operádias simétricas (por exemplo, monadas de multiconjuntos).
  • Monadas $F_{surj}$-operádicas correspondem a operádias regulares (por exemplo, monada de distribuições de probabilidade).

2.3 Monadas $W$-Comutativas

Para construir uma lei distributiva, a monada alvo $T$ deve satisfazer uma condição relativa a $W$. Os autores definem monadas $W$-comutativas usando uma estrutura monoidal lax derivada das forças únicas de $T$.

• Uma monada $T$ é $W$-comutativa se sua estrutura monoidal lax $\psi$ for compatível com os morfismos em $W$.
• Isso unifica propriedades conhecidas:
  • $F_{bij}$-comutativa $\iff$ Comutatividade ordinária.
  • $F_{inj}$-comutativa $\iff$ Comutativa e Afim.
  • $F_{surj}$-comutativa $\iff$ Comutativa e Relevante.

2.4 Estratégia de Construção

A estratégia central envolve encontrar uma categoria verbal $W$ tal que:

1. $S$ seja $W$-operádica (definida usando regras em $W$).
2. $T$ seja $W$-comutativa (invariante sob regras em $W$).

Se a interseção do "conjunto superior" da operadicidade de $S$ e do "conjunto inferior" da comutatividade de $T$ for não vazia, uma lei distributiva canônica pode ser construída. Se a interseção for vazia, os autores propõem o refinamento $W$-operádico para modificar $S$.

3. Contribuições Principais

3.1 Construção de Lei Distributiva Canônica (Teorema 42)

O artigo apresenta uma construção geral de uma lei distributiva $\delta: ST \to TS$ para:

• $S$: Uma monada $W$-operádica.
• $T$: Uma monada $W$-comutativa.

A construção é categórica e canônica, definida via a descrição de co-fim da extensão de Kan à esquerda usada para definir $S$.

• Compatibilidade: $\delta$ é compatível com a unidade e multiplicação de $S$ e a unidade de $T$ incondicionalmente.
• Compatibilidade de Multiplicação: $\delta$ é compatível com a multiplicação de $T$ ($\mu_T$) se:
  1. $T$ for comutativa (sentido ordinário), ou
  2. $S$ for gerada por operações de aridade $\le 1$ (por exemplo, $W = F_{id}$).

3.2 Refinamento $W$-Operádico (Seção 6)

Quando uma monada $S$ falha em ser $W$-operádica para uma $W$ requerida, os autores introduzem o refinamento $W$-operádico, denotado $Rf_W(S)$.

• Definição: $Rf_W(S) = \text{Mnd}(W\text{-Opd}(S))$, onde $W\text{-Opd}(S)$ é a $W$-operádia induzida restringindo $S$ a $W$.
• Propriedade: Esta é uma construção universal (um comonada na categoria de monadas) que força $S$ a tornar-se $W$-operádica ao descartar axiomas equacionais que violam as regras estruturais de $W$.
• Significado: Fornece um mecanismo formal e independente de apresentação para a abordagem de "refinamento" anteriormente usada ad-hoc.

3.3 Unificação de Resultados Conhecidos

O framework unifica vários resultados específicos da literatura (por exemplo, [11, 51, 52, 30, 32, 20]) sob uma única teoria operádica. Clarifica por que certas combinações de efeitos (como probabilidade e não-determinismo) falham e como podem ser corrigidas refinando a monada fonte.

4. Resultados e Aplicações

4.1 Resolução da Monada de Valoração Indexada

O artigo revisita a monada de valoração indexada $IV$ introduzida por Varacca e Winskel [68] para modelar a combinação de probabilidade e não-determinismo.

• Problema: A monada de valoração padrão $V$ e a monada do conjunto das partes finito não-vazio $P^+_{fin}$ não admitem uma lei distributiva.
• Resultado: Os autores provam que $IV$ é isomorfa ao refinamento $F_{inj}$-operádico de $V$ ($Rf_{F_{inj}}(V)$).
• Implicação: A lei distributiva $IV P^+_{fin} \to P^+_{fin} IV$ construída em [68] é exatamente a lei distributiva canônica fornecida pelo Teorema 42 quando $S = Rf_{F_{inj}}(V)$ e $T = P^+_{fin}$.

4.2 Novas Leis Distributivas

O framework gera novas leis distributivas forçando a $W$-operadicidade:

• Exemplo 50: Uma lei distributiva entre a monada de valoração indexada $IV$ e a monada de distribuição de probabilidade $D$ ($IV D \to DIV$). Isso resolve um mau comportamento categórico em uma família de morfismos $\lambda: DD \to DD$ usada em [67] para semântica de MDP.
• Exemplo 66: Uma lei distributiva entre a monada do conjunto das partes finito refinada e uma monada de escritor, modelando processos onde efeitos colaterais são acumulados independentemente de o resultado ser usado.

4.3 Detecção de "Não-Existência"

O framework fornece uma maneira sistemática de detectar a possível não-existência de leis distributivas. Se a interseção da operadicidade de $S$ e da comutatividade de $T$ for vazia para todas as $W$ relevantes, a construção canônica falha. Embora isso não prove um teorema de "não-existência" (leis não-canônicas podem existir), serve como um robusto "sinal de alerta" (por exemplo, para o par $(D, P_{fin})$).

5. Significado e Alegações

O artigo alega fornecer uma imagem categórica unificadora para a interação entre regras estruturais e leis distributivas.

• Uniformidade: Avança além de exemplos específicos para uma teoria parametrizada por categorias verbais, tornando o papel da troca, enfraquecimento e contração explícito e uniforme.
• Independência de Apresentação: Diferentemente de abordagens anteriores de refinamento que dependiam de apresentações equacionais específicas, o refinamento $W$-operádico é uma construção universal independente de como a monada é apresentada.
• Fundação Operádica: Estabelece que a existência de leis distributivas está fundamentalmente ligada à natureza operádica da monada fonte e às propriedades de comutatividade da monada alvo relativas ao mesmo contexto estrutural.

Os autores observam que, embora a teoria seja desenvolvida para monadas em $\mathbf{Set}$, a extensão para outras categorias base e o acomodo de abordagens de "modificar $T$" são direções futuras naturais. A teoria é apresentada como um passo fundamental para entender a combinação de efeitos na semântica de programas e verificação de modelos.