A Fibrational Perspective on Differential Linear Logic

Enunciado do Problema
A Lógica Linear Diferencial (DiLL) estende a Lógica Linear (LL) com regras para diferenciação (cocontração, coenfraquecimento, codiferenciação), capturando diferenciação de ordem superior por meio de simetrias entre fórmulas lineares e não lineares. Embora a DiLL possua modelos categóricos estabelecidos (Categorias Seely Diferenciais) e conexões com Categorias Diferenciais Cartesianas (CDC), ela permanece uma teoria de tipos simples. Isso apresenta uma lacuna conceitual: na geometria diferencial, o diferencial de uma função suave $f: M \to N$ é uma função dependente $D_x(f): TM_x \multimap TN_{f(x)}$, onde o espaço tangente $TM_x$ depende do ponto $x$. O artigo questiona se uma versão dependente da DiLL existe e como seus modelos podem ser expressos para acomodar essa dependência entre tipos lineares (espaços vetoriais) e tipos não lineares (variedades).

Metodologia
O autor emprega o arcabouço das fibras de Grothendieck para modelar dependência, adaptando métodos da semântica categórica da teoria de tipos dependentes ao contexto das adjunções Linear-Não-Linear (LNL).

1. Fibrada Simples Linear: Partindo de uma adjunção LNL entre uma categoria cartesiana $\mathcal{C}$ (não linear) e uma categoria monoidal simétrica $\mathcal{L}$ (linear), o artigo constrói uma "categoria simples linear" $LS(\mathcal{C})$. Esta categoria serve como o equivalente da lógica linear para a categoria simples de teorias de tipos simples. Os objetos são pares $(X, A)$ onde $X \in \mathcal{C}$ e $A \in \mathcal{L}$, representando um contexto onde um tipo linear $A$ depende de um contexto não linear $X$.
2. Adjunções Fibradas: O artigo demonstra que a adjunção LNL original se eleva a uma adjunção fibrada entre a fibrada simples de $\mathcal{C}$ e a fibrada simples linear $LS(\mathcal{C})$.
3. Functor Tangente Linear: Para introduzir diferenciação, o artigo define um "functor tangente linear" $T: \mathcal{C} \to LS(\mathcal{C})$. Este functor é requerido para ser uma seção que preserva produtos da fibrada, satisfazendo axiomas específicos relativos ao fibrado tangente de objetos não lineares e à linearidade parcial de mapas.
4. Categorias Seely Diferenciais Generalizadas (GDSC): Ao equipar uma adjunção LNL com este functor tangente linear, o artigo define uma GDSC.

Contribuições Principais

• Fibrada Simples Linear: A construção de $LS(\mathcal{C})$ a partir de qualquer adjunção LNL, fornecendo uma semântica fibrada para a lógica linear que espelha a estrutura das teorias de tipos dependentes.
• Adjunções LNL Fibradas: Provar que qualquer adjunção LNL induz uma adjunção fibrada entre a categoria simples da base e a categoria simples linear, preservando a estrutura lógica fibra a fibra.
• Categorias Seely Diferenciais Generalizadas (GDSC): Definir GDSCs como adjunções LNL aditivas equipadas com um functor tangente linear que satisfaz três axiomas:
  • $T$ é uma seção que preserva produtos.
  • $T(U(A)) = (U(A), A)$ (o fibrado tangente de um objeto espaço vetorial é o próprio objeto).
  • Uma "Regra de Linearidade Parcial" garantindo que o functor tangente interaja corretamente com o enfraquecimento e mapas lineares parciais.
• Equivalência de Modelos: Provar que em qualquer GDSC, toda fibra da fibrada simples linear é uma Categoria Seely Diferencial (DSC). Inversamente, qualquer DSC induz uma GDSC. Isso estabelece que a abordagem fibrada generaliza os modelos existentes.
• Conexão com GCDCs Generalizadas: O artigo investiga a relação entre GDSCs e Categorias Diferenciais Cartesianas Generalizadas (GCDCs). Mostra-se que a categoria Kleisli de uma DSC é uma CDC e que o endofunctor induzido pelo functor tangente em uma GDSC satisfaz a maioria dos axiomas de uma GCDC, embora a regra de intercâmbio (GCDC.7) para todos os morfismos permaneça uma questão em aberto.

Resultados

• O artigo estabelece que a semântica da DiLL pode ser estendida de categorias Seely para qualquer adjunção LNL aditiva com biprodutos, desde que exista um functor tangente linear.
• É provado que as fibras da fibrada simples linear em uma GDSC são elas próprias DSCs, significando que a estrutura fibrada recupera os modelos padrão da DiLL localmente, enquanto fornece uma estrutura dependente global.
• A construção recupera a transformação derivada padrão $\partial$ em cada fibra, satisfazendo as regras de constante, Leibniz, linear, cadeia e intercâmbio da DiLL.
• O trabalho liga a perspectiva fibrada ao cenário mais amplo das categorias de diferenciação, posicionando as GDSCs como uma generalização que se situa entre as DSCs e a teoria emergente das categorias tangentes fibradas.

Significado e Alegações
O artigo alega que este trabalho é um "primeiro passo" rumo à unificação da Lógica Linear Diferencial e dos tipos dependentes. Ao expressar modelos de DiLL como um par de fibradas de Grothendieck equipadas com um functor tangente, o autor fornece um arcabouço categórico capaz de lidar com a dependência de tipos lineares em contextos não lineares, o que é intrínseco à geometria diferencial, mas ausente na DiLL padrão.

O significado reside em:

1. Unificação: Oferecer um caminho para modelar DiLL dependente, potencialmente permitindo a expressão de tipos como $\Pi_{x:M} (TM_x \multimap TN_{f(x)})$.
2. Generalização: Estender o escopo semântico da DiLL além das categorias Seely para qualquer adjunção LNL aditiva, abrindo a busca por novos modelos surgindo de categorias tangentes.
3. Ponte Fundacional: Conectar a semântica categórica da diferenciação (DSC, CDC) com a semântica da dependência (fibradas, categorias de compreensão), sugerindo que as categorias tangentes podem servir como a generalização dependente natural das GCDCs e modelos para DiLL dependente.

O autor permanece modesto, observando que, embora a construção fibrada funcione para o caso específico de fibradas simples sobre adjunções LNL, o objetivo final é encontrar estruturas em modelos gerais de LL dependente (como os descritos por Vákár e Lundfall) que satisfaçam essas condições. O artigo não alega ter construído completamente uma teoria de tipos DiLL dependente, mas sim ter fornecido a infraestrutura categórica necessária (GDSCs) para apoiar tal desenvolvimento.