- E-graph
-
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.
Sommaire
Création du graphe
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
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
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
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 ensemble 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
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ête 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 tel que n1>n2 et n2>n1 alors c'est que le pré-ordre est un ordre sur l'ensemble de termes considéré.
Wikimedia Foundation. 2010.
