, When a is in S but not in S ? , that is a is a quotient of a non-?-positive S-rewriting sequence, it states that a can be factorized using positive reductions. Note that in that case, P R P can never be terminating: indeed, because of the linear context, for any R-rule a : f ? g, we have a P R P -rewriting step given by g ? P ?f +

?. and +. ,

, However, the quasi-termination assumption of P R P is equivalent to the termination assumption of S ? given

, Indeed, by definition an infinite rewriting path in S ? comes from an infinite

D. J. Anick, On the homology of associative algebras, Trans. Amer. Math. Soc, vol.296, issue.2, pp.641-659, 1986.

L. Bachmair and N. Dershowitz, Completion for rewriting modulo a congruence, Theoretical Computer Science, vol.67, issue.2, pp.173-201, 1989.

B. Buchberger, Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal (An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal), Special Issue on Logic, Mathematics, and Computer Science: Interactions, vol.41, pp.475-511, 1965.

B. Buchberger, History and basic features of the critical-pair/completion procedure, Rewriting techniques and applications, vol.3, pp.3-38, 1985.

B. Dupont and P. Malbos, Coherent confluence modulo relations and double groupoids, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01898868

Y. Guiraud, E. Hoffbeck, and P. Malbos, Convergent presentations and polygraphic resolutions of associative algebras, Math. Z, vol.293, issue.1-2, pp.113-179, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01006220

Y. Guiraud and P. Malbos, Higher-dimensional normalisation strategies for acyclicity, Adv. Math, vol.231, issue.3-4, pp.2294-2351, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00531242

Y. Guiraud and P. Malbos, Polygraphs of finite derivation type, Math. Structures Comput. Sci, vol.28, issue.2, pp.155-201, 2018.
URL : https://hal.archives-ouvertes.fr/hal-00932845

G. Huet, Confluent reductions: abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach, vol.27, issue.4, pp.797-821, 1980.

J. Hullot, A catalogue of canonical term rewriting systems, SRI International, 1980.

J. and H. Kirchner, Completion of a set of rules modulo a set of equations, Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '84, pp.83-92, 1984.

J. and J. Li, Church-Rosser properties of normal rewriting, Computer science logic 2012, vol.16, pp.350-365, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00730271

D. Knuth and P. Bendix, Simple word problems in universal algebras, Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967), pp.263-297, 1970.

Y. Kobayashi, Complete rewriting systems and homology of monoid algebras, J. Pure Appl. Algebra, vol.65, issue.3, pp.263-275, 1990.

F. and W. Lawvere, Functorial semantics of algebraic theories, Proc. Nat. Acad. Sci. U.S.A, vol.50, pp.869-872, 1963.

P. Malbos and S. Mimram, Homological computations for term rewriting systems, 1st International Conference on Formal Structures for Computation and Deduction, vol.52
URL : https://hal.archives-ouvertes.fr/hal-01678175

L. Int, Proc. Inform., pages Art, p.17, 2016.

P. Malbos and S. Mimram, Cartesian polygraphic resolutions. en préparation, 2020.

C. Marché, Normalized rewriting: an alternative to rewriting modulo a set of equations, J. Symbolic Comput, vol.21, issue.3, pp.253-288, 1996.

M. Newman, On theories with a combinatorial definition of "equivalence, Ann. of Math, vol.43, issue.2, pp.223-243, 1942.

M. Nivat, Congruences parfaites et quasi-parfaites, Algèbre, Fasc. 1, pp.25-1971, 1973.

G. E. Peterson and M. E. Stickel, Complete sets of reductions for some equational theories, J. Assoc. Comput. Mach, vol.28, issue.2, pp.233-264, 1981.

J. A. Robinson, A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach, vol.12, pp.23-41, 1965.

A. Shirshov, Some algorithmic problems for Lie algebras, Sib. Mat. Zh, vol.3, pp.292-296, 1962.

C. C. Squier, Word problems and a homological finiteness condition for monoids, J. Pure Appl. Algebra, vol.49, issue.1-2, pp.201-217, 1987.

C. C. Squier, F. Otto, and Y. Kobayashi, A finiteness condition for rewriting systems, Theoret. Comput. Sci, vol.131, issue.2, pp.271-294, 1994.

T. , Term rewriting systems, Cambridge Tracts in Theoretical Computer Science, vol.55, 2003.

P. Viry, Rewriting modulo a rewrite system, 1995.

, CNRS UMR, vol.5208

, CNRS UMR, vol.5208, 2020.