🔢 mathematics

Categorical E-Graphs for Lambda Calculi

Cet article étend le cadre catégorique des e-graphs aux catégories monoïdales symétriques fermées pour supporter nativement la liaison de variables dans le $\lambda$ -calcul, en introduisant une représentation par hypergraphe hiérarchique avec un mécanisme de réécriture par double poussée vers l'extérieur qui est prouvé équivalent à la réécriture de termes standard.

Auteurs originaux : Aleksei Tiurin, Dan R. Ghica, Nick Hu

Publié 2026-06-26

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Aleksei Tiurin, Dan R. Ghica, Nick Hu

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

Imaginez que vous essayez de résoudre un puzzle colossal, mais que chaque fois que vous déplacez une pièce, vous détruisez accidentellement les pièces que vous avez déjà placées. C'est le problème auquel les informaticiens sont confrontés lorsqu'ils tentent d'optimiser des programmes informatiques complexes. Ils utilisent un outil appelé e-graph (graphe d'égalité), qui est comme un classeur ultra-efficace. Au lieu de jeter les anciennes versions d'un programme lorsqu'ils en trouvent une meilleure, l'e-graph conserve toutes les versions dans le même classeur, en regroupant les pièces qui signifient la même chose. Cela permet à l'ordinateur d'explorer des millions de possibilités à la fois sans se perdre.

Cependant, il y a un piège : les e-graphs ont historiquement eu du mal avec les variables (comme le « x » dans les équations mathématiques). Dans un programme, une variable est comme une étiquette de nom qui peut être déplacée. Si vous déplacez l'étiquette, la signification du programme peut changer, ou deux programmes identiques peuvent paraître différents simplement parce que les étiquettes de nom ne sont pas aux mêmes endroits. Cela rend très difficile pour l'e-graph de réaliser qu'ils sont en fait les mêmes.

La Grande Idée : Du Texte aux Images

Les auteurs de cet article proposent une nouvelle façon de gérer ces étiquettes de noms de variables. Au lieu de traiter les programmes comme du texte (comme une phrase que l'on lit), ils les traitent comme des diagrammes de cordes (string diagrams) (comme une carte ou un organigramme).

L'Ancienne Méthode (Texte) : Imaginez écrire une recette. Si vous écrivez « Ajouter du sel » à l'étape 1 et « Ajouter du sel » à l'étape 5, l'ordinateur voit deux phrases distinctes. Même si elles signifient la même chose, l'ordinateur doit faire un travail supplémentaire pour réaliser qu'elles sont identiques.
La Nouvelle Méthode (Diagrammes de Cordes) : Imaginez la recette comme un organigramme physique où des fils connectent les ingrédients aux actions. Si vous avez deux étapes « Ajouter du sel », c'est littéralement le même fil physique connecté à deux endroits différents. Vous n'avez pas besoin de comparer le texte ; l'image montre qu'ils sont les mêmes.

La Solution de la « Boîte Magique »

Pour faire fonctionner cela avec les variables (qui peuvent être « liées » ou enfermées dans une partie spécifique du programme, comme une variable locale dans une fonction), les auteurs utilisent un concept issu des mathématiques avancées : la Théorie des Catégories.

Considérez un programme comme une machine avec des entrées et des sorties.

La Boîte : Ils représentent une fonction (comme une abstraction lambda, λx) sous la forme d'une boîte arrondie. La variable x est un fil qui entre dans la boîte.
Le Partage : Ils utilisent des boîtes en pointillés pour représenter des groupes de choses qui sont équivalentes. Si deux parties du programme sont mathématiquement égales, elles se trouvent à l'intérieur de la même boîte en pointillés.
Le Résultat : En combinant ces boîtes, ils créent une structure appelée E-hypergraphe fermé (Closed E-Hypergraph). C'est un nom sophistiqué pour un « plan de puzzle » qui sait automatiquement quand deux pièces sont les mêmes, même si elles sont enveloppées dans des boîtes différentes ou possèdent des noms de variables différents.

Comment ça marche : L'astuce du « Recâblage »

Dans les e-graphs traditionnels, pour modifier un programme, vous devez supprimer une ancienne pièce et en coller une nouvelle. C'est risqué et lent.

Dans ce nouveau système, changer le programme revient à recâbler un circuit imprimé.

Imaginez une « réduction bêta » (une règle fondamentale en programmation où l'on injecte une valeur dans une fonction) non pas comme la suppression de texte, mais simplement comme le fait de débrancher un fil d'une prise pour le brancher dans une autre.
Parce que la structure est construite sur ces diagrammes, l'ordinateur n'a pas besoin de se soucier du renommage des variables ou de vérifier si elles sont « capturées » (volées par le mauvais contexte). Les fils circulent naturellement.

Pourquoi cela importe (selon l'article)

Les auteurs ont testé cette idée en utilisant un type spécifique de logique de programmation appelé le calcul de substitution linéaire (une façon de gérer les instructions « let » et le partage dans le code).

Le Problème avec l'Ancienne Méthode : Pour gérer les instructions « let » (comme let x = 1 in...), les anciens e-graphs devaient ajouter des nœuds et des règles « bureaucratiques » spéciales juste pour gérer les noms. Cela encombrait le système et le ralentissait.
La Nouvelle Méthode : Dans leur système de diagrammes, les instructions « let » sont de simples connexations naturelles. Le système comprend automatiquement que let x = 1 in (x + x) est la même chose que let y = 1 in (y + y) sans avoir besoin de règles supplémentaires. Le « partage » est intégré dans la géométrie du diagramme.

L'Essentiel

L'article affirme avoir construit un nouveau fondement mathématique pour les e-graphs qui traite les programmes comme des cartes topologiques plutôt que comme du texte. En utilisant des « boîtes » pour cacher les variables et des « fils » pour les connecter, ils ont créé un système où :

L'équivalence est automatique : Si deux diagrammes sont topologiquement identiques, ils sont le même programme.
La réécriture est sûre : Vous pouvez modifier des parties du programme sans détruire le reste.
Les variables sont gérées naturellement : Fini le renommage désordonné ou les nœuds bureaucratiques complexes.

Les auteurs soutiennent que cette approche est particulièrement puissante pour les langages de programmation fonctionnelle (comme ceux basés sur le Lambda-Calcul), offrant une façon plus propre et plus efficace d'optimiser le code par rapport aux méthodes précédentes qui reposaient sur des e-graphs « à fentes » (qui traitent les variables comme des emplacements de données explicites). Ils fournissent la preuve mathématique que leur réécriture par diagrammes est tout aussi correcte que la réécriture textuelle traditionnelle, mais avec l'avantage supplémentaire de manipuler directement la « forme » du programme.

Résumé Technique : E-Graphes Catégoriques pour les Calculs Lambda

Énoncé du Problème

La saturation d'égalité est une technique puissante pour l'optimisation de programmes et le raisonnement, utilisant des classes d'équivalence de termes (e-graphs) pour explorer un espace de règles de réécriture de manière non destructive. Cependant, les e-graphs traditionnels manquent de support natif pour la liaison de variables (variable binding), une caractéristique fondamentale des langages de programmation fonctionnelle basés sur le $\lambda$ -calcul.

Les approches existantes pour intégrer la liaison font face à des défis significatifs :

Représentations Textuelles : Dans la syntaxe textuelle standard, les termes $\alpha$ -équivalents sont distincts et ne peuvent pas être partagés. Bien que les indices de De Bruijn identifient l' $\alpha$ -équivalence de manière syntaxique, les indices dépendent de la portée (scope) des variables, ce qui empêche le partage de termes qui diffèrent uniquement par l'assignation d'indices (ex: $\lambda f. f((\lambda x. fx)2)$ ).
Substitution Explicite : L'ajout de nœuds de substitution explicite (ex: $t[x/u]$ ) pour gérer la liaison introduit de la « bureaucratie ». Cela nécessite des nœuds et des règles de réécriture supplémentaires pour gérer les permutations de substitutions non-interagissantes (équivalence graphique), encombrant l'espace d'état avec une surcharge administrative plutôt qu'avec du réécriture spécifique au domaine.
E-Graphs à Emplacements (Slotted E-Graphs) : Des travaux récents (Schneider et al.) introduisent des « e-graphs à emplacements » où les variables sont des données de premier rang. Bien qu'efficace, cette approche repose sur des techniques nominales applicables à des langages arbitraires (comme le $\pi$ -calculus) mais peut ne pas exploiter les propriétés structurelles spécifiques du $\lambda$ -calcul aussi efficacement qu'un modèle sémantique dédié.

Le problème central est l'absence d'une structure de données catégorique native pour les e-graphs supportant la liaison de variables, permettant une saturation d'égalité efficace dans les $\lambda$ -calculs sans la surcharge des nœuds de substitution explicite ou des règles de renommage complexes.

Méthodologie

Les auteurs proposent une solution fondée sur la sémantique catégorique, étendant l'interprétation des e-graphs comme des diagrammes de cordes (string diagrams).

1. Cadre Catégorique

Le papier s'appuie sur les travaux de Tiurin et al., qui modélisent les e-graphs (sans liaison) comme des morphismes dans des catégories enrichies en semi-treillis monoïdaux symétriques (catégories SLat).

Enrichissement SLat : Les ensembles de morphismes (Hom-sets) sont des semi-treillis, où l'opération de jointure ( $+$ ) représente l'équivalence des sous-termes (classes de l'e-graph).
Structure Monoïdale Fermée : Pour gérer la liaison de variables, les auteurs étendent la catégorie pour qu'elle soit monoïdale fermée. Cela introduit l'objet hom interne ( $A \multimap B$ ) et l'adjonction $- \otimes B \dashv B \multimap -$ .
Diagrammes de Cordes : Les termes sont représentés par des diagrammes de cordes. La liaison est modélisée via des « boîtes arrondies » (représentant l'abstraction $\lambda$ ), et les classes d'équivalence sont modélées via des « boîtes en pointillés » (représentant la jointure de semi-treillis).

2. Représentation Combinatoire : E-Hypergraphes Fermés

Pour fournir une structure de données concrète, les auteurs définissent des e-hypergraphes fermés. Ce sont des hypergraphes hiérarchiques qui encodent :

Hyperarêtes : Représentant les opérations (générateurs).
Arêtes Hiérarchiques : Deux types de structures imbriquées :
- Classes-e (Boîtes en pointillés) : Représentant des classes d'équivalence de sous-termes.
- Boîtes d'Abstraction (Boîtes arrondies) : Représentant les abstractions $\lambda$ .
Interfaces : La structure utilise des cospans étendus pour gérer les entrées et sorties, distinguant les interfaces externes (haut niveau) des interfaces strictement internes (imbriquées dans les boîtes).

3. Système de Réécriture

Les auteurs définissent un système de réécriture Double-Pushout with Interfaces (DPOI) pour les e-hypergraphes fermés.

Règles de Réécriture : Définies comme des spans de cospans étendus.
Compléments de Bordure : Une définition spécialisée du « trou » laissé après le retrait d'une correspondance est introduite pour gérer la nature hiérarchique des graphes. Cela garantit que lorsqu'un sous-graphe est retiré, les interfaces internes sont correctement ajustées (ex: retirer un terme imbriqué met à jour l'interface strictement interne de son parent).
Correction et Complétude : Le papier établit que la réécriture DPO sur ces e-hypergraphes fermés est correcte et complète par rapport à la réécriture de termes $\Sigma^+$ -fermés modulo les équations des catégories monoïdales symétriques SLat et la loi de distributivité de la structure fermée.

Contributions Clés

Extension Catégorique : La construction d'une forme d'e-graphs supportant la liaison en étendant le domaine catégorique des catégories SLat monoïdales symétriques libres aux catégories SLat monoïdales symétriques fermées libres.
E-Hypergraphes Fermés : La définition d'une représentation combinatoire concrète (e-hypergraphes fermés) qui absorbe naturellement les équations de la structure monoïdale symétrique et de la structure fermée (liaison).
Réécriture DPOI pour la Liaison : La formulation d'un système de réécriture DPOI pour ces structures, prouvant sa correction et sa complétude par rapport à la réécriture de termes dans la théorie catégorique correspondante.
Comparaison avec les E-Graphs à Emplacements : Une comparaison théorique démontrant que si les e-graphs à emplacements offrent une liaison générique via des techniques nominales, l'approche catégorique intègre la liaison dans le langage interne du modèle, offrant potentiellement des avantages pour les optimisations spécifiques au $\lambda$ -calcul.

Résultats

Équivalence de Réécriture : Le papier prouve que la réécriture de termes $\Sigma^+$ -fermés est équivalente à la réécriture DPO des e-hypergraphes fermés.
Gestion de l'Équivalence Graphique : L'approche gère naturellement l'« équivalence graphique » (permutations de substitutions non-interagissantes) sans nécessiter de nœuds de substitution explicites. Dans le modèle catégorique, la substitution explicite est modélisée comme une composition, et les lois structurelles de la catégorie absorbent les équivalences nécessaires.
Étude de Cas ( $\lambda_{lsub}$ ) : Les auteurs appliquent la théorie au calcul de substitution linéaire ( $\lambda_{lsub}$ ). Ils démontrent que les termes avec des substitutions explicites (ex: let-bindings) peuvent être représentés directement comme des diagrammes de cordes.
- Contrairement aux e-graphs conventionnels qui nécessitent des nœuds explicites pour la substitution et des règles de réécriture pour gérer leur permutation, le modèle catégorique traite cela comme des propriétés structurelles du diagramme.
- Le papier montre que des programmes sémantiquement équivalents (ex: réordonner des let-bindings) sont mappés vers le même diagramme de cordes, permettant à la saturation d'égalité d'opérer sur une représentation normalisée.

Signification et Revendications

Le papier revendique fournir une sémantique catégorique fondamentale pour les e-graphs avec liaison, un domaine auparavant sous-développé.

Justification Théorique : Il offre une justification rigoureuse des congruences maintenues par les e-graphs avec liaison, en les ancrant dans les propriétés des catégories monoïdales symétriques fermées SLat.
Potentiel d'Efficacité : En absorbant les équations structurelles (comme l'associativité, la commutativité et les permutations de substitution) dans la syntaxe graphique et la catégorie sous-jacente, l'approche vise à réduire la « bureaucratie » dans l'espace d'état de la saturation d'égalité. Cela contraste avec les approches traitant ces éléments comme des règles de réécriture explicites.
Portée : Les auteurs précisent explicitement que leur approche est spécialisée pour le $\lambda$ -calcul et ses variantes, exploitant le langage interne métathéorique du modèle catégorique. Ils reconnaissent que les e-graphs à emplacements peuvent être plus flexibles pour des langages arbitraires avec des lieurs (comme le $\pi$ -calculus), mais soutiennent que leur méthode est supérieure pour les optimisations spécifiques au $\lambda$ -calcul.

Le travail ne présente pas d'implémentation logicielle complète ni de benchmarks empiriques dans ce papier, mais positionne la représentation par e-hypergraphe fermé comme une fondation viable pour construire des « e-graphs pour la réécriture de diagrammes de cordes » dans des travaux futurs.