E-graph
Cet article ne cite pas suffisamment ses sources ().
Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».
En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?
Un E-Graph en informatique est une structure de donnée servant à déterminer si une égalité peut être la conséquence de plusieurs autres égalités, et ceci de manière purement syntaxique.
On considère un ensemble d'égalité sur des termes sur un alphabet donné ayant des applications, des symboles et des variables. On souhaite savoir si une égalité entre deux termes est vraie ou fausse.
Création du graphe[modifier | modifier le code]
On considère que les termes sont représentés par des graphes orientés acyclique. La représentation est définie de manière récursive sur la hauteur des termes. Chaque constante (ou variable) est représentée par une feuille étiquetée par cette constante (ou variable), et les applications à n éléments d'un symbole f sont représentées par n arcs partant d'une racine étiquetée f vers les arbres représentant ces n sous-termes. Ces n arcs sont numérotés de 1 à n de manière à éviter que deux fonctions appliquées aux mêmes termes mais dans un ordre différent ne soient représentées par le même arbre.
Il faut bien voir qu'il y a autant de nœuds étiquetés par f qu'il y a d'applications de f à des termes différents, par contre quand deux termes sont identiques on considère qu'ils ont le même arbre. L'égalité sur les termes est donc équivalente à l'égalité sur des arbres.
Rajout des égalités[modifier | modifier le code]
Une fois qu'on a créé autant d'arbres qu'il fallait pour les termes qui appartiennent aux hypothèses et à la conclusion recherchée, on passe à une deuxième étape.
On initialise une structure d'union-find uf, dans laquelle on fait une union entre chaque terme égaux.
Pour chaque couple de nœud ayant la même étiquette et le même nombre n de fils, on regarde si leurs ième fils sont égaux pour selon uf, pour tout i entre 1 et n. Si c'est le cas, alors on fait l'union de ces deux nœuds dans uf.
On itère cette étape jusqu'à trouver un point fixe. Celui-ci existe car à chaque étape le nombre d'égalité augmente et est majoré par n*(n-1) si n est le nombre de terme du graphe.
Réponse[modifier | modifier le code]
Pour savoir si deux termes sont égaux, il suffit de rendre vrai s'ils sont égaux selon uf, et de renvoyer la réponse.
Amélioration[modifier | modifier le code]
Il va de soi qu'en plus de cet algorithme, de multiples améliorations sont possibles pour l'implémentation, telles que :
- s'arrêter dès qu'on a prouvé l'égalité que l'on voulait montrer ;
- commencer par créer des ensembles de tous les nœuds ayant la même étiquette afin de diminuer le temps pris par l'itération ;
- garder la structure du E-graph en mémoire pour pouvoir éventuellement tester des égalités entre d'autre termes, et potentiellement rajouter de nouvelles égalités ou de nouveaux termes.
Extension[modifier | modifier le code]
Il faut remarquer que si l'algorithme répond non, cela ne signifie pas que deux termes sont différents, mais simplement qu'on ne peut pas prouver qu'ils sont égaux avec les axiomes donné faites.
Pour remédier à cela, on peut rajouter des hypothèses de différences. Il faut alors rajouter des arêtes entre les classes d'uf pour représenter la différence.
Cela permettra de prouver l'incohérence s'il y a une arête "différente" sur une seule classe.
De la même façon, on peut rajouter des préordres à l'aide d'un type d'arc distinct (en supposant que l'ordre passe au contexte). Si on ne peut pas trouver n1 et n2 tels que n1 > n2 et n2 > n1 alors c'est que le préordre est un ordre sur l'ensemble de termes considéré.
Lien externe[modifier | modifier le code]
- [www.decision-procedures.org/slides/equality-e-graphs.ppt Présentation]
