Une approche topologique et fibrationnelle des automates d'ordre supérieur

Cette thèse étudie les liens entre la théorie des automates et le lambda-calcul en termes de syntaxe, de sémantique et de logique. Le point de départ de cette étude est la notion de langage de lambda-termes reconnu par une catégorie cartésienne fermée, définie par Salvati, qui généralise à l'ordre supérieur la notion usuelle de langage régulier de mots et d'arbres finis. Tout d'abord, nous étendons le travail de Salvati en montrant que toutes les catégories cartésiennes fermées bien pointées, localement finies et non-posétales reconnaissent les mêmes langages de lambda-termes que la catégorie des ensembles finis, que nous appelons langages réguliers d'ordre supérieur. Nous étendons ensuite l'approche syntaxique de Hillebrand et Kanellakis à l'ordre supérieur, et montrons que les langages obtenus coïncident avec les langages réguliers d'ordre supérieur, reliant ainsi notre travail à celui de Nguyen et Pradic sur les automates implicites. Ceci établit la robustesse de la notion de langage régulier d'ordre supérieur. Nous construisons ensuite une fibration cartésienne fermée des langages réguliers, nous obtenons des quantificateurs dans le style de la logique monadique du second ordre, et nous montrons comment cela généralise la dérivée de Brzozowski à l'ordre supérieur. Deuxièmement, nous nous inspirons des idées issues de la dualité de Stone et définissons les lambda-termes profinis, une généralisation à l'ordre supérieur de la notion de mot profini. L'espace des lambda-termes profinis peut être décrit de trois manières équivalentes : comme une complétion métrique, comme le dual de Stone des algèbres Booléennes de langages réguliers d'ordre supérieur, et par paramétricité à la Reynolds. Les lambda-termes profinis forment une catégorie cartésienne fermée qui vérifie une propriété universelle par rapport à certaines catégories enrichies sur les espaces de Stone, ce qui fournit une interprétation sémantique du lambda-calcul profini. Nous nous concentrons ensuite sur le fragment d'ordre 2 du lambda-calcul profini, correspondant aux types d'arbres. Nous définissons la complétion profinie des clones, que nous considérons comme des algèbres d'arbres, et montrons qu'elle généralise les complétions profinies des ensembles et des monoïdes. Appliquée aux clones d'arbres, nous obtenons une notion d'arbre profini dont nous montrons qu'elle coïncide avec les lambda-termes profinis.