Non-Cartesian Guarded Recursion with Daggers

Resumen Técnico: Recursión guardada no cartesiana con dagas

Planteamiento del problema
La recursión guardada es un marco bien establecido para la formalización de flujos (streams) y tipos de datos recursivos en lenguajes de programación clásicos, típicamente modelados dentro de categorías cerradas cartesianas (CCC). Sin embargo, muchos paradigmas de computación significativos —específicamente la programación reversible, concurrente y cuántica— no admiten semántica en CCC. En su lugar, dependen de categorías equipadas con una daga (un operador involutivo sobre los morfismos), tales como las categorías inversas o las categorías de espacios de Hilbert. Si bien los tipos inductivos pueden modelarse en algunas categorías de dagas (por ejemplo, categorías inversas mediante el enriquecimiento en órdenes parciales dirigidos completos), la interpretación de la recursión sigue siendo un problema abierto o problemático en otras, particularmente en los espacios de Hilbert. El artículo aborda la brecha en proporcionar una semántica denotacional para la recursión guardada dentro del contexto de las categorías de dagas, con el objetivo de dar soporte a lenguajes de programación reversibles que requieren tanto reversibilidad como estructuras de datos recursivas.

Metodología
El autor propone una construcción categórica que adapta el enfoque de la "topos de árboles" (teoría de dominios guardados sintética) a entornos no cartesianos. La metodología procede en tres etapas principales:

1. La construcción guardada ($C^\infty$): Partiendo de una categoría arbitraria $C$ con un objeto terminal, el artículo construye una nueva categoría $C^\infty$ (isomorfa a $C^{\mathbb{N}^{op}}$). Los objetos en $C^\infty$ son secuencias de objetos en $C$ conectados por morfismos, asemejándose a los presheaves. Esta construcción introduce un functor "posterior" ($L$) y una transformación natural "siguiente" ($\nu$), que desplazan los componentes de la secuencia e insertan un objeto terminal, modelando efectivamente la modalidad de retardo requerida para la recursión guardada.
2. Enriquecimiento y puntos fijos: Se demuestra que la categoría $C^\infty$ está enriquecida sobre el topos de árboles ($S$). Este enriquecimiento permite la aplicación de teoremas de puntos fijos de la teoría de dominios guardados sintética. Específicamente, el artículo demuestra que los functores localmente contractivos en $C^\infty$ admiten puntos fijos únicos, permitiendo la interpretación de tipos inductivos guardados (por ejemplo, streams y listas) incluso cuando la categoría base $C$ no es cerrada cartesiana.
3. Integración con la estructura de rigor de daga: Para modelar la computación reversible, el artículo se centra en categorías de rigor de daga (categorías con una daga, producto tensorial $\otimes$ y tipo suma $\oplus$). El autor observa que, si bien la estructura de rigor (tensor y suma) se preserva por la construcción guardada, la estructura de la daga no se preserva automáticamente en $C^\infty$ porque la daga componente a componente de una transformación natural puede no producir un morfismo válido en la categoría construida. Para resolver esto, el artículo define una subcategoría refinada $C^\infty_e$ (usando epimorfismos de daga) y una subcategoría adicional $C^\infty_\dagger$ que contiene solo morfismos "dagables" (aquellos cuya daga puntual forma un morfismo válido en la categoría).

Contribuciones clave y resultados

• Modelo guardado no cartesiano: El artículo construye un modelo categórico para la recursión guardada partiendo de cualquier categoría con un objeto terminal, generalizando el enfoque del topos de árboles a entornos no cartesianos.
• Preservación de la estructura de rigor: Se prueba que, si la categoría base $C$ es una categoría de rigor de daga, la construcción guardada $C^\infty$ preserva la estructura de rigor (tipos tensor y suma), haciéndola adecuada para modelar tipos de datos como pares y listas.
• Subcategoría dagable: El artículo identifica que la construcción completa no soporta inherentemente una daga. Introduce la categoría $C^\infty_\dagger$, una subcategoría de la construcción guardada donde los morfismos admiten una daga. Se muestra que $C^\infty_\dagger$ es, en sí misma, una categoría de rigor de daga.
• Existencia de puntos fijos: El Teorema 3.12 establece que los functores localmente contractivos en $C^\infty$ admiten puntos fijos parametrizados. Este resultado se aplica a la subcategoría $C^\infty_\dagger$ para interpretar tipos inductivos guardados dentro de un entorno reversible.
• Semántica del emparejamiento de patrones simétrico guardado: El artículo aplica el modelo construido para interpretar el "emparejamiento de patrones simétrico guardado", un lenguaje de programación reversible de orden superior. La semántica cubre:
  • Tipos base (incluyendo tipos inductivos guardados como listas).
  • Funciones de primer orden (isos) definidas mediante uniones de funciones parciales reversibles.
  • Funciones de orden superior a través de un cálculo $\lambda$ guardado simplemente tipado enriquecido en $S$.
  • Ejemplos específicos incluyen una operación de control cuántico y una definición de orden superior de la Transformada de Fourier Cuántica (QFT) para listas de qubits.

Significancia y afirmaciones
El artículo afirma extender la utilidad de la recursión guardada más allá del procesamiento de flujos clásico hacia los paradigmas de programación reversible y cuántica. Al unir la semántica de la programación reversible (categorías de daga) con la recursión guardada (topos de árboles), el autor proporciona un modelo denotacional para lenguajes reversibles de orden superior que soportan tipos de datos infinitos.

El autor señala explícitamente que, si bien la construcción resuelve el problema de modelar tipos inductivos guardados en categorías de rigor de daga, no resuelve la cuestión abierta más amplia de si los espacios de Hilbert pueden interpretar la recursión general. En su lugar, el artículo ofrece un camino específico a través de la recursión guardada. La significancia radica en proporcionar una base categórica sólida para lenguajes reversibles con características como el emparejamiento de patrones simétrico y la recursión guardada, permitiendo la definición de algoritmos cuánticos complejos (como la QFT) en un formalismo de orden superior sin depender de descripciones de circuitos de bajo nivel. El artículo reconoce modestamente que la semántica de los streams en categorías de daga requiere una nueva teoría, ya que la construcción de límite estándar falla debido a la naturaleza de objeto cero de los objetos terminales en las categorías de daga.