Contexte des e‑graphs

Un e‑graph (equality graph) est une structure qui conserve une relation de congruence sur des arbres d’expression, c’est‑à‑dire une équivalence stable lors de la construction de nouvelles expressions. Le concept a été introduit par Nelson et Oppen en 1980. Après plusieurs décennies de relative obscurité, Willsey et al. (2021) ont montré, via le paquet egg, que les e‑graphs combinés à la saturation d’égalité offrent une méthode rapide et adaptable pour le raisonnement équationnel. Leur successeur, egglog (Zhang et al., 2023), étend le cadre aux catégories finiment présentées, ouvrant la voie à une analyse plus abstraite.

Diagrammes et foncteurs initiaux

Dans la théorie des catégories, une équation entre morphismes se représente par un diagramme commutatif. Formellement, un diagramme est un foncteur D : J → C où J est la catégorie d’indice. Le texte introduit la notion de foncteur initial R : J → K, noté R : J ↠ K, caractérisée par trois conditions équivalentes :

- préimage de limites préserve les limites : lim_K D → lim_J (D∘R) est un isomorphisme ;
- préimage de limites de ensembles donne une bijection : lim_K D → lim_J (D∘R) ;
- chaque tranche R/k est non vide et connexe.

Ces critères garantissent que le tirage arrière d’un diagramme le long de R ne modifie pas les solutions des équations qu’il encode. Sans cette propriété, les opérations de « pull‑back » ou d’extension de diagrammes pourraient introduire ou perdre des identités, brisant ainsi la cohérence du raisonnement.

Analyse de la sémantique catégorique

Deux travaux récents (Biondo, Castelnovo & Gadducci 2025 ; Tiurin et al. 2025) proposent une sémantique catégorique des e‑graphs en les re‑définissant comme e‑hypergraphes : des hypergraphes étiquetés munis d’une structure supplémentaire qui encode explicitement une relation d’équivalence. Cette abstraction élimine les détails d’implémentation tels que l’union‑find, tout en conservant la capacité de raisonner sur les congruences. L’auteur du billet prévoit de remplacer les e‑hypergraphes par des « e‑diagrammes », où les transformations autorisées seront exactement les foncteurs initiaux décrits plus haut. Ainsi, chaque manipulation de diagramme correspond à un passage de D à D∘R avec R initial, assurant la préservation des limites et donc des équations sous‑jacentes.

Limites et perspectives

Le cadre présenté se limite d’abord aux symboles fonctionnels unaires, afin de réduire la complexité de la construction des catégories d’indice. Cette restriction exclut les produits finis, indispensables à la version classique des e‑graphs. L’auteur indique que les prochains articles élargiront le modèle aux catégories possédant des produits finis, récupérant ainsi la pleine puissance des e‑graphs. En attendant, l’absence de données empiriques sur les performances de l’approche catégorique rend difficile l’évaluation comparative avec les implémentations traditionnelles basées sur union‑find.