Abstract FR:

Cette thèse s'inscrit dans le cadre général de la preuve de terminaison de systèmes de réécriture, avec un accent particulier sur le problème de la complexité. La terminaison est une propriété indécidable de la théorie de la réécriture. Il existe toutefois un résultat de combinatoire qui fournit un critère suffisant : le théorème de Kruskal. Ce théorème a conduit à la définition d'ordres de terminaison largement utilisés en démonstration automatique. Nous donnons une analyse de la complexité pour ces ordres de terminaison dans le cas des termes ou des mots et nous envisageons quelles en sont les limites. L'approche que nous avons retenue pour cette étude repose sur la théorie des hiérarchies de fonctions indexées par les ordinaux. Un second volet de la thèse est consacré à une extension des hiérarchies de fonctions, avec la définition d'un système alternatif de termes ordinaux. Les opérateurs fonctionnels sont introduits de manière purement syntaxique. La construction des ordinaux limites est gérée par un opérateur unaire, qui permet d'intégrer les suites fondamentales à la notation. Par rapport aux ordinaux de la théorie des ensembles, ce système est à la fois plus souple dans le maniement des opérateurs fonctionnels et plus précis dans l'analyse de la récursion. Établir la terminaison d'un système de réécriture revient alors à résoudre une équation ordinale générée directement à partir des règles du système. Cela s'apparente à la résolution d'une équation récurrente sur les entiers. La preuve de terminaison fournit en outre une mesure gratuite pour la complexité. Plusieurs exemples illustrent cette approche.