💻 computer science

A Fibrational Perspective on Differential Linear Logic

Cet article propose une sémantique catégorielle pour la Logique Linéaire Différentielle en la modélisant comme une paire de fibrations de Grothendieck équipées d'un foncteur tangent, adaptant ainsi les méthodes de la théorie des types aux adjonctions linéaire-non-linéaire comme étape fondamentale vers l'unification de DiLL avec les types dépendants.

Auteurs originaux : Jad Koleilat

Publié 2026-05-12

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Jad Koleilat

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

La Vue d'Ensemble : Mélanger Deux Mondes Différents

Imaginez que vous essayez de construire une machine capable de faire deux choses très différentes en même temps :

Le Monde « Strict » (Logique Linéaire) : Dans ce monde, les ressources sont précieuses. Si vous avez une pomme, vous pouvez l'utiliser, mais une fois utilisée, elle est partie. Vous ne pouvez ni la copier ni la jeter. C'est comme un comptable strict où chaque centime doit être comptabilisé exactement une fois.
Le Monde « Flexible » (Types Dépendants) : Dans ce monde, les choses peuvent changer selon le contexte. Imaginez une carte où les routes que vous pouvez emprunter dépendent de l'endroit où vous vous tenez. Si vous êtes à Paris, la carte affiche les rues de Paris ; si vous êtes à Londres, elle affiche les rues de Londres. Les règles changent selon la situation.

Le Problème :
Le papier examine un système logique appelé Logique Linéaire Différentielle (DiLL). Ce système tente d'intégrer le calcul (la différentiation) dans la logique. Le calcul est naturellement « flexible » car la pente d'une courbe dépend exactement de l'endroit où vous vous trouvez sur cette courbe. Cependant, la DiLL standard est « stricte » (linéaire). Elle peine à exprimer l'idée que « la dérivée dépend du point spécifique que vous observez ».

L'auteur, Jad Koleilat, se demande : Pouvons-nous construire un modèle où les règles strictes de la logique peuvent gérer la nature flexible et changeante du calcul ?

La Solution : La « Fibration » (Le Faisceau de Cartes)

Pour résoudre ce problème, l'auteur utilise un outil mathématique appelé Fibration.

L'Analogie : L'Agence de Voyages et les Guides Touristiques
Imaginez une immense agence de voyages (la Catégorie de Base). Cette agence gère les principales destinations (comme « Paris » ou « Londres »).

Dans un modèle standard, l'agence se contente de lister les destinations.
Dans le modèle de ce papier, pour chaque destination, il existe un faisceau spécifique de guides touristiques (la Fibre) qui lui est attaché.
- Si la destination est « Paris », le faisceau contient des guides qui parlent français et connaissent les rues de Paris.
- Si la destination est « Londres », le faisceau contient des guides qui parlent anglais et connaissent les rues de Londres.

Cette structure est appelée une Fibration. Elle permet aux règles « strictes » de l'agence de voyages de fonctionner avec la réalité « flexible » selon laquelle chaque lieu possède ses propres règles spécifiques.

La « Catégorie Linéaire Simple » : Le Bus de Tourisme Spécialisé

L'auteur construit un type spécifique de Fibration appelé la Catégorie Linéaire Simple.

L'Analogie :
Imaginez un bus standard (Logique Linéaire) où les passagers (ressources) ne peuvent pas descendre ni se dupliquer.
Maintenant, imaginez un bus de tourisme spécialisé (La Catégorie Linéaire Simple).

Le bus a un Chauffeur (la partie non-linéaire, comme la destination « Paris »). Le chauffeur peut être copié, ignoré ou changé librement.
Le bus a des Passagers (la partie linéaire, comme la « pomme »). Ils doivent rester dans le bus et ne peuvent pas être dupliqués.
La magie réside dans le fait que l'itinéraire que le bus emprunte (la logique) dépend de l'endroit où le chauffeur se rend.

Cette structure permet à l'auteur de mélanger les passagers « stricts » avec les destinations « flexibles ».

Le « Foncteur Tangent Linéaire » : Le Moteur Différentiel

Le cœur du papier consiste à introduire un nouveau moteur dans ce système de bus, appelé le Foncteur Tangent Linéaire.

L'Analogie : Le Compteur de Vitesse et la Carte
En calcul, pour trouver la vitesse (dérivée) d'une voiture, vous avez besoin de deux choses :

La position actuelle de la voiture (le point sur la carte).
La direction et la vitesse à laquelle elle se déplace (le vecteur tangent).

Dans le modèle de l'auteur :

La Catégorie de Base est la carte de toutes les positions possibles.
La Catégorie Linéaire Simple est la collection de tous les couples possibles « position + vitesse ».
Le Foncteur Tangent Linéaire est la machine qui prend une « position » et génère automatiquement le couple correspondant « position + vitesse ».

L'auteur définit trois règles (axiomes) pour cette machine afin de s'assurer qu'elle se comporte comme le vrai calcul :

Préservation : Si vous combinez deux positions, la machine combine correctement leurs paires de vitesses.
Identité : Si vous avez un « espace vectoriel pur » (comme une ligne droite), la machine sait exactement comment le transformer en une paire position-vitesse.
Linéarité Partielle : C'est la règle la plus complexe. Elle garantit que si vous avez une fonction qui est « linéaire » dans une partie (comme la vitesse) mais « flexible » dans une autre (comme la position), la machine peut calculer le changement correctement. C'est comme s'assurer que si vous changez légèrement la position, le calcul de la vitesse se met à jour de manière fluide sans briser les règles strictes des passagers dans le bus.

Qu'Ont-ils Démontré ?

Le papier démontre deux choses principales :

Mise à Niveau des Anciens Modèles : Si vous prenez un modèle existant et plus simple de DiLL (appelé Catégorie de Seely Différentielle) et que vous l'intégrez dans cette nouvelle structure de « Fibration », il fonctionne toujours parfaitement. La nouvelle structure est une généralisation, ce qui signifie qu'elle couvre tous les anciens cas et davantage.
Création de Nouveaux Modèles : Chaque « tranche » (ou destination spécifique) de cette nouvelle structure agit comme un modèle parfait de Logique Linéaire Différentielle. Cela signifie que l'auteur a réussi à créer un cadre où les règles strictes de la logique peuvent gérer la nature changeante et dépendante du calcul.

Le « Et Alors ? » (Sans Spéculation)

Le papier affirme que ceci est une première étape vers l'unification de deux domaines majeurs :

Logique Linéaire Différentielle (DiLL) : Logique qui gère le calcul.
Types Dépendants : Logique où les types dépendent des valeurs (comme « une liste de 5 éléments » vs « une liste de 10 éléments »).

En utilisant cette approche de « Fibration » (le faisceau de cartes), l'auteur montre qu'il est possible d'exprimer la dérivée d'une fonction comme une fonction dépendante. En termes simples, ils ont construit un « conteneur » logique capable de contenir l'idée que « la dérivée d'une fonction change selon le point que vous observez », quelque chose que les modèles logiques précédents peinaient à faire formellement.

Le papier ne prétend pas résoudre des problèmes de physique réels ni créer de nouveaux logiciels pour l'instant ; c'est purement une construction théorique pour voir si ces deux mondes mathématiques complexes peuvent s'assembler dans un cadre unique et cohérent.

Énoncé du problème
La Logique Linéaire Différentielle (LLD) étend la Logique Linéaire (LL) par des règles de différentiation (cocontraction, coweakening, codereliction), capturant la différentiation d'ordre supérieur via des symétries entre formules linéaires et non linéaires. Bien que la LLD dispose de modèles catégoriels établis (Catégories de Seely Différentielles) et de liens avec les Catégories Différentielles Cartésiennes (CDC), elle reste une théorie simplement typée. Cela présente un écart conceptuel : en géométrie différentielle, le différentiel d'une fonction lisse $f: M \to N$ est une fonction dépendante $D_x(f): TM_x \multimap TN_{f(x)}$ , où l'espace tangent $TM_x$ dépend du point $x$ . L'article s'interroge sur l'existence d'une version dépendante de la LLD et sur la manière dont ses modèles peuvent être exprimés pour accommoder cette dépendance entre types linéaires (espaces vectoriels) et types non linéaires (variétés).

Méthodologie
L'auteur emploie le cadre des fibrations de Grothendieck pour modéliser la dépendance, adaptant des méthodes issues de la sémantique catégorielle des théories des types dépendants au contexte des adjonctions Linéaire-Non-Linéaire (LNL).

Fibration Linéaire Simple : À partir d'une adjonction LNL entre une catégorie cartésienne $\mathcal{C}$ (non linéaire) et une catégorie monoïdale symétrique $\mathcal{L}$ (linéaire), l'article construit une « catégorie linéaire simple » $LS(\mathcal{C})$ . Cette catégorie sert d'équivalent en logique linéaire de la catégorie simple pour les théories simplement typées. Les objets sont des paires $(X, A)$ où $X \in \mathcal{C}$ et $A \in \mathcal{L}$ , représentant un contexte où un type linéaire $A$ dépend d'un contexte non linéaire $X$ .
Adjonctions Fibrées : L'article démontre que l'adjonction LNL originale se relève en une adjonction fibrée entre la fibration simple de $\mathcal{C}$ et la fibration linéaire simple $LS(\mathcal{C})$ .
Foncteur Tangent Linéaire : Pour introduire la différentiation, l'article définit un « foncteur tangent linéaire » $T: \mathcal{C} \to LS(\mathcal{C})$ . Ce foncteur doit être une section préservant les produits de la fibration, satisfaisant des axiomes spécifiques concernant le fibré tangent des objets non linéaires et la linéarité partielle des applications.
Catégories de Seely Différentielles Généralisées (GDSC) : En équipant une adjonction LNL de ce foncteur tangent linéaire, l'article définit une GDSC.

Contributions Clés

Fibration Linéaire Simple : La construction de $LS(\mathcal{C})$ à partir de n'importe quelle adjonction LNL, fournissant une sémantique fibrée pour la logique linéaire qui reflète la structure des théories des types dépendants.
Adjonctions LNL Fibrées : La preuve que toute adjonction LNL induit une adjonction fibrée entre la catégorie simple de la base et la catégorie linéaire simple, préservant la structure logique fibre par fibre.
Catégories de Seely Différentielles Généralisées (GDSC) : La définition des GDSC comme des adjonctions LNL additives équipées d'un foncteur tangent linéaire satisfaisant trois axiomes :
- $T$ est une section préservant les produits.
- $T(U(A)) = (U(A), A)$ (le fibré tangent d'un objet espace vectoriel est l'objet lui-même).
- Une « Règle de Linéarité Partielle » assurant que le foncteur tangent interagit correctement avec l'affaiblissement et les applications linéaires partielles.
Équivalence des Modèles : La preuve que dans toute GDSC, chaque fibre de la fibration linéaire simple est une Catégorie de Seely Différentielle (DSC). Inversement, toute DSC induit une GDSC. Cela établit que l'approche fibrée généralise les modèles existants.
Lien avec les GCDC Généralisés : L'article examine la relation entre les GDSC et les Catégories Différentielles Cartésiennes Généralisées (GCDC). Il montre que la catégorie de Kleisli d'une DSC est une CDC et que le foncteur endo-induit par le foncteur tangent dans une GDSC satisfait la plupart des axiomes d'une GCDC, bien que la règle d'interchange (GCDC.7) pour tous les morphismes reste une question ouverte.

Résultats

L'article établit que la sémantique de la LLD peut être étendue des catégories de Seely à toute adjonction LNL additive avec biproduits, à condition qu'un foncteur tangent linéaire existe.
Il est prouvé que les fibres de la fibration linéaire simple dans une GDSC sont elles-mêmes des DSC, ce qui signifie que la structure fibrée retrouve localement les modèles standards de la LLD tout en fournissant une structure dépendante globale.
La construction retrouve la transformation de dérivation standard $\partial$ dans chaque fibre, satisfaisant les règles de constante, de Leibniz, de linéarité, de chaîne et d'interchange de la LLD.
Le travail relie la perspective fibrée au paysage plus large des catégories de différentiation, positionnant les GDSC comme une généralisation située entre les DSC et la théorie émergente des catégories tangentes fibrées.

Portée et Affirmations
L'article affirme que ce travail est un « premier pas » vers l'unification de la Logique Linéaire Différentielle et des types dépendants. En exprimant les modèles de LLD comme une paire de fibrations de Grothendieck équipées d'un foncteur tangent, l'auteur fournit un cadre catégoriel capable de gérer la dépendance des types linéaires vis-à-vis des contextes non linéaires, intrinsèque à la géométrie différentielle mais absente dans la LLD standard.

La portée réside dans :

Unification : Offrir une voie pour modéliser la LLD dépendante, permettant potentiellement l'expression de types tels que $\Pi_{x:M} (TM_x \multimap TN_{f(x)})$ .
Généralisation : Étendre le champ sémantique de la LLD au-delà des catégories de Seely vers toute adjonction LNL additive, ouvrant la recherche de nouveaux modèles issus des catégories tangentes.
Pont Fondamental : Relier la sémantique catégorielle de la différentiation (DSC, CDC) à la sémantique de la dépendance (fibrations, catégories de compréhension), suggérant que les catégories tangentes peuvent servir de généralisation dépendante naturelle des GCDC et de modèles pour la LLD dépendante.

L'auteur reste modeste, notant que bien que la construction fibrée fonctionne pour le cas spécifique des fibrations simples sur les adjonctions LNL, l'objectif ultime est de trouver des structures dans les modèles généraux de la LL dépendante (tels que ceux décrits par Vákár et Lundfall) qui satisfont ces conditions. L'article ne prétend pas avoir entièrement construit une théorie des types LLD dépendante, mais plutôt d'avoir fourni l'infrastructure catégorielle nécessaire (les GDSC) pour soutenir un tel développement.