A Fibrational Perspective on Differential Linear Logic

Enunciado del Problema
La Lógica Lineal Diferencial (DiLL) extiende la Lógica Lineal (LL) con reglas para la diferenciación (cocontracción, coweakening, coderrestricción), capturando la diferenciación de orden superior mediante simetrías entre fórmulas lineales y no lineales. Aunque DiLL ha establecido modelos categóricos (Categorías de Seely Diferenciales) y conexiones con Categorías Diferenciales Cartesianas (CDC), sigue siendo una teoría tipada simplemente. Esto presenta una brecha conceptual: en geometría diferencial, el diferencial de una función suave $f: M \to N$ es una función dependiente $D_x(f): TM_x \multimap TN_{f(x)}$, donde el espacio tangente $TM_x$ depende del punto $x$. El artículo pregunta si existe una versión dependiente de DiLL y cómo pueden expresarse sus modelos para acomodar esta dependencia entre tipos lineales (espacios vectoriales) y tipos no lineales (variedades).

Metodología
El autor emplea el marco de fibraciones de Grothendieck para modelar la dependencia, adaptando métodos de la semántica categórica de la teoría de tipos dependientes al contexto de las adjunciones Lineal-No Lineal (LNL).

1. Fibración Simple Lineal: Partiendo de una adjunción LNL entre una categoría cartesiana $\mathcal{C}$ (no lineal) y una categoría monoidal simétrica $\mathcal{L}$ (lineal), el artículo construye una "categoría simple lineal" $LS(\mathcal{C})$. Esta categoría sirve como el equivalente en lógica lineal de la categoría simple para teorías tipadas simplemente. Los objetos son pares $(X, A)$ donde $X \in \mathcal{C}$ y $A \in \mathcal{L}$, representando un contexto donde un tipo lineal $A$ depende de un contexto no lineal $X$.
2. Adjunciones Fibradas: El artículo demuestra que la adjunción LNL original se eleva a una adjunción fibrada entre la fibración simple de $\mathcal{C}$ y la fibración simple lineal $LS(\mathcal{C})$.
3. Functor Tangente Lineal: Para introducir la diferenciación, el artículo define un "functor tangente lineal" $T: \mathcal{C} \to LS(\mathcal{C})$. Se requiere que este functor sea una sección que preserve productos de la fibración, satisfaciendo axiomas específicos respecto al haz tangente de objetos no lineales y la linealidad parcial de los morfismos.
4. Categorías de Seely Diferenciales Generalizadas (GDSC): Al equipar una adjunción LNL con este functor tangente lineal, el artículo define una GDSC.

Contribuciones Clave

• Fibración Simple Lineal: La construcción de $LS(\mathcal{C})$ a partir de cualquier adjunción LNL, proporcionando una semántica fibrada para la lógica lineal que refleja la estructura de las teorías de tipos dependientes.
• Adjunciones LNL Fibradas: Demostrar que cualquier adjunción LNL induce una adjunción fibrada entre la categoría simple de la base y la categoría simple lineal, preservando la estructura lógica fibra a fibra.
• Categorías de Seely Diferenciales Generalizadas (GDSC): Definir las GDSCs como adjunciones LNL aditivas equipadas con un functor tangente lineal que satisface tres axiomas:
  • $T$ es una sección que preserva productos.
  • $T(U(A)) = (U(A), A)$ (el haz tangente de un objeto espacio vectorial es el objeto mismo).
  • Una "Regla de Linealidad Parcial" que asegura que el functor tangente interactúe correctamente con el debilitamiento y los morfismos lineales parciales.
• Equivalencia de Modelos: Demostrar que en cualquier GDSC, cada fibra de la fibración simple lineal es una Categoría de Seely Diferencial (DSC). Recíprocamente, cualquier DSC induce una GDSC. Esto establece que el enfoque fibrado generaliza los modelos existentes.
• Conexión con GCDCs Generalizadas: El artículo investiga la relación entre las GDSCs y las Categorías Diferenciales Cartesianas Generalizadas (GCDCs). Muestra que la categoría de Kleisli de una DSC es una CDC y que el endofunctor inducido por el functor tangente en una GDSC satisface la mayoría de los axiomas de una GCDC, aunque la regla de intercambio (GCDC.7) para todos los morfismos sigue siendo una pregunta abierta.

Resultados

• El artículo establece que la semántica de DiLL puede extenderse desde las categorías de Seely a cualquier adjunción LNL aditiva con biproducciones, siempre que exista un functor tangente lineal.
• Se demuestra que las fibras de la fibración simple lineal en una GDSC son ellas mismas DSCs, lo que significa que la estructura fibrada recupera los modelos estándar de DiLL localmente mientras proporciona una estructura dependiente global.
• La construcción recupera la transformación derivada estándar $\partial$ en cada fibra, satisfaciendo las reglas de constante, Leibniz, lineal, cadena e intercambio de DiLL.
• El trabajo vincula la perspectiva fibrada con el panorama más amplio de las categorías de diferenciación, posicionando a las GDSCs como una generalización que se sitúa entre las DSCs y la teoría emergente de las categorías tangentes fibradas.

Significado y Afirmaciones
El artículo afirma que este trabajo es un "primer paso" hacia la unificación de la Lógica Lineal Diferencial y los tipos dependientes. Al expresar los modelos de DiLL como un par de fibraciones de Grothendieck equipadas con un functor tangente, el autor proporciona un marco categórico capaz de manejar la dependencia de los tipos lineales sobre contextos no lineales, lo cual es intrínseco a la geometría diferencial pero está ausente en la DiLL estándar.

El significado radica en:

1. Unificación: Ofrecer un camino para modelar DiLL dependiente, potencialmente permitiendo la expresión de tipos como $\Pi_{x:M} (TM_x \multimap TN_{f(x)})$.
2. Generalización: Extender el alcance semántico de DiLL más allá de las categorías de Seely hacia cualquier adjunción LNL aditiva, abriendo la búsqueda de nuevos modelos surgidos de categorías tangentes.
3. Puente Fundacional: Conectar la semántica categórica de la diferenciación (DSC, CDC) con la semántica de la dependencia (fibraciones, categorías de comprensión), sugiriendo que las categorías tangentes pueden servir como la generalización dependiente natural de las GCDCs y modelos para DiLL dependiente.

El autor permanece modesto, señalando que, aunque la construcción fibrada funciona para el caso específico de fibraciones simples sobre adjunciones LNL, el objetivo último es encontrar estructuras en modelos generales de LL dependiente (como los descritos por Vákár y Lundfall) que satisfagan estas condiciones. El artículo no afirma haber construido completamente una teoría de tipos DiLL dependiente, sino haber proporcionado la infraestructura categórica necesaria (GDSCs) para apoyar dicho desarrollo.