Diagramme de Décision Fonctionel: Une Structure de Donnée Unifiante pour les Diagrammes de Décision Binaires

Zero-suppressed binary Decision Diagram (ZDD) is a notable alternative data structure of Reduced Ordered Binary Decision Diagram (ROBDD) thatachieves a better size compression rate for Boolean functions that evaluate to zero almost everywhere.Deciding \textit{a priori} which variant is more suitable to represent a given Boolean function is as hard as constructing the diagrams themselves.Moreover, converting a ZDD to a ROBDD (or vice versa) often has a prohibitive cost.This observation could be in fact stated about almost all existing BDD variants as it essentially stems from the non-compatibilityof the reduction rules used to build such diagrams.Indeed, they are neither interchangeable nor composable.In this work, we investigate a novel functional framework, termed Lambda Decision Diagram (LDD), that ambitions to classify the already existing variants asimplementations of special LDD models while suggesting, in a principled way, new models that exploit application-dependant propertiesto further reduce the diagram's size.We show how the reduction rules we use locally capture the global impact of each variable on the output of the entire function.Such knowledge suggests a variable ordering that sharply contrasts with the static fixed global ordering in the already existing variants as well as the dynamic reordering techniques commonly used.Zero-suppressed binary Decision Diagram (ZDD) est le variant le plus connu des Reduced Ordered Binary Decision Diagram (ROBDD) permettant d'atteindre une représentation plus compacte en mémoire des fonctions booléennes creuses, i.e., les fonctions valant zéro presque partout.Décider \'a priori quel variant est plus adapté pour représenter une fonction donnée est aussi dur que construire les diagrammes eux-mêmes. De plus, convertir un ZDD en ROBDD (ou vice versa) a usuellement un cout trop élevé. Cette même observation peut être faite pour presque tous les variants de BDD dans la mesure où les règles de réductions pour calculer les diagrammes sont pour l'essentiel incompatibles. En particulier, elles ne peuvent ni commuter ni composer.Dans cet article, nous introduisons une interprétation fonctionnelle des BDD, dénommée Lambda Decision Diagram (LDD), qui a pour ambition de classifier les variants existants comme des implémentations particulières de modèles de LDD tout en suggérant, de manière systématique, de nouveaux modèles exploitants des propriétés spécifiques aux applications souhaitées.De manière à d'avantage réduire la taille des diagrammes, nous montrons comment les règles de réduction capturent, dans une certaine mesure, l'impacte global de chaque variable sur le résultat des fonctions considérées.Cette connaissance suggère un ordre local des variables: ceci différencie fortement notre approche de l'ordre statique global des variants déjà existants ou des techniques de réordonnancement dynamique. Nous appelons ces variants uniformes dans la mesure où les règles de réduction sont appliquées de manière identique à chaque variable et non spécifiquement à la première dans l'ordre choisi