E-graph

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.

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.

Pour savoir si deux termes sont égaux, il suffit de rendre vrai s'ils sont égaux selon uf, et de renvoyer la réponse.

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.

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é.

• [www.decision-procedures.org/slides/equality-e-graphs.ppt Présentation]