A Fibrational Perspective on Differential Linear Logic

Enunciato del Problema
La Logica Lineare Differenziale (DiLL) estende la Logica Lineare (LL) con regole per la differenziazione (cocontrazione, coweakening, codereliction), catturando la differenziazione di ordine superiore tramite simmetrie tra formule lineari e non lineari. Sebbene la DiLL abbia modelli categoriali consolidati (Categorie Seely Differenziali) e connessioni con le Categorie Differenziali Cartesiane (CDC), essa rimane una teoria tipizzata semplicemente. Ciò presenta un divario concettuale: nella geometria differenziale, il differenziale di una funzione liscia $f: M \to N$ è una funzione dipendente $D_x(f): TM_x \multimap TN_{f(x)}$, dove lo spazio tangente $TM_x$ dipende dal punto $x$. Il lavoro si chiede se esista una versione dipendente della DiLL e come i suoi modelli possano essere espressi per accogliere questa dipendenza tra tipi lineari (spazi vettoriali) e tipi non lineari (varietà).

Metodologia
L'autore utilizza il quadro delle fibrature di Grothendieck per modellare la dipendenza, adattando metodi dalla semantica categoriale della teoria dei tipi dipendenti al contesto delle adjunzioni Lineare-Non Lineare (LNL).

1. Fibratura Semplice Lineare: Partendo da un'adjunzione LNL tra una categoria cartesiana $\mathcal{C}$ (non lineare) e una categoria monoidale simmetrica $\mathcal{L}$ (lineare), il lavoro costruisce una "categoria semplice lineare" $LS(\mathcal{C})$. Questa categoria funge da equivalente logico lineare della categoria semplice per le teorie tipizzate semplicemente. Gli oggetti sono coppie $(X, A)$ dove $X \in \mathcal{C}$ e $A \in \mathcal{L}$, rappresentando un contesto in cui un tipo lineare $A$ dipende da un contesto non lineare $X$.
2. Adjunzioni Fibrate: Il lavoro dimostra che l'adjunzione LNL originale si solleva a un'adjunzione fibrata tra la fibratura semplice di $\mathcal{C}$ e la fibratura semplice lineare $LS(\mathcal{C})$.
3. Funtore Tangente Lineare: Per introdurre la differenziazione, il lavoro definisce un "funtore tangente lineare" $T: \mathcal{C} \to LS(\mathcal{C})$. Questo funtore deve essere una sezione che preserva i prodotti della fibratura, soddisfacendo assiomi specifici riguardanti il fibrato tangente degli oggetti non lineari e la parzialità lineare delle mappe.
4. Categorie Seely Differenziali Generalizzate (GDSC): Dotando un'adjunzione LNL di questo funtore tangente lineare, il lavoro definisce una GDSC.

Contributi Chiave

• Fibratura Semplice Lineare: La costruzione di $LS(\mathcal{C})$ da qualsiasi adjunzione LNL, fornendo una semantica fibrata per la logica lineare che rispecchia la struttura delle teorie dei tipi dipendenti.
• Adjunzioni LNL Fibrates: Dimostrando che qualsiasi adjunzione LNL induce un'adjunzione fibrata tra la categoria semplice della base e la categoria semplice lineare, preservando la struttura logica fibra per fibra.
• Categorie Seely Differenziali Generalizzate (GDSC): Definire le GDSC come adjunzioni LNL additive dotate di un funtore tangente lineare che soddisfa tre assiomi:
  • $T$ è una sezione che preserva i prodotti.
  • $T(U(A)) = (U(A), A)$ (il fibrato tangente di un oggetto spazio vettoriale è l'oggetto stesso).
  • Una "Regola di Parzialità Lineare" che garantisce che il funtore tangente interagisca correttamente con il weakening e le mappe lineari parziali.
• Equivalenza dei Modelli: Dimostrando che in qualsiasi GDSC, ogni fibra della fibratura semplice lineare è una Categoria Seely Differenziale (DSC). Viceversa, qualsiasi DSC induce una GDSC. Ciò stabilisce che l'approccio fibrato generalizza i modelli esistenti.
• Connessione con le GCDC Generalizzate: Il lavoro indaga la relazione tra GDSC e Categorie Differenziali Cartesiane Generalizzate (GCDC). Mostra che la categoria di Kleisli di una DSC è una CDC e che l'endofuntore indotto dal funtore tangente in una GDSC soddisfa la maggior parte degli assiomi di una GCDC, sebbene la regola di scambio (GCDC.7) per tutti i morfismi rimanga una questione aperta.

Risultati

• Il lavoro stabilisce che la semantica della DiLL può essere estesa dalle categorie Seely a qualsiasi adjunzione LNL additiva con biprodotti, a condizione che esista un funtore tangente lineare.
• È dimostrato che le fibre della fibratura semplice lineare in una GDSC sono esse stesse DSC, il che significa che la struttura fibrata recupera i modelli standard della DiLL localmente, fornendo al contempo una struttura dipendente globale.
• La costruzione recupera la trasformazione di derivazione standard $\partial$ in ogni fibra, soddisfacendo le regole della costante, di Leibniz, lineare, della catena e di scambio della DiLL.
• Il lavoro collega la prospettiva fibrata al panorama più ampio delle categorie di differenziazione, posizionando le GDSC come una generalizzazione che si colloca tra le DSC e la teoria emergente delle categorie tangenti fibrates.

Significato e Affermazioni
Il lavoro afferma che questo è un "primo passo" verso l'unificazione della Logica Lineare Differenziale e dei tipi dipendenti. Esprimendo i modelli DiLL come una coppia di fibrature di Grothendieck dotate di un funtore tangente, l'autore fornisce un quadro categoriale capace di gestire la dipendenza dei tipi lineari dai contesti non lineari, intrinseca alla geometria differenziale ma assente nella DiLL standard.

Il significato risiede in:

1. Unificazione: Offrire una via per modellare la DiLL dipendente, potenzialmente abilitando l'espressione di tipi come $\Pi_{x:M} (TM_x \multimap TN_{f(x)})$.
2. Generalizzazione: Estendere la portata semantica della DiLL oltre le categorie Seely fino a qualsiasi adjunzione LNL additiva, aprendo la ricerca di nuovi modelli derivanti dalle categorie tangenti.
3. Ponte Fondazionale: Collegare la semantica categoriale della differenziazione (DSC, CDC) con la semantica della dipendenza (fibrature, categorie di comprensione), suggerendo che le categorie tangenti possano servire come generalizzazione dipendente naturale delle GCDC e modelli per la DiLL dipendente.

L'autore rimane modesto, notando che mentre la costruzione fibrata funziona per il caso specifico delle fibrature semplici su adjunzioni LNL, l'obiettivo ultimo è trovare strutture nei modelli generali della LL dipendente (come quelli descritti da Vákár e Lundfall) che soddisfino queste condizioni. Il lavoro non afferma di aver costruito completamente una teoria dei tipi DiLL dipendente, ma piuttosto di aver fornito l'infrastruttura categoriale necessaria (GDSC) per supportare tale sviluppo.