Coherence of algebraic rewriting systems by decreasingness

Cohérence des systèmes de réécriture algébrique par décroissance La réécriture algébrique fournit un modèle de calcul pour les structures algébriques présentées par générateurs et relations, en orientant ces relations. Cette approche offre des méthodes algorithmiques pour résoudre des problèmes de décision, étudier les relations entre les relations et calculer des résolutions libres. Les systèmes de réécriture confluents et terminants génèrent des présentations cohérentes, où les relations entre les relations sont engendrées par des diagrammes de confluence des paires critiques. Cette méthode de complétion s’appuie sur le lemme de Newman, qui établit l'équivalence entre la confluence locale et la confluence dans les systèmes de réécriture terminants. van Oostrom a introduit la propriété de décroissance, permettant de prouver la confluence à partir de la confluence locale, sans nécessiter la terminaison des systèmes. Dans cette thèse, nous développons une approche basée sur la théorie de la décroissance de van Oostrom pour construire des présentations cohérentes de monoïdes à partir de systèmes de réécriture de mots qui ne sont pas nécessairement terminants. Nous étudions ces systèmes avec une description catégorique en utilisant la notion de polygraphes de dimension deux. Nous établissons également des présentations cohérentes d'algèbres associatives à partir de systèmes de réécriture linéaires non-terminants. Nous étudions ces derniers à l’aide du langage de polygraphes linéaires de dimension deux. Dans un premier temps, nous obtenons un résultat de cohérence pour les systèmes de réécriture abstraits non-terminants, en nous appuyant sur le principe d'induction par décroissance introduit par van Oostrom. Nous démontrons ensuite une méthode de complétion fondée sur cette méthode d'induction par décroissance, permettant de calculer une présentation cohérente à partir d'une présentation non-terminante des catégories. Ce résultat s'appuie sur le résultat de la cohérence abstraite en surmontant deux problèmes : la stabilité de la décroissance par rapport au contexte, et la décroissance des relations de Peiffer. Nous étendons ce résultat aux systèmes de réécriture de mots admettant une structure cristalline. Dans un second temps, nous établissons un théorème fondé sur l'induction par décroissance, qui permet d'obtenir une présentation cohérente à partir d'une présentation non-terminante des algèbres associatives. Ce résultat est sous l'hypothèse de la stabilité de la décroissance par rapport au contexte linéaire, ainsi que de la décroissance élémentaire des relations de Peiffer et des relations additives. Enfin, nous étendons ce résultat de cohérence aux présentations non-terminantes afin de construire des résolutions libres partielles à la Anick, à partir de présentations non-terminantes des algèbres associatives.