L'algorithme de complétion de Knuth-Bendix permet, dans certains
cas, d'utiliser les systèmes de réécriture pour décider le
problème du mot dans un monoïde. Le problème du mot est alors
réduit a un calcul de forme normale. Cependant, tous les monoïdes
décidables ne peuvent pas être résolus de cette façon. Un
programme, initie par Squier, vise a caractériser par des
invariants algébriques la classe des monoïde décidables par
réécriture.
L'objectif de cette thèse est d'étendre ce travail a la réécriture
de termes.
Nous établissons des conditions de finitude homologique pour
l'existence de présentations convergentes de type fini par
réécriture de termes de théories équationnelles du premier ordre
avec une sorte. Une théorie équationnelle est sémantiquement
décrite par une théorie algébrique au sens de Lawvere. Nous
introduisons l'homologie de ces théories à coefficients dans les
bimodules non additifs, comme généralisation de l'homologie de
MacLane des anneaux. Cette homologie admet une interprétation en
terme d'homologie de Hochschild-Mitchell de la petite catégorie
sous-jacente. Nous généralisons les résolutions libres de Squier
et Kobayashi, établies en réécriture de mots, à la réécriture de
petites catégories. En utilisant ces résolutions, nous montrons
qu'une théorie algébrique admettant une présentation convergente
de type fini est de type bi-$\mathrm(PF)_(\infty)$. Nous
construisons une théorie équationnelle, non unaire, décidable et
n'admettant pas de présentation convergente de type fini.