Si vous n'avez besoin que d'un modèle mathématique, sans vous préoccuper des performances réelles, j'opterais pour le plus simple : une carte fonctionnelle (fonction partielle finie) dans laquelle chaque élément est éventuellement lié à un autre élément avec lequel il a été fusionné.
- Si un élément n'est lié à rien, alors son représentant canonique est lui-même.
- Si un élément est lié à un autre élément, alors son représentant canonique est le représentant canonique de cet autre élément.
Note : dans le reste de cette réponse, comme c'est la norme avec union-find, je supposerai que les éléments sont simplement des nombres naturels. Si vous voulez un autre type d'éléments, il suffit d'avoir une autre carte qui lie tous les éléments à des nombres uniques.
Ensuite, vous devez définir une fonction find : UnionFind nat nat qui renvoie le représentant canonique d'un élément donné, en suivant les liens aussi longtemps que possible. Remarquez que cette fonction utiliserait la récursion, dont l'argument de terminaison n'est pas trivial. Pour y parvenir, je pense que le moyen le plus simple est de maintenir l'invariant selon lequel un nombre ne peut être lié qu'à un nombre inférieur (c'est-à-dire si i liens vers j entonces i > j ). Ensuite, la récursion se termine car, en suivant les liens, l'élément courant est un entier naturel décroissant.
Définition de la fonction union : UnionFind nat nat UnionFind est plus facile : union m i j renvoie simplement une carte mise à jour avec max i' j' la liaison avec min i' j' , donde i' = find m i y j' = find m j .
[Note sur les performances : le maintien de l'invariant signifie que vous ne pouvez pas choisir de manière adéquate laquelle des deux partitions doit être fusionnée dans l'autre, en fonction de leur rang ; cependant, vous pouvez toujours mettre en œuvre la compression de chemin si vous le souhaitez].
Quant à la structure de données à utiliser pour la carte, il en existe plusieurs. Le site bibliothèque standard (regardez sous le titre FSets ) possède plusieurs implémentations (FMapList, FMapPositive, etc.) satisfaisant l'interface FMapInterface . La librairie stdpp a gmap .
Encore une fois, si les performances ne sont pas un problème, choisissez simplement le codage le plus simple ou, plus important encore, celui qui rend vos preuves les plus simples. Je pense simplement à une liste de nombres naturels. Les positions de la liste sont les éléments dans l'ordre inverse . Les valeurs de la liste sont offsets c'est-à-dire le nombre de positions à sauter en avant pour atteindre la cible du lien.
- Pour un élément
i la liaison avec j ( i > j ), le décalage est i j .
- Pour un représentant canonique, le décalage est de zéro.
Avec mes meilleurs talents de pseudo-art ASCII, voici une carte où les liens sont { 62, 42, 30, 21 } et les représentants canoniques sont { 5, 1, 0 } :
6 5 4 3 2 1 0 element
/
[ 4 ; 0 ; 2 ; 3 ; 1 ; 0 ; 0 ] map
\ \____ \_
\___________/
La motivation est que l'invariant discuté ci-dessus est alors mis en application structurellement . On peut donc espérer que find pourrait en fait être défini par induction structurelle (sur la structure de la liste), et avoir une terminaison gratuite.
Un article connexe est publié : Sylvain Conchon et Jean-Christophe Filliâtre. A Persistent Union-Find Data Structure. Dans Atelier ACM SIGPLAN sur les ML .
Il décrit l'implémentation d'une structure de données union-find efficace en ML, qui est persistante du point de vue de l'utilisateur, mais qui utilise la mutation en interne. Ce qui peut être plus intéressant pour vous, c'est qu'ils prouvent que c'est correct dans Coq, ce qui implique qu'ils ont un modèle Coq pour union-find. Cependant, ce modèle reflète le magasin de mémoire pour le programme impératif dont ils cherchent à prouver la correction. Je ne suis pas sûr qu'il soit applicable à votre problème.
