| Introduction to structure theory and its application to boolean functions (Introduction à la théorie des structures et son application aux fonctions booléennes) Thibault, Joan - (2024-12-19) / Université de Rennes Introduction to structure theory and its application to boolean functions
| |||
Langue : Anglais Directeur(s) de thèse: Caillaud, Benoît; Ghorbal, Khalil Discipline : Informatique Laboratoire : IRISA Ecole Doctorale : MATISSE Classification : Informatique Mots-clés : représentation canonique, fonction booléenne, Diagrammes de Décision Binaire (BDD), Graphe Dirigé Acylique (DAG)
| |||
Résumé : 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. Abstract : 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. | |||