Critères de finitude homologique pour la non convergence des systèmes de réécriture de termes

We construct homological finiteness conditions for the existence of finite type convergent presentations by rewriting of one-sorted and first-order equational theories. An equational theory is semantically described by an algebraic theory in the sense of Lawvere. Generalising the MacLane homology of rings, we introduce the homology of such an algebraic theory with coefficients in non additive bimodules. This homology can be interpretated in terms of Hochschild-Mitchell homology of the underlying small category. We generalise the free resolutions of Squier and Kobayashi from the string rewriting to the rewriting of morphisms in small categories. By using these resolutions, we prove that any algebraic theory admitting a finite type convergent presentation is of type bi-$\mathrm(PF)_(\infty)$. We construct a decidable non unitary equational theory which does not admit a finite type convergent presentation.L'algorithme de complétion de Knuth-Bendix permet, dans certainscas, d'utiliser les systèmes de réécriture pour décider leproblème du mot dans un monoïde. Le problème du mot est alorsréduit a un calcul de forme normale. Cependant, tous les monoïdesdécidables ne peuvent pas être résolus de cette façon. Unprogramme, initie par Squier, vise a caractériser par desinvariants algébriques la classe des monoïde décidables parréécriture.L'objectif de cette thèse est d'étendre ce travail a la réécriturede termes.Nous établissons des conditions de finitude homologique pourl'existence de présentations convergentes de type fini parréécriture de termes de théories équationnelles du premier ordreavec une sorte. Une théorie équationnelle est sémantiquementdécrite par une théorie algébrique au sens de Lawvere. Nousintroduisons l'homologie de ces théories à coefficients dans lesbimodules non additifs, comme généralisation de l'homologie deMacLane des anneaux. Cette homologie admet une interprétation enterme d'homologie de Hochschild-Mitchell de la petite catégoriesous-jacente. Nous généralisons les résolutions libres de Squieret Kobayashi, établies en réécriture de mots, à la réécriture depetites catégories. En utilisant ces résolutions, nous montronsqu'une théorie algébrique admettant une présentation convergentede type fini est de type bi-$\mathrm(PF)_(\infty)$. Nousconstruisons une théorie équationnelle, non unaire, décidable etn'admettant pas de présentation convergente de type fini