Itegories

Resumo Técnico de "Itegories"

Problema
O artigo aborda a formulação categórica da iteração, especificamente no contexto de categorias de restrição, que fornecem os fundamentos para a teoria da parcialidade. Enquanto a interpretação categórica padrão da iteração depende de operadores de traço definidos em coprodutos (especificamente em categorias monoidais coCartesianas traçadas), essa abordagem requer a presença de coprodutos. Os autores observam que os operadores de varas de Kleene (Kleene wand operators) foram introduzidos anteriormente em [13] para capturar a iteração em categorias de restrição oriundas da teoria da complexidade, mas estes foram apenas brevemente definidos para categorias de restrição extensivas distributivas usando a relação de interferência máxima. Além disso, uma prova completa estabelecendo a equivalência entre varas de Kleene e operadores de traço não foi fornecida. O problema central é desenvolver uma teoria robusta de varas de Kleene que funcione em ambientes sem coprodutos e estabelecer rigorosamente sua equivalência com a iteração parametrizada e operadores de traço em categorias de restrição extensivas.

Metodologia
Os autores desenvolvem a teoria através de uma série de definições estruturais e construções categóricas:

1. Relações de Interferência: O artigo introduz o conceito de uma relação de interferência ($\perp$) em uma categoria de restrição com zeros de restrição. Esta relação formaliza quando dois mapas são "disjuntos" (ou seja, onde um é definido, o outro não é). Os autores distinguem entre a relação de interferência máxima ($\perp_0$, onde a disjunção é definida por $fg=0$) e outras relações, observando que uma categoria de restrição de interferência é um par $(\mathcal{X}, \perp)$.
2. Junções Disjuntas: O conceito de $\perp$-junções (junções de mapas $\perp$-disjuntos) é adaptado. Os autores definem junções "fortes", que preservam a disjunção, e mostram como qualquer categoria de restrição de interferência pode ser incorporada em uma categoria "disjunta" via uma construção $DJ[(\mathcal{X}, \perp)]$.
3. Varas de Kleene: Uma vara de Kleene ($\star|$) é definida como um operador binário em uma categoria de restrição de interferência que recebe um mapa $f: X \to X$ e um mapa disjunto $g: X \to A$ e produz um mapa $f \star| g: X \to A$. Isso é interpretado como iterar $f$ até que a "guarda" $g$ seja satisfeita. Os axiomas para varas de Kleene são apresentados como análogos aos axiomas de operadores de iteração, mas formulados sem coprodutos.
4. Categorias de Restrição Extensivas: O artigo revisa categorias de restrição extensivas, que possuem coprodutos de restrição e "decisões" (mapas que separam o domínio de definição de um mapa em partes que caem em diferentes componentes do coproduto). Os autores definem uma relação de interferência canônica ($\perp_d$) nestas categorias induzida por decisões.
5. Contexto Clássico: Na presença de complementos relativos (categorias de restrição clássicas), os autores mostram que as varas de Kleene são completamente determinadas por sua ação sobre endomorfismos, levando à definição de uma "upper-star de Kleene".
6. Construção de Matriz: Uma construção de matriz $MAT[(\mathcal{X}, \perp)]$ é introduzida, que incorpora uma categoria de restrição de interferência finitamente disjunta em uma categoria de restrição extensiva.

Principais Contribuições e Resultados

• Definição de Itegories: Os autores definem uma itegoria como uma categoria de restrição de interferência com junções disjuntas binárias e uma vara de Kleene.
• Equivalência em Categorias de Restrição Extensivas: O principal resultado (Teorema 9.11) estabelece uma correspondência bijetiva entre operadores de iteração parametrizada (e, equivalentemente, operadores de traço) em uma categoria de restrição extensiva e varas de Kleene definidas em relação à relação de interferência canônica induzida por decisão ($\perp_d$). Isso prova que, para categorias de restrição extensivas, ser "traçada" é equivalente a ser uma "itegoria".
• Construção Canônica: Em contextos com junções disjuntas contáveis, os autores demonstram a existência de uma vara de Kleene fortemente indutiva canônica definida pela junção disjunta de todas as iterações ($f \star| g = \bigsqcup_{n \in \mathbb{N}} f^n g$).
• Equivalência Clássica: Para categorias de restrição de interferência clássicas (aquelas com complementos relativos), o artigo prova uma correspondência bijetiva entre varas de Kleene e upper-stars de Kleene (Teorema 6.9), mostrando que, neste cenário, o operador de iteração é totalmente determinado pelo seu comportamento sobre endomorfismos.
• Representação Matricial de Traços: O artigo fornece um cálculo de matrizes para categorias de restrição extensivas. Ele demonstra que computar o traço de uma matriz arbitrária $n+m \times n+p$ em uma categoria de restrição extensiva traçada reduz-se a computar traços de matrizes $2 \times 2$.
• Teoremas de Incorporação: Os autores mostram que aplicar a construção de matriz a uma itegoria resulta em uma categoria de restrição extensiva traçada (Proposição 9.15). Além disso, qualquer categoria de restrição com zeros de restrição pode ser incorporada em uma categoria de restrição extensiva traçada via a composição da construção de junção disjunta e da construção de matriz (Corolário 9.18).

Significância
O artigo afirma que as varas de Kleene fornecem uma noção mais geral de iteração que não requer a existência de coprodutos, tornando-as aplicáveis a uma classe mais ampla de categorias de restrição do que os operadores de traço tradicionais. Ao estabelecer a equivalência entre varas de Kleene e operadores de traço em categorias de restrição extensivas, o trabalho unifica o traço de "estilo partícula" (iteração) com o arcabouço das categorias de restrição. A introdução de relações de interferência permite um tratamento matizado da disjunção que não se limita à relação máxima, corrigindo e generalizando definições anteriores encontradas em [13]. Os resultados sugerem que as varas de Kleene podem servir como um primitivo para interpretar construtos de programação imperativa (loops) dentro de modelos categóricos de computabilidade, particularmente em contextos onde coprodutos estão ausentes ou onde uma relação de interferência específica (como a separabilidade recursiva) é mais apropriada do que a simples disjunção de domínio.