Skip to Main content Skip to Navigation

Propriétés combinatoires pour la terminaison de systèmes de réécriture

Abstract : 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.
Document type :
File URL :
Complete list of metadata
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:57:05 AM
Last modification on : Friday, February 26, 2021 - 3:26:01 PM


  • HAL Id : tel-01747313, version 1



Hélène Touzet. Propriétés combinatoires pour la terminaison de systèmes de réécriture. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1997. Français. ⟨NNT : 1997NAN10295⟩. ⟨tel-01747313⟩



Record views