| Titre : | Critères de Finitude Homologique pour la non Convergence des Systèmes de Réécriture de Termes | | Type de document : | texte imprimé | | Auteurs : | P. MALBOS, Auteur | | Année de publication : | 2004 | | Langues : | Français (fre) | | Tags : | THEORIE ALGEBRIQUE SYSTEMES DE REECRITURE ALGEBRE HOMOLOGIQUE THEORIE ALGEBRIQUE SYSTEMES DE REECRITURE ALGEBRE HOMOLOGIQUE REWRITING SYSTEMS ALGEBRAIC THEORIES HOMOLOGICAL ALGEBRA | | Index. décimale : | THE Thèses de doctorat | | Résumé : | 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 à un calcul de forme normale. Cependant, tous les monoïdes décidables ne peuvent pas être résolus de cette façon. Un programme, initié par Squier, vise à 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 à 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.
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. | | Directeur(s) de thèse : | GUIN D. | | Co-directeur(s) de thèse : | ELBAZ-VINCENT P. | | Président du jury : | CURIEN P.L. | | Rapporteur(s) : | GOUBAULT E.;LAFONT Y.;PORTER T. | | Invité(s) : | SALLANTIN J. | | Date de soutenance : | 28/01/2004 |
Critères de Finitude Homologique pour la non Convergence des Systèmes de Réécriture de Termes [texte imprimé] / P. MALBOS, Auteur . - 2004. Langues : Français ( fre) | Tags : | THEORIE ALGEBRIQUE SYSTEMES DE REECRITURE ALGEBRE HOMOLOGIQUE THEORIE ALGEBRIQUE SYSTEMES DE REECRITURE ALGEBRE HOMOLOGIQUE REWRITING SYSTEMS ALGEBRAIC THEORIES HOMOLOGICAL ALGEBRA | | Index. décimale : | THE Thèses de doctorat | | Résumé : | 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 à un calcul de forme normale. Cependant, tous les monoïdes décidables ne peuvent pas être résolus de cette façon. Un programme, initié par Squier, vise à 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 à 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.
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. | | Directeur(s) de thèse : | GUIN D. | | Co-directeur(s) de thèse : | ELBAZ-VINCENT P. | | Président du jury : | CURIEN P.L. | | Rapporteur(s) : | GOUBAULT E.;LAFONT Y.;PORTER T. | | Invité(s) : | SALLANTIN J. | | Date de soutenance : | 28/01/2004 |
|
Affiner la recherche Interroger des sources externesCritères de Finitude Homologique pour la non Convergence des Systèmes de Réécriture de Termes / P. MALBOS
