Université de Rennes Introduction to structure theory and its application to boolean functions Introduction à la théorie des structures et son application aux fonctions booléennes représentation canoniquefonction booléenneDiagrammes de Décision Binaire (BDD)Graphe Dirigé Acylique (DAG) canonical representationBoolean functionBinary Decision Diagram (BDD)Directed Acyclic Graph (DAG) Fonctions booléennes Modèles acycliques Cette dissertation introduit et formalise la notion de structures comme moyen mathématique de capturer diverses propriétés dans plusieurs domaines scientifiques. Nous définissons les représentations structurelles comme des arbres ou des graphes acycliques dirigés (DAG) de structures, où la sémantique globale est la composition des structures individuelles, permettant un raisonnement inductif et modulaire. Nous formaliserons les notions de représentations inductives et de représentations canoniquement inductives. Nous étudions les conditions nécessaires et suffisantes pour que les représentations structurelles soient canoniques, en introduisant le concept de « confluence structurelle », non formalisée auparavant, et en proposant plusieurs approximations. Nous appliquons notre théorie aux fonctions Booléennes, montrant qu'elle unifie la plupart des variantes de diagrammes de décision binaire tout en suggérant une manière systématique d'en concevoir de nouvelles. Enfin, nous discutons brièvement de leur mise en œuvre et des résultats expérimentaux encourageants, qui soutiennent notre affirmation selon laquelle les représentations basées sur la structure sont conçues pour une utilisation pratique. This dissertation introduces and formalizes the notion of structures as a mathematically sound way to capture various patterns in several domains across sciences. We introduce the notion of structure-based representations as essentially trees or directed acyclic graphs (DAG) of structures. The overall semantics is the composition of the individual structures which allows for inductive and modular reasoning. We formalize the intuitive notions of inductive representations and inductively canonical representations. We prove that the latter are, somewhat, equivalent to canonical structure-based representations. We study necessary and/or sufficient conditions under which structure-based representations are canonical, highlighting the need for a notion of "structural confluence" that was not formalized in previous work and for which we formalize several approximations in this dissertation. Structural confluence allows us to avoid various pitfalls associated with the usual (rewriting-rule oriented) notion of confluence, in particular, the difficulty to generally prove (or disprove) it without further assumptions. We apply our theoretical results to the case of Boolean functions. We show that our theory not only unifies most variants of Binary Decision Diagrams but also suggests new ones in a principled way. We briefly discuss their implementation and encouraging experimental results supporting our claim that structure-based representations are designed for practical use. Electronic Thesis or DissertationText en application/pdf1 : 2945 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/e7dedaad-231b-4db2-83df-6bd1b37c1b0f Thibault Joan 1995-02-12 FR 28458407X joan.thibault@live.fr 2024URENS104 http://www.theses.fr/2024URENS104 2024-12-19 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Doctorat non ouiCaillaudBenoîtintervenant_1148066518GhorbalKhalilintervenant_2160369223TruchetCharlotteintervenant_3183896068CaillaudBenoîtintervenant_1148066518GhorbalKhalilintervenant_2160369223MazzaDamianointervenant_6115658599CouceiroMiguelintervenant_4223362395GenitriniAntoineintervenant_5 MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 CaillaudBenoîtGhorbalKhalilTruchetCharlotteCouceiroMiguelGenitriniAntoineMazzaDamianoUniversité de RennesMATISSE IRISA ASCII PDF 3016002