Combinatorial properties for termination in term rewriting theory
Propriétés combinatoires pour la terminaison de systèmes de réécriture
Résumé
The thesis is about termination in rewriting theory, with particular emphasis on complexity. Termination is an undecidable property of term rewriting systems. However, there exists a combinatorial result that provides a syntactic sufficient condition for termination: Kruskal's tree theorem. This theorem has given rise to several widely used termination orderings in automated reasoning. We study the complexity of those orderings in the case of string and term rewriting systems and give new upper bounds. This work relies on the theory of number-theoretic hierarchies of functions indexed by ordinals. A second part of the thesis is devoted to a modified approach to number-theoretic hierarchies of functions by means of a syntactic approach to ordinal recursion. Our framework of ordinal terms is defined by a set of function symbols whose semantics are given by a rewrite system. Terms are equipped with a binary operator that builds up limit terms from a fundamental sequence. Compared to set-theoretical ordinals, the calculus we obtain is more flexible and involves a more precise analysis of the recursion principle. It appears to be appropriate for finding semantic termination proofs in a systematic way through the reduction to the problem of solving ordinal term inequations. The proof then gives a complexity measure for free. Various examples of applications illustrate this method.
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.