Measuring Well Quasi-Orders and Complexity of Verification
Mercredi 3 juillet 2024 à 14h
ENS Paris-Saclay, salle 1Z18, Lien Zoom.
Abstract. We investigate three ordinal measures of a well quasi-order, also called ordinal invariants: maximal order type, width, and height. One main challenge is to compute the ordinal invariants of complex well quasi-orders built from simpler well quasi-orders through classical operation, such as the Cartesian product, and high-order constructions, like the finite words embedding.
In this thesis, we compute compositionally the maximal order type of the direct product, the width of the multiset embedding, and the height and width of the multiset ordering. Furthermore, we compute the width of the Cartesian product in restricted cases and prove tight bounds on the ordinal measures of the finite powerset.
In the process, we develop several tools and techniques, notably a game-theoretical approach to computing width using the notion of quasi-incomparable families of subsets. To tackle the width of the multiset ordering, we introduce and study a fourth ordinal invariant, the friendly order type.
As an illustration of the power of our results, we delimit a large family of elementary wqos, built from ordinals and classical constructions, whose ordinal invariants are known.
Résumé
Nous étudions trois mesures ordinales des beaux pré-ordres, aussi appelées invariants ordinaux: le type d'ordre maximal, la largeur et la hauteur. Un enjeu principal est de calculer les invariants ordinaux de beaux pré-ordres complexes construits à partir de beaux pré-ordres plus simples grâce à des opérations classiques, tel que le produit Cartésien, ou encore des opérations d'ordre supérieur comme le plongement sous-mot sur les mots finis.
Dans cette thèse, nous calculons compositionellement le type d'ordre maximal du produit direct, la largeur de l'ordre plongement sur les multisets, et les largeur et hauteur de l'ordre Dershowitz-Manna sur les multisets finis. De plus, nous calculons la largeur du produit Cartésien dans des cas restreints, et prouvons des bornes atteintes pour les mesures ordinales du powerset fini.
Pour ce faire, nous développons plusieurs outils et techniques, notamment une approche par jeu et stratégies pour calculer la largeur, amenant à la notion de famille de sous-ensembles quasi-incomparables. Pour la largeur de l'ordre Dershowitz–Manna, nous introduisons et étudions un quatrième invariant ordinal, le type d'ordre amical.
Pour illustrer l'intérêt de nos résultats, nous délimitons une grande famille de beaux pré-ordres élémentaires, construits à partir d'ordinaux et de constructions classiques, dont les invariants sont connus.
My manuscript is available here.
Membres du jury :
- Alexander Rabinovich, Professor, Tel Aviv University - Rapporteur & Examinateur
- Sophie Tison, Professeure émérite, Université de Lille, CRIStAL - Rapporteure & Examinatrice
- Thomas Colcombet, Directeur de recherche, CNRS, IRIF - Examinateur
- Évelyne Contejean, Directrice de recherche, CNRS, LMF - Examinatrice
- Mirna Džamonja, Professor, IRIF - Examinatrice
- Daniel Hirschkoff, Maître de conférence, ENS Lyon, LIP - Examinateur
- Andreas Weiermann, Professor, Ghent University - Examinateur
Directeur de thèse : Philippe Schnoebelen, Directeur de recherche, CNRS, LMF