Abstract FR:

Le thème de la thèse concerne l'étude des ordres, en termes de complexité en réécriture, mais aussi dans le cadre des termes ordinaux, des hiérarchies de fonctions sous-récursives. Nous avons cherché à extraire de la notion de preuve de terminaison des informations concernant la complexité des fonctions calculées par des systèmes de réécriture. Cela nous a permis d'établir de nombreuses caractérisations, en termes de complexité, des systèmes de réécriture. Ainsi, est-il possible de déterminer a priori la complexité d’un système, au seul vu de sa preuve de terminaison. Nous étudions plus spécifiquement le cas de l'ordre de Knuth-Bendix et celui de l'ordre par interprétation polynomiale. D'autre part, nous avons entamé une recherche plus fondamentale concernant la représentation de la notion d'ordre dans les λ-calculs typés. Cet intérêt provient de ce qu'une telle représentation est nécessaire dès lors que l'on veut représenter des structures définies par des opérateurs ω -aire, ce qui est le cas des termes ordinaux par exemple. Nous étudions d'un point de vue sémantique l'univers de travail, nous dégageons en particulier une notion de structure monoïdale fermée, mais aussi de manière syntaxique en proposant un calcul pour lequel un type représente un graphe plutôt qu'un (traditionnel) ensemble