, 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 +
,
, 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
On the homology of associative algebras, Trans. Amer. Math. Soc, vol.296, issue.2, pp.641-659, 1986. ,
Completion for rewriting modulo a congruence, Theoretical Computer Science, vol.67, issue.2, pp.173-201, 1989. ,
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. ,
History and basic features of the critical-pair/completion procedure, Rewriting techniques and applications, vol.3, pp.3-38, 1985. ,
Coherent confluence modulo relations and double groupoids, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01898868
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
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
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
Confluent reductions: abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach, vol.27, issue.4, pp.797-821, 1980. ,
A catalogue of canonical term rewriting systems, SRI International, 1980. ,
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. ,
Church-Rosser properties of normal rewriting, Computer science logic 2012, vol.16, pp.350-365, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00730271
Simple word problems in universal algebras, Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967), pp.263-297, 1970. ,
Complete rewriting systems and homology of monoid algebras, J. Pure Appl. Algebra, vol.65, issue.3, pp.263-275, 1990. ,
Functorial semantics of algebraic theories, Proc. Nat. Acad. Sci. U.S.A, vol.50, pp.869-872, 1963. ,
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
, Proc. Inform., pages Art, p.17, 2016.
Cartesian polygraphic resolutions. en préparation, 2020. ,
Normalized rewriting: an alternative to rewriting modulo a set of equations, J. Symbolic Comput, vol.21, issue.3, pp.253-288, 1996. ,
On theories with a combinatorial definition of "equivalence, Ann. of Math, vol.43, issue.2, pp.223-243, 1942. ,
Congruences parfaites et quasi-parfaites, Algèbre, Fasc. 1, pp.25-1971, 1973. ,
Complete sets of reductions for some equational theories, J. Assoc. Comput. Mach, vol.28, issue.2, pp.233-264, 1981. ,
A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach, vol.12, pp.23-41, 1965. ,
Some algorithmic problems for Lie algebras, Sib. Mat. Zh, vol.3, pp.292-296, 1962. ,
Word problems and a homological finiteness condition for monoids, J. Pure Appl. Algebra, vol.49, issue.1-2, pp.201-217, 1987. ,
A finiteness condition for rewriting systems, Theoret. Comput. Sci, vol.131, issue.2, pp.271-294, 1994. ,
Term rewriting systems, Cambridge Tracts in Theoretical Computer Science, vol.55, 2003. ,
Rewriting modulo a rewrite system, 1995. ,
, CNRS UMR, vol.5208
, CNRS UMR, vol.5208, 2020.