Itegories

Resumen Técnico de "Itegories"

Planteamiento del Problema
El artículo aborda la formulación categórica de la iteración, específicamente dentro del contexto de las categorías de restricción, que proporcionan los fundamentos para la teoría de la parcialidad. Mientras que la interpretación categórica estándar de la iteración depende de operadores de traza definidos sobre coproductos (específicamente en categorías monoidales coCartesianas trazadas), este enfoque requiere la presencia de coproductos. Los autores señalan que los operadores de vara de Kleene (Kleene wand operators) fueron introducidos previamente en [13] para capturar la iteración en categorías de restricción derivadas de la teoría de la complejidad, pero estos solo se definieron brevemente para categorías de restricción extensivas distributivas utilizando la relación de interferencia máxima. Además, no se proporcionó una prueba completa que estableciera la equivalencia entre las varas de Kleene y los operadores de traza. El problema central es desarrollar una teoría robusta de las varas de Kleene que funcione en entornos sin coproductos y establecer rigurosamente su equivalencia con la iteración parametrizada y los operadores de traza en categorías de restricción extensivas.

Metodología
Los autores desarrollan la teoría a través de una serie de definiciones estructurales y construcciones categóricas:

1. Relaciones de Interferencia: El artículo introduce el concepto de una relación de interferencia ($\perp$) en una categoría de restricción con ceros de restricción. Esta relación formaliza cuándo dos mapas son "disjuntos" (es decir, donde uno está definido, el otro no lo está). Los autores distinguen entre la relación de interferencia máxima ($\perp_0$, donde la disjuntidad se define por $fg=0$) y otras relaciones, señalando que una categoría de restricción de interferencia es un par $(\mathcal{X}, \perp)$.
2. Uniones Disjuntas: Se adapta el concepto de $\perp$-uniones (uniones de mapas $\perp$-disjuntos). Los autores definen uniones "fuertes", que preservan la disjuntidad, y muestran cómo cualquier categoría de restricción de interferencia puede ser embebida en una de tipo "disjunto" mediante una construcción $DJ[(\mathcal{X}, \perp)]$.
3. Varas de Kleene: Una vara de Kleene ($\star|$) se define como un operador binario en una categoría de restricción de interferencia que toma un mapa $f: X \to X$ y un mapa disjunto $g: X \to A$ y produce un mapa $f \star| g: X \to A$. Esto se interpreta como iterar $f$ hasta que la "guarda" $g$ se satisfaga. Los axiomas para las varas de Kleene se presentan como análogos a los axiomas de los operadores de iteración, pero formulados sin coproductos.
4. Categorías de Restricción Extensivas: El artículo revisa las categorías de restricción extensivas, que poseen coproductos de restricción y "decisiones" (mapas que separan el dominio de definición de un mapa en partes que aterrizan en diferentes componentes del coproducto). Los autores definen una relación de interferencia canónica ($\perp_d$) en estas categorías inducida por las decisiones.
5. Entorno Clásico: En presencia de complementos relativos (categorías de restricción clásicas), los autores muestran que las varas de Kleene están completamente determinadas por su acción sobre los endomorfismos, lo que conduce a la definición de una "super-estrella de Kleene" (Kleene upper-star).
6. Construcción de Matrices: Se introduce una construcción de matriz $MAT[(\mathcal{X}, \perp)]$, que embe la una categoría de restricción de interferencia finitamente disjunta en una categoría de restricción extensiva.

Contribuciones Clave y Resultados

• Definición de Itegories: Los autores definen una itegory como una categoría de restricción de interferencia con uniones disjuntas binarias y una vara de Kleene.
• Equivalencia en Categorías de Restricción Extensivas: El resultado principal (Teorema 9.11) establece una correspondencia biyectiva entre los operadores de iteración parametrizados (y equivalentemente, los operadores de traza) en una categoría de restricción extensiva y las varas de Kleene definidas con respecto a la relación de interferencia canónica inducida por decisiones ($\perp_d$). Esto demuestra que, para las categorías de restricción extensivas, ser "trazada" es equivalente a ser una "itegory".
• Construcción Canónica: En entornos con uniones disjuntas contables, los autores demuestran la existencia de una vara de Kleene fuertemente inductiva canónica definida por la unión disjunta de todas las iteraciones ($f \star| g = \bigsqcup_{n \in \mathbb{N}} f^n g$).
• Equivalencia Clásica: Para las categorías de restricción de interferencia clásicas (aquellas con complementos relativos), el artículo demuestra una correspondencia biyectiva entre las varas de Kleene y las super-estrellas de Kleene (Teorema 6.9), mostrando que en este entorno el operador de iteración está totalmente determinado por su comportamiento sobre los endomorfismos.
• Representación Matricial de las Trazas: El artículo proporciona un cálculo de matrices para las categorías de restricción extensivas. Demuestra que computar la traza de una matriz arbitraria de $n+m \times n+p$ en una categoría de restricción extensiva trazada se reduce a computar trazas de matrices de $2 \times 2$.
• Teoremas de Embebimiento: Los autores muestran que aplicar la construcción de matriz a una itegory produce una categoría de restricción extensiva trazada (Proposición 9.15). Además, cualquier categoría de restricción con ceros de restricción puede ser embebida en una categoría de restricción extensiva trazada mediante la composición de la construcción de unión disjunta y la construcción de matriz (Corolario 9.18).

Significado
El artículo afirma que las varas de Kleene proporcionan una noción de iteración más general que no requiere la existencia de coproductos, lo que las hace aplicables a una clase más amplia de categorías de restricción que los operadores de traza tradicionales. Al establecer la equivalencia entre las varas de Kleene y los operadores de traza en las categorías de restricción extensivas, el trabajo unifica la traza de "estilo partícula" (iteración) con el marco de las categorías de restricción. La introducción de las relaciones de interferencia permite un tratamiento matizado de la disjuntidad que no se limita a la relación máxima, corrigiendo y generalizando las definiciones previas encontradas en [13]. Los resultados sugieren que las varas de Kleene pueden servir como un primitivo para interpretar constructos de programación imperativa (bucles) dentro de modelos categóricos de computabilidad, particularmente en contextos donde los coproductos están ausentes o donde una relación de interferencia específica (como la separabilidad recursiva) es más apropiada que la simple disjuntidad de dominios.