Twenty years after the discovery of the F5 algorithm, Gröbner bases with signatures are still challenging to understand
and to adapt to different settings.
This contrasts with Buchberger's algorithm, which we can bend in many directions keeping correctness and termination obvious.
I propose an axiomatic approach to Gröbner bases with signatures
with the purpose of uncoupling the theory and the algorithms, and giving general results applicable in many different settings (e.g. Gröbner for submodules, F4-style reduction, noncommutative rings, non-Noetherian settings, etc.).

§ INTRODUCTION

Introduced by Faugere_2002 to compute ,
the F5 algorithm proposes the concept of signature
to avoid the redundant computations that arise in Buchberger's algorithm Buchberger_1965,Buchberger_2006.
Each polynomial handled by the algorithm is augmented with a signature
designed to enforce a fundamental postulate, which we may state as “two elements with the same signature are substitutable”.
We can find precursive ideas in the work of GebauerMoller_1986 and MollerMoraTraverso_1992
and signatures also share somes ideas with Hilbert-driven algorithms []Traverso_1996.

Today's situation of signature algorithms is equivocal.
F5's relevance, from the pure aspect of performance,
was demonstrated by a success on cryptographic challenges early on FaugereJoux_2003.
But none of the current best implementations for computing  uses signatures, be it Magma BosmaCannonPlayoust_1997, msolve BerthomieuEderSafeyElDin_2021, Singular Singular_CAS or Maple.
They prefer Buchberger's algorithm, handling S-pairs as GebauerMoller_1988 do
and using simultaneous reductions in the F4 style Faugere_1999 – see the report of MonaganPearce_2015 on this approach.
The theoretical benefits of signature algorithms are diminished by a higher implementation complexity
and a larger output (the signature bases computed by signature algorithms are more constrained than ).
More than benchmarks, literature about signature algorithms is turned towards revealing the core ideas
behind F5 and understanding what makes a signature algorithm terminate.
Termination is a very peculiar aspect, not as transparent as termination of Buchberger's algorithm.
Nonetheless, thanks to decisive work by HashemiArs_2010,GaoGuanVolny_2010,ArriPerry_2011,EderPerry_2011,GaoVolnyWang_2016
these goals have been reached – see the survey by EderFaugere_2017.

The point of studying signature algorithm may not be the quest of new world records for polynomial system solving,
but rather the understanding of signatures themselves, and what we can extract from them.
Signature bases convay an extra information compared to , related to the syzygy module of the input generators. Many ideal-theoretic operations – intersection, quotient, saturation, Ext modules Stillman_1990 –
are related to syzygy modules, and signature algorithms seem to give an efficient access to them
Porting these ideas to more general settings is a strong motivation to engage in the study of signatures.
Yet, in my view, the lack of flexibility of the theory of signature algorithms hinders further development, both practical and theoretical. For example, modern implementations for computing  make it clear that simultaneous reductions in the F4 style are key towards high performance. Yet, there is no satisfactory description of a signature algorithm with F4-style reduction (AlbrechtPerry_2010 do not prove termination and [13]EderFaugere_2017 are superficial).

I propose a set of axioms that specifies a context in
which signature algorithms are applicable. They fit many known settings – such as solvable algebras SunWangMaZhang_2012 and free algebras HofstadlerVerron_2022 – and some previously unknown settings – such as the module case or localizations of Weyl algebras with an elimination order, see Section <ref>. Note however that the case where the coefficient ring is not a field is out of scope, as well as local orderings. Many of the ideas of the most recent frameworks for signature algorithms EderPerry_2011,GaoVolnyWang_2016 work smoothly in this axiomatic setting, so many statements will of course be familiar, yet with a wider applicability.

Working with axioms makes some useful ideas emerge.
At least two of them are worth attention.
Firstly, the concept of prebasis is introduced to uncouple the theory from the input.
Previous work all start by fixing the input and developping the theory with respect to this input [e.g.][Definition 2.2]EderFaugere_2017.
This is problematic when trying to define what a  is, independently of an input.
are defined by the equality $\brack{\lm G} = \lm \brack{G}$, or the confluence of some rewriting system,
we do not need to say a  of something [e.g.][Definition 5.37]BeckerWeispfenning_1993.
It is a very desirable definition which should have an equivalent in the signature setting.
The main obstacle here is the definition of signatures independently of an input.
This raise an interesting question:
given a set of signatures – basically anything well-ordered on which act monomials –, what are the admissible inputs?
This leads to the concept of prebasis, that is
a set of sigpoly pairs which satisfy the fundamental postulates of signatures (elements with equal signatures are substitutable). I prove that if a set of sigpoly pairs is a  in the module representation, then it is a prebasis (Theorem <ref>).

Secondly, I introduce sigtrees to uncouple the termination criterion from the algorithms themselves. Sigtrees make a very general termination criterion.
For Buchberger's algorithm, termination follows from a general principle, Dixon's Lemma,
not from ad hoc arguments.
The concept of sigtrees is a tentative to provide such a general argument.
As a direct application, it proves the termination of signature algorithms with out-of-order signature handling and the F5 reductant selection strategy (among all possible reductants, choose the most recent one).
It was unproved even in the classical polynomial setting.
We may blend in an F4-style reduction, the termination argument remains the same.

Lastly, as a didactic contribution, I try to emphasize an elemental feature of  (or rather, for that matter, ),
putting a clear distinction with .
To check that a given set $G$ is a  of an ideal $I$,
it is enough to check that (1) $G$ generates $I$, and (2) the S-pairs reduce to zero.
Typically (1) will hold by design if $G$ has been constructed from a generating set of $I$ by adding new elements
obtained by allowed reduction steps. The condition (2) is more difficult to check and requires arithmetic operations in the base field.
This is typically a costly operation.
To check that a given set $G$ with signatures is a  of an ideal $I$,
it is enough to check that (1') $G$ is a prebasis of $I$, and (2') the leading monomials and the signatures satisfy some combinatorial property (Corollary <ref>).
The concept of prebasis is introduced in Section <ref>, but for the moment, it is enough to say that (1') will hold by design
if $G$ is obtained by allowed reduction steps from an initial prebasis of $I$.
The important part is the nature of (2'): it requires no arithmetic operations to be checked, only operations on monomials.
Algorithms for  are all about exploiting this combinatorial structure.
This reminds of staggered linear bases introduced by []GebauerMoller_1986 to compute , they feature a similar combinatorial structure – and the link with signatures have recently been investigated by HashemiJavanbakht_2021.

In Section <ref>, we define the algebraic structure in which we consider , monomial modules,
that are vector spaces with a “leading monomial” map and an action of a monoid
with some compatibility rules. We also introduce the rewriting system defined by the top reduction.
In Section <ref>, we define signatures,  and prebases.
In Section <ref>, we define  and state a combinatorial criterion for a set to be a .
In Section <ref>, we introduce Noetherian hypotheses, termination arguments and review algorithm templates.
In Section <ref>, we illustrate the axioms by several different settings in which they apply.

I am grateful to Hadrien Brochet and Frédéric Chyzak for a very careful reading and useful comments.

Before going to signatures,
we lay down some definitions.
The main ones are the definitions of a monomial space – a vector space with a concept of leading monomial, see <ref> – and a monomial module – a monomial space
endowed with a linear action of a (non necessarily commutative) monoid, compatible with leading monomials,
see Section <ref>.

In monomial spaces, we develop a (short) theory of top reduction modulo tail equivalence,
using the terminology of rewriting systems, see Section <ref> and <ref>.
Using rewriting systems to describe the theory of  in polynomial rings is done in several textbooks [e.g.][]BeckerWeispfenning_1993,Winkler_1996,KreuzerRobbiano_2000,Mora_2005: in a few words, we say that a polynomial $f$ can be reduced by a polynomial $g$, if the we can cancel out one of the terms of $f$ by substracting a multiple of the leading monomial of $g$.
The context of signatures puts the emphasis on top reduction – the reduction of the leading monomial –
as opposed to tail reduction.
The practice of  computation also shows
that tail reduction steps are optional, they are irrelevant as far as termination and correctness is concerned.
Lastly, tail reduction does not enjoy nice properties.
For example, if $g$ reduces $f$ then $mg$ reduces $mf$ for any monomial $m$, in a polynomial setting.
But this implication breaks if $m$ is a polynomial rather than a monomial,
or if $f$ and $g$ lie in a Weyl algebra, unless the reduction is a top reduction.
All of this hints at replacing tail reduction by a more flexible tail equivalence
and replace the customary reduction by the top reduction modulo tail equivalence.
This fits the abstract setting of “reduction modulo equivalence” developed by Huet_1980.

§.§ Rewriting systems

Let $X$ be a set and $\myto{1}$ a binary relation on $X$. “$x\myto{1} y$” reads “$x$ reduces to $y$”.
Following Huet_1980, we define
the following binary relations:[Actually Huet denotes $\to$ the one-step reduction, which I denote $\myto1$,
and $\myto*$ the multistep reduction, which I denote $\to$.]

* $x \myto{n} y$, for $n>0$, if there is some $z\in X$ such that $x\myto{1} z$ and $z\myto{n-1}y$;

* $x\to y$ if $x\myto{n}y$ for some $n \geq 0$, this is the reflexive transitive closure of $\myto1$;

* $x\uparrow y$ if there is some $z\in X$ such that $z\to x$ and $z\to y$;

* $x\downarrow y$ if there is some $z\in X$ such that $x\to z$ and $y\to z$.

The relation $\myto{1}$ is Noetherian if there is no infinite sequence $x_0\myto1 x_1 \myto1 \dotsb$.
An element $x\in X$ is $\myto1$-reduced if there is no $y\in X$ such that $x\myto{1} y$.
If $x \to y$ and $y$ is $\myto1$-reduced, then $y$ is a normal form of $x$.
If $\myto1$ is Noetherian, then every element has at least one normal form.
The relation $\myto{1}$ is confluent if $x\uparrow y$ implies $x\downarrow y$ for any $x, y\in X$.
If $\myto{1}$ is confluent, then any $x\in X$ has at most one normal form.

Moreover, given an equivalence relation $\smile$ on $X$,
we define:

* $x \tup y$ if there are $z, z' \in X$ such that $z\smile z'$, $z\to x$ and $z'\to y$;

* $x \tdown y$ if there are $z, z' \in X$ such that $z\smile z'$, $x\to z$ and $y\to z'$;

The relation $\rew$ is confluent modulo $\smile$ if for any $x, y\in X$, if $x\tup y$ then $x\tdown y$.

§.§ Top reduction

Let $\basis$ be a set with a well-order $\leq$ and a minimal element denoted $0$.
Let $M$ be a linear space over a field $K$
endowed with a surjective map $\lm : M \to \basis$ (where $\lm$ stands for leading monomial in analogy with the usual polynomial setting)
such that

*  $\forall x\in M, \lm x = 0 \Leftrightarrow x = 0$;

*  $\forall x, y\in M, \lm x = \lm y \neq 0 \Leftrightarrow \exists \lambda \in K^\times, \lm(x-\lambda y) < \lm x$.

A linear space with such a map $\lm$ is called a monomial space. The set of monomials of $M$ is the corresponding set $\basis$.[We could define $\basis \setminus \left\{ 0 \right\}$ to be a basis of $M$
and then define the leading monomial in the usual way. But for a single determination of the map $\lm$, there would be many ways to choose such a basis.
The axiomatic definition above highlights the irrelevance of nonleading terms.
Nonetheless, the easiest way to describe the map $\lm$ on concrete example is indeed to exhibit a well-ordered basis of $M$.]
It is useful to introduce the relation $\eqlt$ defined on $M$ by $x\eqlt y$ if $x=y=0$ or $\lm(x-y) < \lm x$,
to be understood as “$x$ and $y$ have the same leading term”.
We first state useful relations between sums and leading monomials that follow directly from the axioms.

For any $x, y, z\in M$,

* $\forall\lambda\in K^\times, \lm(\lambda x) = \lm x$;

*  $\lm(x+y) \leq \max(\lm x, \lm y)$;

* $x \eqlt y \Rightarrow \lm x = \lm y$;

* $\eqlt$ is an equivalence relation.

A subset $E\subseteq M$ defines a relation $\rew_E$, called top reduction, on $M$
defined by

\[ x \rew_E y \Leftrightarrow \lm y < \lm x \text{ and } \exists \lambda \in K^\times, \exists e \in E, y = x - \lambda e. \]

In other words, $x\rew_E y$ if $y$ is the result of cancelling the leading monomial of $x$ using a reducer in $E$.
In this situation, we always have $\lambda e \eqlt x$.
Moreover, we introduce a relation $\tailred_E$, called tail equivalence, defined by

\[ x \tailred_E y \Leftrightarrow \exists \lambda\in K^\times, \exists e\in E, y = x - \lambda e \text{ and } \lm e < \lm x. \]

In this situation, we always have $x \eqlt y$.
The reflexive transitive closure of $\tailred_E$ is denoted $\smile_E$.
The confluence relations $\tup_E$ and $\tdown_E$ are defined using $\smile_E$.
The tail equivalence is not a reduction since it is symmetric, we cannot tell which side of an equivalence $x\smile_E y$ is more reduced.

The following statement is a variant, in the setting of monomials spaces, of the  Buchberger's well known criterion for polynomial ideals.
A subset $E\subseteq M$ is a pivot basis if it satisfies the equivalent properties of Theorem <ref>.
The concept of pivot basis is similar to that of a row echelon form of a matrix.
For $E\subseteq M$, let $\brack{E}$ denote the $K$-linear subspace generated by $E$.

Let $E$ be a subset of $M$.
The following assertions are equivalent:

(Characterization by leading monomials)

*  $\forall x\in {\brack{E}}, x \neq 0 \Rightarrow \exists e\in E, \lm e = \lm x$.

(Characterization by rewriting)

*  $\forall x\in {\brack{E}}, x \to_E 0$;

(Characterizations by confluence properties)

*  $\forall x, y\in M, x - y \in \brack{E} \Rightarrow x\tdown_E y$;

*  $\to_E$ is confluent modulo $\smile_E$, that is  $\forall x, y\in M, x \tup_E y \Rightarrow x\tdown_E y$;

(Characterizations by S-pairs)

*  $\forall e, f\in E, \forall \lambda \in K^\times, e \eqlt \lambda f \Rightarrow e-\lambda f \to_E 0$;

*  $\forall e, f\in E, \forall \lambda \in K^\times, e \eqlt \lambda f \Rightarrow e - \lambda f \in \brack{g\in E\st \lm g<\lm e}$;

Let $x \in \brack{E}$ be a nonzero element
and let $y$ be a $\to$-normal form of $x$. In particular $y\in \brack{E}$.
By hypothesis, either $y=0$, or $\lm y = \lm e$ for some $e\in E$. The latter would contradict the irreducility of $y$, so $y=0$ and $x\to 0$.

Let $x, y\in M$ such that $x-y\in \brack{E}$.
There is some $e\in E$ and $\lambda\in K^\times$ such that $x-y \myto1 x-y-\lambda e \to 0$ (unless $x=y$ but this case is trivial). In particular $\lambda e \eqlt x-y$.

If $\lm x > \lm y$, then $x\myto1 x-\lambda e$ and $x-\lambda e - y \in \brack{E}$
and by induction on $\max(\lm x, \lm y)$, we may assume that $x-\lambda e\tdown y$ and therefore $x\tdown y$.
The case $\lm y > \lm x$ is similar.
If $\lm x = \lm y$, there is some $\mu \in  K^\times$ such that $\lm(x - \mu y) < \lm x$.
There are again two cases. If $\mu = 1$, that is $x\eqlt y$,
then the sequence of top-reduction $x-y \myto1 u_1 \myto1 u_2 \myto1 \dotsb \myto1 u_n \myto1 0$
gives a sequence of tail equivalence
$y \smile y + u_n \smile y + u_{n-1} \smile \dotsb \smile y + (x-y) = x$.
In particular, $x\tdown y$.
If $\mu \neq 1$, then $\lm x = \lm y = \lm e$,
so there are reductions $x \myto1 x - \kappa e$ and $y\myto1 y - \nu e$, for some $\kappa,\nu\in K^\times$.
By induction on $\max(\lm x, \lm y)$, we may assume that $x -  \kappa e \tdown y - \nu e$,
which implies $x \tdown y$.

Let $x, y\in M$ such that $x\tup y$.
Both $\myto1$ and $\tailred$ preserve equality modulo $\brack{E}$, so $y-x \in \brack{E}$,
therefore $x \tdown y$, by hypothesis.

If $e \eqlt \lambda f$, then $e \myto1 e - \lambda f$.
Moreover $e\myto1 e-e = 0$. The confluence hypothesis implies that $e - \lambda f \to z$
and $0 \to z'$ for some $z, z'\in M$ such that $z\smile z'$.
But $0$ is reduced and only $\smile$-equivalent to itself.
So $z = 0$ and $e - \lambda f \to 0$.

The rewriting $e - \lambda f \rewrites_E 0$ implies,
by definition of $\to_E$, this implies that $e-\lambda f\in \brack{g\in E\st \lm g \leq \lm (e-\lambda f)}$.
Since $\lm(e - \lambda f) < \lm e$, this gives the claim.

Let $x\in \brack{E}$
and let $m\in \basis$ minimal such that $x\in \brack{e\in E\st \lm e \leq m}$.
We can write $x = \lambda_1 e_1 + \dotsb + \lambda_r e_r$ with $e_i \in E$, $\lambda_i \in K$
and $\lm e_i \leq m$.
By minimality of $m$, and up to reordering the indices, we may assume that $\lm e_1 = m$.

Assume for contradiction that $\lm x < m$.
For each $i$, there is some $\mu_i \in K$ such that $e_i - \mu_i e_1 \in \brack{e\in E\st \lm e < m}$:
if $\lm e_i < m$, we choose $\mu_i = 0$,
and if $\lm e_i = m$, we choose $\mu_i$ such that $e_i \eqlt \mu_i e_1$ (using <ref>)
and then <ref> ensures that $e_i - \mu_i e_1 \in \brack{e\in E\st \lm e < m}$.
The equality

\[ x - \sum_{i=1}^r\lambda_i (e_i - \mu_i e_1) =  \big(\sum_{i=1}^r \lambda_i\mu_i \big) e_1 \]

implies that $\lambda_1\mu_1+\dotsb+\lambda_r\mu_r = 0$, otherwise, the leading monomial of the right-hand side would be $m$, greater that the leading monomial of the left-hand side. Therefore

\[ x = \sum_{i=1}^r \lambda_i (e_i - \mu_i e_1). \]

Thus, $x \in \brack{e\in E\st \lm e < m}$, contradicting the minimality of $m$.
Therefore $\lm x = m = \lm e_1$.

The following minor lemma, on increasing unions of pivot bases, will be used in Sections <ref>
and <ref>.

Let $I$ be a totally ordered set
and let $(E_i)_{i\in I}$ be a family of subsets of $M$.
If $E_i \subseteq E_j$ for any $i,j \in I$ with $i < j$,
and if each $E_i$ is a pivot basis, then $\cup_{i\in I} E_i$ is a pivot basis.

We check the criterion <ref>.
Let $e, f \in \cup_i E_i$ and $\lambda \in K^\times$ such that $e \eqlt \lambda f$.
By definition, $e$ is in some $E_j$ while $f$ is in some $E_k$,
so both $e$ and $f$ are in $E_{\max(j,k)}$.
Since $E_{\max(j,k)}$ is a pivot basis, $e - \lambda f \to 0$ with respect to $E_{\max(j,k)}$.
A fortiori, it rewrites to $0$ with respect to $\cup_i E_i$, which contains $E_{\max(j,k)}$.

§.§ Monomial modules

A monoid is a set $A$ with an associative composition
law $A\times A\to A$ (denoted multiplicatively) which admits an identity element
denoted $1_A$. A monomial module over a monoid $A$
is a monomial space $M$ with a linear action of $A$ on $M$ (denoted also multiplicatively)
with some compatibility with the map $\lm$ and the order $\leq$. In details, we require that:

*  $\forall f\in M, 1_A f = f$;

* $\forall a, b\in A, \forall f\in M, (ab)f=a(bf)$;

* $\forall a\in A, \forall f, g\in M, \forall \lambda \in K, a(f + \lambda g) = af + \lambda (ag)$;

*  $\forall a\in A, \forall f, g \in M, \lm f = \lm g \Rightarrow \lm(af) = \lm(ag)$;

*  $\forall a\in A, \forall f, g\in M, \lm f < \lm g \Rightarrow \lm(af) < \lm(ag)$;

Assumption <ref> implies also the following:

*  $\forall a\in A, \forall f\in M, \lm(af) \geq \lm f$.

Indeed, if $\lm(af) < \lm f$, then $\lm(a^{k+1} f) < \lm(a^k f)$
for any $k \geq 0$, which would contradicts the well-orderedness of $\basis$.
Note also that $M$ is torsionfree: if $g \neq 0$, then $ag \neq 0$ for all $a\in A$,
as a consequence of <ref>.

Assumption <ref> and the surjectivity of $\lm$
makes it possible to define an action of $A$ on the set of monomials $\basis$ by $a \lm f \eqdef \lm(af)$.
A divisor of $m\in \basis$ is an element $n \in \basis$ such that $a n = m$ for some $a\in A$.

We can always embed $A$ in a $K$-algebra $R$ such that the composition law in $A$ is the restriction of the multiplication in $R$
and such that $A$ generates $R$, so that $M$ is a left module over $R$.
However, the assumptions <ref> and <ref> may not extend to $R$, or even to the nonzero elements of $R$.

In the context above,
a subset $G\subseteq M$ is a
if $A G$, that is $\left\{ af \st a\in A, f\in G \right\}$,
is a pivot basis.
It is naturally a key concept, see []CoxLittleOShea_2015 for an introduction to the topic.
The purpose of signatures it not to extend or generalize it, but rather to give a way to compute .

Let $f$ be a non zero element of $M$.
Is $\left\{ f \right\}$ a ?
It will be the case in many practical settings but it is not a consequence of the axioms above.
Unfolding the definitions, we see that it is implied by the following assumption:

*  $\forall f\in M, \forall g\in \brack{a f \st a\in A} \setminus \left\{ 0 \right\}, \exists a\in A, \lm g = \lm(af)$.

This holds, for example, when $A$ is the multiplicative monoid of a $K$-algebra
and if $M$ is a module over $A$, with the obvious compatibility conditions.

To check that $G$ is a a , we may apply Criterion <ref>.
This requires, in general, infinitely many checks,
many of them are redundant due to the action of $A$.
This leads to the well known Buchberger's criterion.
To state it, we define a set of critical pairs of a set $G\subseteq M$, as any set $P\subseteq \brack{AG}$, such that
for any $f, g \in G$, $a, b\in A$ and $\lambda \in K^\times$ such that $\lm(af - \lambda bg) < \lm (af)$,
there are some $c\in A$ and $h\in P$ such that $af-\lambda bg = c h$.
In the polynomial case, we may count on the existence of finite sets of critical pairs.
We will not elaborate further in this direction.

Let $G\subseteq M$ and let $P$ be a set of critical pairs for $G$.
Then $G$ is a  if and only if $h\to_G 0$ for any $h \in P$.

This follows directly from Criterion <ref> and Lemma <ref> below.

For any $G\subseteq M$, $f\in G$ and $a\in A$,
if $f \to_{AG} 0$, then $a f\to_{AG} 0$.

We proceed by induction on $n$ such that $f\myto n 0$. The base case $n=0$ is trivial.
Assuming $n > 0$, let $\lambda\in K$, $b\in A$ and $g\in G$ such that $f \myto1 f - \lambda bg \myto{n-1} 0$.
By induction hypothesis, $a f - \lambda abg \to 0$
and it remains to check that $af \myto 1 af - \lambda bag$.
This follows from <ref> as follows: $\lm(af - \lambda abg) = \lm (a (f-\lambda bg) ) < \lm (af)$.

§ SIGNATURES

§.§ Signature bases

From now on, we fix a monoid $A$ and two monomial modules over $A$, denoted $M$ and $S$,
with respective sets of monomials denoted $\basis$ and $\SIG$. A signature is an element of $\SIG$.
We are interested in computing  in $M$ while $S$ is the module of signatures.

In addition to the axioms above for the monomial module $S$, we also require that

*  $\forall a \in A, \forall \sigma \in \SIG, \forall m \in \basis, a \sigma = \sigma \text{ and } \sigma \neq 0 \Rightarrow am = m$.

*  $\forall a, b\in A, \forall \sigma \in \SIG, \forall m \in \basis, a \sigma \leq b \sigma \text{ and } \sigma \neq 0 \Rightarrow am \leq bm$.

Naturally <ref> implies <ref>, but we state them separately because <ref> will only be useful later in Section <ref> (and specifically in Lemma <ref>) when we will study algorithms for computing  and termination issues.
This hypothesis is called compatibility by GaoVolnyWang_2016 and others.

A sigpair is an element of $M\times \SIG$.
The first element of a sigpair $f$ is denoted $f^\natural$, it is the polynomial part of $f$ (eventhough $f$ may not be a polynomial, strictly speaking).
The second element of a sigpair $f$ is denoted $\sig f$, it is the signature of $f$.

For a sigpair $f$ and some $a\in A$, we define the sigpair $a f = (a f^\natural, a \sig f)$.
For $\lambda \in K^\times$, we define $\lambda f = (\lambda f^\natural, \sig g)$.
A sigset is a set of sigpairs.
For any sigset $G$, let $A G$ denote the sigset
$AG = \left\{ af \st a\in A, f \in G \right\}$.
For $\sigma\in\SIG$, let

\[ AG^{\sigma} \eqdef \left\{ \smash{af^\natural} \st a\in A \text{ and } a\sig f = \sigma \right\}, \  AG^{\leq \sigma} \eqdef \cup_{\tau \leq \sigma} AG^\tau \text{ and } AG^{< \sigma} \eqdef \cup_{\tau < \sigma} AG^\tau. \]

They are subsets of $M$, not sigsets.
Each set $\AGlt$ defines a reduction rule $\myto1_{\AGlt}$, that we denote $\myto1_G^\sigma$, the regular reduction in signature $\sigma$.
On $M\times \SIG$, we define $f \myto1_G g$ if $\sig f = \sig g$ and $f^\natural \myto1_G^{\sig f} g^\natural$.
This is the regular reduction of sigpairs.
The tail equivalence relations $\smile_G^\sigma$ and $\smile_G$ are defined similarly using $\smile_{\AGlt}$.

The following statements are direct consequences of the axioms for monomial modules.

Let $G$ be a sigset, let $\sigma\in\SIG$ and $a\in A$. Then

* for any $\tau \leq \sigma$, $AG^{\leq \tau} \subseteq AG^{\leq \sigma}$;

* for any $f\in AG^{\leq \sigma}$, $af \in AG^{\leq a\sigma}$;

* for any $f\in AG^{< \sigma}$, $af \in AG^{< a\sigma}$.

Signature-based algorithms for  actually compute something more constrained than .
A  is a sigset such that for any $\sigma \in \SIG$
the set $\AGle$ is a pivot basis.
In view of Theorem <ref>, a sigset $G$ is a  if and only if regular reduction $\to_G$ is confluent modulo tail equivalence $\smile_G$.
This concept is a refinement of the concept of , and
forgetting the signatures in a  gives a .

If $G$ is a , then $G^\natural = \left\{ \smash{f^\natural} \st f \in G \right\}$ is a .

The set $A G^\natural$ is the union of all $A G^{\leq\sigma}$, with $\sigma \in \SIG$. By construction, $A G^{\leq\sigma} \subseteq AG^{\leq\tau}$ if $\sigma \leq \tau$. So Lemma <ref> applies and shows that $A G^\natural$ is a pivot basis.

§.§ Prebases

A sigset is a prebasis if

*  $AG^0 \subseteq \left\{ 0_M \right\}$;

*  $\forall \sigma\in\SIG, \forall f, g\in AG^\sigma, \exists \lambda \in K^\times, f - \lambda g \in \LAGlt$.

Equivalently, <ref> means that any $f \in AG^\sigma$
generates the quotient space $\LAGle/\LAGlt$ as a $K$-linear space.
The concept of prebasis embodies the postulate that “two elements with the same signature are substitutable”.
A prebasis is an admissible input for signature algorithms.

A trivial choice for the set of signatures is $\SIG = \basis$.
Let $G$ be a sigset such that $\sig f = \lm f^\natural$ for any $f \in G$.
Then $G$ is a prebasis if and only if $G^\natural$ is a .
Indeed, in this case, $\LAGlt = \brack{ \smash{ag^\natural} \st a \in A, g\in G, \lm(ag) < \sigma}$.
So the condition for being a prebasis is exactly Criterion <ref> (together with <ref>) for $A G^\natural$ to be a pivot basis, that is for $G^\natural$ to be a .

There is a way to add elements to a prebasis which yields another prebasis.
To this purpose, we say that a sigset $H$ is a sigsafe extension of a sigset $G$
if $G\subseteq H$ and for any $h \in H$, there is some $f\in AG^{\sig h}$ and some $\lambda\in K^\times$ such that $h \equiv \lambda f \pmod{\LAGlt[\sig h]}$.
The problem of computing  is more formally stated as “given a sigset $G$, compute a that is a sigsafe extension of $G$”.
(Compare with the problem of computing : “given a set $G$, compute a that generates the same ideal/module as $G$”.)
Sigsafe extensions preserve many properties.

Let $G$ be a prebasis and let $H$ be a sigsafe extension of $G$.

* $\forall \sigma\in\SIG, \LAGlt = \LAXlt{H}$ and $\LAGle = \LAXle{H}$;

* $H$ is a prebasis;

* if $H'$ is a sigsafe extension of $H$, it is also a sigsafe extension of $G$.

We skip the proof, which is a simple application of Lemma <ref>.

Generalizing Example <ref>, we may construct prebasis in $M$ from a  in $S$.

Let $\phi : S \to M$ be a $K$-linear map commuting with the action of $A$.
If $H \subseteq S$ is a , then $\left\{ (\phi(h), \lm h)  \st h \in H \right\}$
is a prebasis.

Let $G = \left\{ (\phi(h), \lm h) \st h \in H \right\}$.
We first check <ref>.
Let $f \in AG^0$.
By definition, there is some $h \in H$ and $a\in A$ such that $f = \phi(ah)$
and $\lm(ah) = 0$. By <ref>, this implies $ah = 0$, so $f = 0$.

As for <ref>,
let $\sigma\in \SIG$, $f,g\in G$
and $a, b\in A$ such that $\sigma = a \sig f=b \sig g$.
By definition, there are some $h, k\in H$ such that $\lm h = \sig f$, $\lm k = \sig g$,
$f = \phi(h)$ and $g =\phi(k)$.
In particular $\sigma = \lm(ah) = \lm(bk)$.
By <ref>, there is some $\lambda\in K$ such that $ah \eqlt \lambda bk$.
By Criterion <ref> applied to the pivot basis $A H$,
we have $ah - \lambda bk  = \sum_i m\mu_i c_i l_i$ for some $\mu_i\in K$, $c_i\in A$ and $l_i \in H$ such that $\lm(c_i h_i) < \sigma$.
In particular, $af - \lambda bg = \sum_i \mu_i c_i \phi(l_i)$
and $c_i \phi(l_i) \in AG^{< \sigma}$.

As a special case of this result, we recover the following classical construction.
Given $g_1,\dotsc,g_r \in M$, we want to find a signature set $\mathcal{S}$ and signatures $\sigma_1,\dotsc,\sigma_r$
such that $\left\{ (g_i, \sigma_i) \right\}_{1\leq i \leq r}$ is a prebasis.
Then the idea, is to compute a sigsafe extension of this prebasis that is a  to obtain in the end a of the submodule generated by $g_1,\dotsc,g_r$,
by removing signatures,  Lemma <ref>.

Let $r$ be a positive integer.
Let $\SIG = \big(\basis_> \times \left\{ 1,\dotsc,r \right\} \big) \cup \left\{ 0 \right\}$, where $\basis_> = \left\{ m\in\basis \st m > 0 \right\}$.
There are two natural well-orderings on $\SIG$, called position-over-term (POT)
and term-over-position (TOP):

POT $(m, i) \leq_\SIG (n, j)$ if $i < j$ or $i=j$ and $m \leq_\basis n$;

TOP $(m, i) \leq_\SIG (n, j)$ if $m <_\basis n$ or $m=n$ and $i \leq j$.

(And $0$ is always the minimal element.)
Let $S = M^r$. For $m\in M$, let $m\otimes e_i$ denote the element $(0,\dotsc,0,m,0,\dotsc,0)$ of $S$,
where the nonzero component is at the $i$th position.
If $B$ is a basis of $M$ such that $\lm|_B$ is injective,
then $\left\{ b\otimes e_i \st b\in B, 1\leq i \leq r \right\}$
is a basis of $S$
and we define $\lm (b\otimes e_i) = (\lm b, i)$,
which extends uniquely to a map $\lm : S \to \SIG$ that turns $S$ into a monomial space.

The monoid $A$ acts on $S$ by $a(h_1,\dotsc,h_r) = (ah_1,\dotsc,ah_r)$
and this turns $S$ into a monomial module.
Moreover, <ref> and <ref>
are satisfied, so $S$ is a suitable signature module, with either the POT or the TOP ordering.
Let $\phi : S \to M$ defined by $\phi(h_1,\dotsc,h_r) = h_1+\dotsb+h_r$.

Let $g_1,\dotsc,g_r\in M$
such that each singleton set $ \left\{ g_i \right\}$ is a  – recall that it is not automatic, see Remark <ref>.
Let $H = \left\{ g_i \otimes e_i \st 1\leq i\leq r \right\}$.
Then it is easy to check that $H$ is a .
By Theorem <ref>,
this implies that

\[ G = \left\{ \left( g_i, (\lm g_i, i) \right) \st 1\leq i \leq r \right\} \]

is a prebasis such that $G^\natural = \left\{ g_1,\dotsc,g_r \right\}$.

Let $\phi : S \to M$ be a $K$-linear map commuting with the action of $A$.
Consider a subset $H\subseteq S$, $G = \left\{ (\phi(h), \lm h) \st h \in H \right\}$
and $G'$ a sigsafe extension of $G$.
Then there is a set $H'\subseteq S$ containing $H$ such that $G'  = \left\{ (\phi(h), \lm h) \st h \in H' \right\}$.

§ REWRITE BASES

We have defined
and introduced signatures.
The definition of  is a natural refinement of in the context of signatures.
Then, the definition of prebases reflects what we expect from signatures,
and it is related to .
However, we can obtain prebases for free, that is craft a signature module
and choose signatures that will turn a finite subset of $M$ into a prebasis.

In this section, we introduce . The definition is purely combinatorial, it only depends on leading monomials and signatures.
We will see that a prebasis that satisfies these combinatorial conditions is a .
Being a  is a matter of subtle arithmetic conditions.
(One cannot change the coefficients of a  and hope that it remains a . The same is true for of course,
and also prebases.)
Somehow, we can split these conditions into the prebasis property and the combinatorial properties of .
The concept was first introduced by EderRoune_2013.
It is simplified here  by removing the need for what Eder and Roune call a “rewrite order”.
(So my definition of  is actually different than their.)

§.§ Definition and basic results

For $\sigma\in \SIG$, a sigset $G$
is a  at $\sigma$ if either $AG^\sigma = \varnothing$, or there is some $\to_G$-reduced element $f \in AG$ with $\sig f = \sigma$.

A sigset $G$ is a  if it is a prebasis and a at $\sigma$ for any $\sigma\in\SIG$.

Checking if $G$ is a  at $\sigma$ involves only manipulations in $A$, $\basis$ and $\SIG$, but no operations in the base field $K$.
Moreover, if $G$ is not a  at some $\sigma$, then it is easy to compute a sigsafe extension of $G$ which is a at $\sigma$:
simply pick some $f\in AG$ with $\sig f = \sigma$, compute a $\to_G$-normal form, and insert the result into $G$.
This leads to an algorithm schema for computing (Pseudo-algorithm <ref>).

input A full prebasis $G$

output A sigsafe extension $H$ of $G$ that is a

while $G$ is not a  do
pick $\sigma\in\SIG$ such that $G$ is not a  at $\sigma$

pick $f\in AG$ with $\sig f = \sigma$  $f$ is called the reductant

$g \gets $ any $\to_G$-normal form of $f$

$G \gets G \cup \{ g \}$   $G$ is now a  at $\sigma$
return $G$

Algorithm schema for computing

There are two significant difficulties to turn this schema into an actual algorithm.
Firstly, how to check that $G$ is a ? And how to pick a signature at which $G$ is not a ? These questions are addressed in Section <ref>.
Secondly, how to ensure termination? This is addressed, in Section <ref>, under Noetherian hypotheses
and under some restrictions on the choice of $\sigma$ on line <ref>, or the choice of $f$ on line <ref>.

Before studying  in more details, we first introduce a classification of signatures.
Let $G$ be a prebasis.
For any $\sigma\in\SIG$, either $AG^\sigma = \varnothing$, this is a trivial case, or any element of $AG^\sigma$ generates the quotient $\LAGle/\LAGlt$.
In the latter case, either  every element of $AG^\sigma$ is in $\LAGlt$, if the quotient is zero-dimensional,
or no element of $AG^\sigma$ is in $\LAGlt$, if the quotient is one-dimensional.
This leaves the following categories.
A signature $\sigma\in\SIG$ is:

* an empty signature  if $AG^\sigma = \varnothing$;

* a nonempty signature  if $AG^\sigma \neq \varnothing$;

* a regular signature if is is nonempty and $AG^\sigma \cap \LAGlt = \varnothing$;

* a syzygy signature if it is nonempty and $AG^\sigma \subseteq \LAGlt$.

A nonempty signature is either regular or syzygy, as long as $G$ is a prebasis.
This classification is relative to the sigset $G$, but we check easily that it remains unchanged
under sigsafe extensions.

Let $G$ be a prebasis and let $\sigma\in\SIG$
such that $G$ is a  at any signature $\tau < \sigma$.
For any $f, g\in AG^\sigma + \LAGlt$, there is some $\lambda \in K^\times$ such that $f\tdown_G^\sigma \lambda g$.

By Lemma <ref> below, the set $\AGlt$ is a pivot basis.
Let $f, g\in AG^\sigma + \LAGlt$.  <ref> implies that there is some $\lambda\in K^\times$ such that $f-\lambda g\in \LAGlt$.
Criterion <ref> implies that $f \tdown_G^\sigma \lambda g$.

Let $G$ be a prebasis and let $\sigma\in \SIG$ such that $\AGlt$ is a pivot basis.
If $G$ is a  at $\sigma$ or if $\sigma$ is not a regular signature, then $\AGle$ is a pivot basis.

If $\sigma$ is not regular, then $\LAGle = \LAGlt$ so $\AGle$ is a pivot basis because it contains the pivot basis $\AGlt$.

So we may assume that $\sigma$ is regular and that $G$ is a  at $\sigma$
and prove that $\AGle$ is a pivot basis using Criterion <ref>.
Let $f \in \LAGle$ and let $g \in AG^\sigma$ be a $\to_G^\sigma$-reduced element (which exists because $G$ is a  at $\sigma$).
We write $f = c_1f_1+\dotsb+c_rf_r+h$ with $f_i \in AG^\sigma$, $c_i \in K$ and $h \in \LAGlt$.
For each $f_i$, there is a $\lambda_i \in K^\times$ such that $f_i - \lambda_i g \in \LAGlt$, because $G$ is a prebasis.
So $f - \mu g \in \LAGlt$, with $\mu = \sum_i c_i \lambda_i$, and Criterion <ref> implies that $f \tdown_G^\sigma \mu g$.
But $g$ is $\to_G^\sigma$-reduced, so
$f \to_G^\sigma h \smile_G^\sigma \lambda g$ for some $h\in \LAGle$.
Next, $h \to_{ \left\{ g \right\} } h - \lambda g$, because $h \eqlt \lambda g$.
And then $h - \lambda g \to_G^\sigma \nu g$, for some $\nu \in K$. But $\nu$ must be zero because $\lm(h-\lambda g) < \lm g$.
All in all,

\[ f \to_G^\sigma h \to_{ \left\{ g \right\} } h - \lambda g \to_G^\sigma 0. \]

Therefore $f \to_{\AGle} 0$ and $\AGle$ is a pivot basis, by Criterion <ref>.

Let $G$ be a prebasis and let $\sigma\in\SIG$.

* If $G$ is a rewrite basis at any regular signature $\tau < \sigma$ then $\AGlt$ is a pivot basis.

* If $G$ is a rewrite basis at any regular signature $\tau \leq \sigma$ then $\AGle$ is a pivot basis.

Both assertions are proved simultaneously by induction on $\sigma$.

Assume that $G$ is a rewrite basis at any regular signature $\tau < \sigma$.
Then the second point (applied in signatures $<\sigma$) implies that $\AGlt[\tau]$
is a pivot basis for any $\tau < \sigma$.
Lemma <ref> (applied as in Example <ref>),
implies that $\AGlt$, which is nothing but $\cup_{\tau < \sigma}\AGle[\tau]$,
is a pivot basis.

Assume that $G$ is a rewrite basis at any regular signature $\tau \leq \sigma$.
Then the first point implies that $\AGlt$ is a pivot basis.
Lemma <ref> then implies that $\AGle$ is a pivot basis.

§.§ Relation between  and

It follows immediatly from Lemma <ref> that  are .
Conversely, the only property
that a  misses to be a , is an explicit marking of syzygy signatures
by sigpairs with polynomial parts equal to zero.

Let $G\subseteq M$ be a prebasis.
$G$ is a  if and only if
$G$ is a rewrite basis at any regular signature.

Assume first that $G$ is a . Let $\sigma\in \SIG$ be a regular signature
and let us prove that $G$ is a rewrite basis at $\sigma$. Because $\sigma$ is
regular there is some $f \in AG$ with $\sig f = \sigma$.
Let $v$ be a $\to_G$-normal form of $f$,
with respect to $G$.

The signature $\sigma$ is regular, so $AG^\sigma \cap \LAGlt = \varnothing$.
In particular $f^\natural$ is not in $\LAGlt$, and thus $v^\natural$ is not zero.
Because $\AGle$ is a pivot basis, $v^\natural$ is reducible with respect to $\AGle$.
So there is some $g\in AG$ such that $\sig g \leq \sigma$ and $\lm g = \lm v$.
But $v$ is $\to_G$-reduced so $\sig g = \sigma$.
Moreover $\lm v = \lm g$, so $g$ is also $\to_G$-reduced.
So $G$ is a  at $\sigma$.

The converse follows from the follows directly from Lemma <ref>.

One step further, we state this equivalence theorem between  with explicit marking of syzygy signatures and . The proof is an easy exercise.
This statement does not hold for the original definition of  by [3.2]EderRoune_2013.
This is the main motivation for the simplified definition.

Let $G \subseteq M$ be a prebasis.
$G$ is a  if and only if the following hold:

* $G$ is a ;

* for any syzygy signature $\sigma$, there is a $\tau$ dividing $\sigma$
such that $0 \in G^\tau$.

§.§ A criterion for

There is a criterion (that we will call Faugère's criterion)
to check that a prebasis is a . It plays the same role as Buchberger's criterion plays for :
reducing a definition that involves infinitely many monomials or signatures to finitely many computations.
However, the analogy between the two criterion is rather thin.
For one, Faugère's criterion is not derived from Buchberger's one and I could not find either a derivation of Buchberger's criterion from Faugère's one.
Moreover, Faugère's criterion only involves combinatorial operations (on leading monomials and signatures) while Buchberger's criterion
involves arithmetic operations through the reductions of S-pairs.
When applying Faugère's criterion, the arithmetic side (that is how the coefficients are relevant)
is hidden in the prebasis hypothesis.

The slogan of signature-based algorithms for  is “process at most one S-pair per signature”,
an algorithmic point of view on the idea that “two elements with the same signature are substitutable”.
Going one step further, we may ask at which signature we need to process a S-pair.
In what follows, the concept of S-pair, inherited from Buchberger's algorithm, fades in favor of a study of the signatures themselves.
This approach is somewhat closer to the concept of J-pairs proposed by GaoVolnyWang_2016.

Our goal here, given a prebasis $G$, is to define a set of signatures $\Sigma(G)$ such that it is enough to check that $G$ is a  at any signature in $\Sigma(G)$ to prove that $G$ is a .
Naturally we want $\Sigma(G)$ to be as small as possible.
And as soon as we will have introduced Noetherian hypotheses, we will want $\Sigma(G)$ to be finite and computable in a combinatorial way (that is without arithmetic operations in the base field).

For a sigset $G$ and a sigpair $f$,
the critical set of $f$ modulo $G$, denoted $\Sigma(f, G)$,
is the set of all $\sigma\in \SIG$ such that:

*  $\exists a\in A, a \sig f = \sigma$ and $af$ is not $\to_G$-reduced;

*  $\forall b,c \in A, (cb \sig f = \sigma \text{ and } b \sig f < \sigma) \Rightarrow$ $bf$ is  $\to_G$-reduced.

In other words, the condition <ref> defines a subset of $\SIG$ that is closed under the action of $A$,
whereas the condition <ref> retains only some minimal elements for divisibility.
The critical set of $G$, is the set of signatures

\begin{equation*}
\label{eq:1}
\Sigma(G) \eqdef \bigcup_{f\in G} \Sigma(f, G).
\end{equation*}

There is a resemblance with the notion of critical pairs in Buchberger's criterion (see Section <ref>)
but also an important difference: critical pairs are elements of $M$, while the critical set $\Sigma(f, G)$ only contains signatures, it is a combinatorial content.
Note that $\Sigma(f, G)$ is included in the union $\cup_{g\in G} \Sigma(f, \left\{ g \right\})$
and $\Sigma(f, \left\{ g \right\})$ may be thought as the set of signatures of the possible S-pairs between $f$ and $g$. In the classical polynomial setting, $\# \Sigma(f, \left\{ g \right\}) = 1$.
In the general case, $\Sigma(f, \left\{ g \right\})$ can contain zero, one, finitely many or infinitely many elements, see Section <ref> for examples.

Let $G$ be a prebasis. If $G$ is a rewrite basis at $\sigma$ at any signature $\tau < \sigma$,
then $G$ is a  at $\sigma$ or $\sigma\in \Sigma(G)$.

Assume that $G$ is not a  at $\sigma$
and let us prove that $\sigma\in \Sigma(G)$.
We may assume that $AG^\sigma \neq \varnothing$, otherwise $G$ is a  at $\sigma$.
Let $a\in A$ and $f \in G$ such that $a \sig f = \sigma$.
We choose $f$ so that $\lm(af)$ is smallest.
By hypothesis, $af$
is not $\to_G$-reduced (otherwise $G$ is a  at $\sigma$).
Let $b \in A$ such that:

* $bf$ is not $G$-reduced;

* $\exists c\in A, cb \sig f  = \sigma$.

(These conditions are not empty, we may choose $b = a$ and $c=1_A$.)
Let $\tau = b\sig f$.
Among all possible choice of $b$, we minimize $\tau$. We check easily that this implies $\tau\in \Sigma(f, G)$.

If $\tau = \sigma$, we are done: $\sigma \in \Sigma(f, G)$.
For contradiction, assume that $\tau < \sigma$.
In particular, $G$ is a  at $\tau$. So there is some $\to_G^\tau$-reduced $g \in AG^\tau$.
By Proposition <ref>, there is $\lambda\in K^\times$ such that $g \tdown_G^\tau \lambda bf$.
Since $g$ is $\to_G^\tau$-reduced and $bf$ is not, this implies that $\lm g < \lm  (bf)$, and,
by <ref>, that
$\lm(cg) < \lm(cbf)$.
Moreover, $cb \sig f = a\sig f$, so <ref> implies that $\lm(cbf) = \lm(af)$, and therefore $\lm(cg) < \lm(af)$.
This contradicts the minimality of $\lm(af)$.

This statement will be often used in the following form.

Let $G$ be a prebasis. If $G$ is a rewrite basis at any $\sigma\in \Sigma(G)$,
then $G$ is a .

§.§ Minimal elements in

We first introduce a binary relation on the set of sigpairs.
We say that $g$ dominates $f$domination, and denote it $g \sqsubseteq f$, if one of the following holds:

*  $\exists a \in A, a  \sig g = \sig f$ and $a \lm g \leq \lm f$;

*  $\exists a \in A, a  \sig g < \sig f$ and $a \lm g = \lm f$.

The sigpairs $f$ and $g$ are $\sqsubseteq$-equivalent if $f\sqsubseteq g$ and $g\sqsubseteq f$
(which actually means that $\lm f = \lm g$ and $\sig f = \sig g$, see Lemma <ref> below.)
We say that $g \sqsubset f$ if $g \sqsubseteq f$ and $f$ is not equivalent to $g$.
A sigpair $f$ is dominant in a sigset $G$ if $f \in G$ and for any $g \in G$ such that $g \sqsubseteq f$,
we also have $f \sqsubseteq g$.
Note that the domination relation may not be transitive, although both <ref> and <ref>, considered separately,
define a transitive relation.
Note also that <ref> is the covering relation defined by [p. 454]GaoVolnyWang_2016.

The elements of a sigset that are strictly dominated are useless in a .
It is important to understand why.
The condition <ref> means that $ag$ can be used to top-reduce $f$, so $f$ will never help any sigset containing also $g$ to be a rewrite basis.
The interpretation of the condition <ref> splits into two cases.
Firstly, when $a\lm g = \lm f$, then $f$ will not help because $ag$ can serve just as well in any situation where $f$ would serve.
When $a\lm g < \lm f$, Proposition <ref> proves that $f$ will never be reduced in a rewrite basis containing $g$.

Sigpairs $f$ and $g$
are $\sqsubseteq$-equivalent if and only if $\lm f = \lm g$ and $\sig f = \sig g$.

If $f \sqsubseteq_2 g$ (meaning that $f$ and $g$ satisfy <ref>),
then the reverse domination $f \sqsubseteq g$
implies that $a \sigma < \sigma$ for some $a\in A$, in contradiction with <ref>.
Similarly, $g \sqsubseteq_2 f$ leads to a contradiction.
So we may assume that $f \sqsubseteq_1 g$ and $g \sqsubseteq_1 f$, that is,
there are $a, b\in A$ such that, on the one hand, $a \sig g = \sig f$ and $a\lm g \leq \lm f$,
and on the other hand, $b \sig f = \sig g$ and $b \lm f \leq \lm g$.
By <ref>, this implies that $\sig f = \sig g$ and $\lm f = \lm g$.

Let $G$ be a prebasis and $H$ be a sigsafe extension
such that  every element of $H$ is dominated by an element of $G$.
Let $\sigma$ be a signature such that $H$ and $G$ are  at any signature $\tau < \sigma$.
Then $H$ is a  at $\sigma$ if and only if $G$ is a at $\sigma$.

A sigsafe extension of a  is a , so one inclusion is clear.
Conversely, assume that $H$ is a  at $\sigma$.
Because $H$ is a  at $\sigma$, there are
$b\in A$ and $f \in H$ such that $b \sig f = \sigma$ and $bf$ is $\to_H$-reduced (and thus $\to_G$-reduced too).
By hypothesis, there is some $g \in G$ such that $g \sqsubseteq f$.
Since $bf$ is $\to_G$-reduced, <ref> cannot hold, so <ref> does:
there is some $a\in A$ such that $a \sig g = \sig f$ and $a\lm g \leq \lm f$.

Since $H$ is a sigsafe extension of $G$, $f \in AG^\sigma + \LAGlt$ (maybe after a scalar multiplication), by definition.
By Proposition <ref>,
there is some $\lambda \in K^\times$ such that
$bf \tdown_G \lambda bag$.
Since $bf$ is $\to_G$-reduced, this implies $\lm(bf) \leq \lm(bag)$.
Combining with the previous inequality, we obtain that $\lm(bag) = \lm(bf)$. So $bag$,
which has same leading monomial and signature as $bf$, is $\to_G$-reduced and thus $G$ is a  at $\sigma$.

Combining with Corollary <ref>, we obtain the following corollary
which may be used to reduce the number of signatures to consider when computing a .

Let $G$ be a prebasis and $H$ be a sigsafe extension
such that  every element of $H$ is dominated by an element of $G$.
If $H$ is a  at any $\sigma$ for any $\sigma\in \Sigma(G)$, then $G$ and $H$ are .

§.§ Syzygies

When a rewrite basis comes from a  in the signature module through a map $\phi : S\to M$ (see Section <ref>),
the syzygy signatures have an interpretation in terms of the kernel of $\phi$.
This is an important feature of  that can be exploited to compute efficiently colon ideals and saturations []GaoGuanVolny_2010,EderLairezMohrSafeyElDin_2022.

Let $\phi : S\to M$ be a linear map commuting with the action of $A$,
let $H\subseteq S$ be a ,
let $G = \left\{ (\phi(h), \lm h) \st h\in H \right\}$,
and $K = \left\{ h\in H \st \phi(h) = 0 \right\}$.
If $G$ is a , then $K$ is a and $\brack{AK} = \ker \phi \cap \brack{AH}$.

It is clear that $\brack{AK} \subseteq \ker \phi \cap \brack{AH}$.
Let $h \in \ker \phi \cap \brack{AH}$,
let $\sigma = \lm h$
and let us prove that there is some $k \in AK$ such that $\lm h = \lm k$.
This will prove at the same time that $K$ is a , using Criterion <ref>,
and that $\brack{AK} = \ker \phi \cap \brack{AH}$.

Because $H$ is a ,
we can decompose $h$ as $\lambda p + q$, with $p\in AH^\sigma$, $q \in \LAXlt{H}$ and $\lambda\in K^\times$ (using the first reduction step of the reduction given by Criterion <ref>).
In particular $\lambda^{-1} \phi(h) \in AG^\sigma + \LAGlt$.
Since $G$ is a  at $\sigma$, there is some $a \in A$ and $g\in G$ such that
$ag$ it $\to_G$-reduced and $a\sig g = \sigma$.
By Proposition <ref>,
we have $\phi(h) \tdown_G^\sigma \mu ag^\natural$ for some $\mu\in K^\times$.
But $\phi(h) = 0$ and $ag^\natural$ is $\to_G^\sigma$-reduced, so $ag^\natural = 0$
and therefore $g^\natural = 0$.
By definition of $H$, $g = (\phi(k), \lm k)$ for some $k\in H$.
And since $g^\natural = 0$, we have $k \in K$.
In particular, $\lm h = \sigma = \lm(ak)$.

§ ALGORITHM TEMPLATES

In all this section we assume that $M$ and $S$ are Noetherian monomial modules, which we define in Section <ref>.
This will imply the finiteness of the critical set $\Sigma(G)$ of finite sigsets $G$
as well as the existence of finite sigsafe extensions that are , for any sigsets.

As it will become clear, there is not a single algorithm for computing .
There are many possible variants, some major, such as F5 selection strategy or F4-style reduction, and some minor.
There are also many possible ways to combine them.
More than to prescribe some algorithms, the goal of this section is to highlight design principles.

Section <ref> introduces the Noetherian hypotheses.
Section <ref> studies an algorithm where signatures are processed in order,
that is when a signature is always processed after any smaller signatures.
This is a natural setting, yielding simple proofs of termination, but it does not fit all situations.
Section <ref> studies the idea of minimizing the leading mononomial of the reductant,
in the style of ArriPerry_2011 and SunWang_2011.
Again, it leads to rather simple proofs of termination, but it leaves aside other reductant selection strategy, such as the original F5 strategy.

To study algorithms where the signatures may be processed out of order
and the reductant selected (almost) freely, Section <ref>
introduces sigtrees. It is a tree whose nodes are the elements of the  being computed,
and $g$ is a child of $f$ if was obtained from a reduction a multiple of $f$.
Under mild hypotheses, sigtrees are finite (Proposition <ref>)
and this gives a very useful termination criterion (Theorem <ref>).
This criterion is put into practice in Section <ref>, to study the F5 selection strategy
with out-of-order signature processing, in Section <ref>,
to study the most general selection strategy, according to the sigtree criterion,
and in Section <ref> to study simultaneous reduction in the F4 style.

§.§ Noetherian monomial modules

A partial order $\trianglelefteq$ on a set $X$ is a well partial order (or wpo)
if for any sequence $(x_i)_{i \geq 0}$ in $X$, there are some $i < j$ such that $x_i \trianglelefteq x_j$.
A subset $T$ of a partially ordered set $X$ is closed if $a\trianglelefteq b$ and $a\in T$ imply $b\in T$.
Wpos have several equivalent characterizations.

Let $X$ be a set with a partial order $\trianglelefteq$.
The following assertions are equivalent:

* any sequence $T_0 \subseteq T_1 \subseteq \dotsc$ of closed subsets of $X$ stabilizes;

*  for any sequence $(x_i)_{i\geq 0}$ in $\SIG$, there are some $i<j$ such that $x_i \trianglelefteq x_j$;

*  for any sequence $(x_i)_{i \geq 0}$ in $\SIG$, there is a subsequence $(x_j)_{j \geq 0}$ such that $x_j \trianglelefteq x_{j+1}$ for any $j \geq 0$;

*  for any closed set $T\subseteq X$, there is finite set $B$ such that $T = \left\{ x\in X\st \exists b\in B, b \trianglelefteq x \right\}$.

A monomial set $\basis$ of a monomial module $M$ is partially ordered by divisibility,
an order that we will denote $\trianglelefteq$, not to be confused with the total order $\leq$.
Namely, $m\trianglelefteq n$ if there is some $a\in A$ such that $am = n$.
Nonetheless, if $a\trianglelefteq b$ then $a\leq b$, by <ref>.
The monomial space $M$ is Noetherian
if $\trianglelefteq$ is a wpo.
In case $M$ is a module over some algebra generated by $A$ (with the obvious compatibility hypotheses),
it is possible that $M$ is Noetherian as a module but not as a monomial module,
see Section <ref> for an example.
However, if $M$ is Noetherian as a monomial space, it is Noetherian as a module.

So we now assume that the monomial spaces $M$ and $S$ (the signature module)
are Noetherian. The first interesting consequence is the finiteness of the critical set $\Sigma(G)$ for a given finite sigset $G$.

Let $G$ be a finite sigset. If $S$ is Noetherian then $\Sigma(G)$ is finite.

Let $f\in G$.
By definition, $\Sigma(f, G)$ is the set of $\trianglelefteq$-minimal elements of some closed subset of $\SIG$.
By Criterion <ref>, it is finite.

The termination arguments will not follow from the Noetherianity of $M$ or $S$ alone,
but in conjunction.
More precisely, in $\basis \times \SIG$  we define $(m, \sigma) \trianglelefteq (n, \tau)$ if $m \trianglelefteq n$ and $\sigma \trianglelefteq \tau$.
In other words, $(m, \sigma) \trianglelefteq (n, \tau)$ if there $a, b\in A$ such that $am = n$ and $b \sigma = \tau$.
Let me insist that $a$ and $b$ may not be equal.

If $M$ and $S$ are Noetherian monomial modules, then $\trianglelefteq$ is a wpo on $\basis \times \SIG$.

Let $\big((m_i, \sigma_i)\big)_{i \geq 0}$ be an infinite sequence in $\basis\times \SIG$.
By Criterion <ref>,
we may assume, up to extracting a subsequence, that $m_i \trianglelefteq m_{i+1}$.
Similarly, we may assume, up to extracting a subsubsequence, that $\sigma_i \trianglelefteq \sigma_{i+1}$.
So $\trianglelefteq$ on $\basis\times\SIG$ satisfies Criterion <ref>.

For any sigpairs $f$ and $g$, if $(\sig f, \lm f) \trianglelefteq (\sig g, \lm g)$
then $f \sqsubseteq g$.

Let $a, b\in A$ such that $a\sig g=\sig f$ and $b\lm g = \lm f$.
If $b \sig g < \sig f$, then <ref> holds (with $b$ in place of $a$).
Otherwise, if $a \sig g = \sig f \leq b \sig g$, then <ref> implies that $a \lm g \leq b \lm g = \lm f$ (so <ref> holds), unless $\sig g = 0$. In this last case, we have $\sig f = b\sig g = 0$ and $b\lm g = \lm f$, so <ref> also holds.

The following statement will underlie all the termination proofs.
It is an analogue of Dixon's Lemma for sigpairs. However, we will see that this statement may not apply directly.
The relation $\trianglelefteq$ on $\basis\times \SIG$, the domination relation $\sqsubseteq$
and Lemma <ref> appeared
first in the work of
ArriPerry_2011,ArriPerry_2017 and they have been used several times since then

For any infinite sequence $(f_i)_{i \geq 0}$ of sigpairs, there are indices $i< j$ such that $f_i \sqsubseteq f_j$.

It is a direct corollary of Lemma <ref>, Criterion <ref> and Lemma <ref>.

§.§ Processing signatures in order

By Theorem <ref>,
we can compute the smallest signature at which a given prebasis $G$ is not a : it must be an element of the critical set $\Sigma(G)$, which is finite by Lemma <ref>.
This signature has many good properties induced by Proposition <ref>, and in particular we deduce the following one.

Let $G$ be a prebasis and let $\sigma$ such that $G$ is a  at any $\tau < \sigma$.
Let $f \in AG$ with $\sig f = \sigma$
and let $h$ be any $\to_G$-normal form of $f$.
Then $g \not\sqsubseteq h$ for any $g \in G$.

By contradiction, assume that there is some $g\in G$ such that $g\sqsubseteq h$.
Domination condition <ref> is ruled out because $h$ is $\to_G$-reduced.
Therefore <ref> holds: there is some $a\in A$ such that $a \sig g = \sigma$ and $\lm(ag) \leq \lm h$.

By minimality of $\sigma$ and Proposition <ref>,
$f \tdown_G \lambda ag$ for some $\lambda \in K^\times$.
By confluence, we also have $h \tdown_G \lambda ag$.
Since $h$ is $\to_G$-reduced, this implies that $\lm h \leq \lm(ag)$.
Combining the condition <ref>, we obtain that $\lm(ag) = \lm h$ and therefore that $ag$ is $\to_G$-reduced.
So $G$ is a  at $\sigma$, in contradiction with the hypothesis.

This leads to Algorithm <ref>.

There is no restriction whatsoever on the choice of the reductant on line <ref>,
they all reduce to the same sigpair, up to scaling and tail equivalence $\smile_G$ (Proposition <ref>).

input A finite prebasis $G$

output A finite sigsafe extension of $G$ which is a

while $G$ is not a  at all $\sigma\in \Sigma(G)$ do
$\sigma \gets \min \left\{ \sigma \in \Sigma(G) \st G \text{ is not a \rb{} at $\sigma$} \right\}$

pick any $f\in AG$ with $\sig f = \sigma$

$g \gets $ any $\to_G$-normal form of $f$

$G \gets G \cup \left\{ g \right\}$
return $G$

Computation of a  handling signatures in increasing order

Algorithm <ref> is correct and terminates.

Correction follows from Theorem <ref>.
For contradiction, assume that the algorithm does not terminate for some input.
Let $g_1,g_2,\dotsc$ be the sigpairs that are inserted to $G$ on line <ref> on each iteration.
By Proposition <ref>, there are some indice $i< j$ such that $g_i \sqsubseteq g_j$.
However, this contradicts Proposition <ref>.

This algorithm is close in essence to the original F5 algorithm Faugere_2002
and more generally to the RB algorithm of EderPerry_2011.
The notion of critical set and the notation $\Sigma(G)$ greatly simplify the presentation of the algorithm,
but it hides combinatorial computations.
For example, how to update $\Sigma(G)$ after inserting a new element?
How to find the next signature to handle? How to check the halting condition?
These questions are addressed in Section <ref>.

§.§ Minimizing the leading monomial of the reductant

Processing S-pairs in increasing order seems to be a natural option
but it is also important to understand what happens when signatures are processed in any order.
There may be various reasons to do so: parallel computing, simultaneous reduction in the F4 style []Faugere_1999.
Recently, EderLairezMohrSafeyElDin_2022 used signature algorithms to compute the saturations,
this involves enlarging the the input ideal on the fly. It can be interpreted as an algorithm processing signatures out of order.

In a time where the termination of F5 was still unsettled, ArriPerry_2011 – mind the erratum ArriPerry_2017 –
introduced the idea of choosing carefully the sigpair to be reduced, I call it the reductant, at a given signature to ensure termination.
This is based on the following observation.

Let $G$ be a prebasis and let $\sigma$ be a signature at which $G$ is not a .
Let $f \in AG$ with $\sig f = \sigma$ and $\lm f$ minimal.
Let $h$ be a $\to_G$-normal form of $f$.
Then $g \not\sqsubseteq h$ for any $g \in G$.

By contradiction, assume that there is some $g\in G$ such that $g \sqsubseteq h$.
Condition <ref> is ruled out because $h$ is $\to_G$-reduced.
Therefore <ref> holds: there is some $a\in A$ such that $a \sig g = \sigma$ and $\lm(ag) \leq \lm h$.
Besides,  $G$ is not a  at $\sigma$, it follows that $f$ is not $G$-reduced,
and thus $\lm h < \lm f$ since $f \to_G h$.
It follows that $\lm(ag) < \lm f$, which contradicts the minimality of $f$.

still requires to process signatures by increasing order,
Proposition <ref> opens the way for out-of-order signature handling,
as SunWang_2013 and GaoVolnyWang_2016 did.
The formulation that I propose (Algorithm <ref>)
is mostly equivalent to that of the latter.
The choice of signature on line <ref> is unconstrained, but the choice of the reductant is imposed.

input A finite prebasis $G$

output A finite sigsafe extension of $G$ which is a

while $G$ is not a  at all $\sigma\in \Sigma(G)$ do
pick any $\sigma\in \SIG$ such that $G$ is not a  at $\sigma$

pick $f\in AG$ with $\sig f = \sigma$ and $\lm f$ minimal

$g \gets $ any $\to_G$-normal form of $f$

$G \gets G \cup \left\{ g \right\}$
return $G$

Computation of a  with out-of-order signature processing, minimizing the leading monomial of the reductant

Algorithm <ref> is correct and terminates.

Identical to the proof of Theorem <ref>, but using Proposition <ref>
instead of Proposition <ref>.

§.§ Well-formed sigtrees

A tree is a set $\mathcal{T}$, finite or infinite, of finite sequences of nonnegative integers
such that for any $(k_1,\dotsc,k_r) \in \mathcal{T}$ (with $r \geq 1$),
the prefix subsequence $(k_1,\dotsc,k_{r-1})$ is also in $\mathcal{T}$.
The elements of $\mathcal{T}$ are called nodes.
The children of a given node $n\in \mathcal{T}$ are the sequences in $\mathcal{T}$ that extend $n$ by exactly one integer.
The root node is the empty sequence, denoted $\epsilon$, it is the only node that is not the child of another node. The set $\mathcal{T} \setminus \left\{ \epsilon \right\}$ of nonroot nodes is denoted $\mathcal{T}^+$.
The nodes are partially ordered: $n \leq_\mathcal{T} m$ if $n$ is a prefix of $m$.
For any node $n \in \mathcal{T}$, the set $\left\{ m \in \mathcal{T} \st m \leq_\mathcal{T} n \right\}$ is the set of ancestors of $n$.

A sigtree is a tree $\mathcal{T}$ together with a rank function $\rk : \mathcal{T} \to \mathbb{N}$ and a label funtion $\lambda:\mathcal{T}^+ \to M\times \SIG$
(recall that $M\times \SIG$ is the set of sigpairs).
A sigtree is a natural way to represent the process of computing a rewrite basis.
Indeed, Algorithms <ref> or <ref>, as well as Pseudo-algorithm <ref>,
produce naturally a sigtree as follows.
The elements of $G$ are the labels of a sigtree, which at the beginning of the algorithm,
is made only of the root node and one leaf for each element in the input. Then, each time some $f \in AG$ is picked,
reduced, and inserted into $G$, we can write $f = a \lambda(n)$, for some nonroot node $n$ of the sigtree,
and we insert in the sigtree a new child of $n$ containing the new element.
The rank function reflects the birthdate of a node.

A well-formed sigtree
is a sigtree $\mathcal{T}$ such that:

*  $\forall n \in \mathcal{T}^+, \forall m \text{ child of $n$}, \exists a \in A, a \sig \lambda (n) = \sig \lambda(m)$ and $a \lm \lambda(n) > \lm\lambda(m)$,

“a child is more reduced than its parent”;

$\forall n \in \mathcal{T}^+$, $\lambda(n)$ is $\to$-reduced with respect to the sigset $ \left\{ \lambda(p) \st \epsilon <_{\mathcal{T}} p <_{\mathcal{T}} n \right\}$,

“a child is reduced modulo its ancestors”;

*  $\forall n \in \mathcal{T},\forall p, q $ children of $n$, $\rk(p) < \rk(q) \Rightarrow \sig \lambda(p)$ does not divide $\sig\lambda(q)$,

“the signature of a node does not divide that of younger sibling nodes”.

Typically, <ref> and <ref> are satisfied by design if $\lambda(m)$ is obtained by reducing $a \lambda(n)$ modulo a sigset containing at least the labels of the ancestors of $m$,
and assuming that $a \lambda(n)$ is indeed reducible to account for the strict inequality in <ref>.

<ref> is the real constraint. In the context above, <ref> puts a contraint on the choice of the reductant. It means that whenever we want to reduce $a \lambda(n)$, we must first check that we have not previously computed a reduction $b \lambda(n) \to \lambda(m)$ for some child $m$ of $n$ and for some $b$ such that $\exists c\in A, cb = a$. In which case we can reduce $c \lambda(m)$ instead of $a \lambda(n)$.

Let $\mathcal{T}$ be a well-formed sigtree.
If  $\left\{ n\in \mathcal{T} \st \rk(n) = k \right\}$ is finite for any $k\in \mathbb{N}$, then $\mathcal{T}$ is finite.

Let $\mathcal{T}$ be a well-formed sigtree.
By König's lemma, it is enough to prove that $\mathcal{T}$ has no infinite branch
and that every node has at most finitely many children.

If there is an infinite branch, then there is a sequence of nodes $(n_i)_{i \geq 0}$
such that $n_{i+1}$ is a child of $n_i$.
By Proposition <ref>, there are some indices $i < j$ such that $\lambda(n_i) \sqsubseteq \lambda(n_j)$.
Condition <ref> would contradict <ref>
so Condition <ref> holds: there is some $b\in A$ such that $b\sig \lambda(n_i) = \sig \lambda(n_j)$
and $b \lm \lambda(n_i) \leq \lm \lambda(n_j)$.
By <ref> (applied all along the path from $n_i$ to $n_j$),
there is some $a \in A$ such that $a\sig \lambda(n_i) = \sig\lambda(n_j)$ and $a \lm\lambda(n_i) > \lm \lambda(n_j)$.
But <ref> implies that $a\lm \lambda(n_i) = b \lm \lambda(n_i)$, leading to a contradiction.

If a node has infinitely many children,
the hypothesis ensures that we can extract an infinite sequence of children with increasing ranks.
By Noetherianity of $S$, the signature of one child would divide the signature of another with higher rank.
This contradicts <ref>.

We will most often consider a variant of this statement.
An extension of sigtree $\mathcal{T}$ (with label function $\lambda$ and rank function $\rk$) is a sigtree $\mathcal{T}'$ (with label function $\lambda$ and rank function $\rk'$)
such that $\mathcal{T} \subseteq \mathcal{T}'$,
$\lambda'|_{\mathcal{T}^+} = \lambda$,
and $\rk'|_\mathcal{T} = \rk$.

Let $(\mathcal{T}_i)_{i \geq 0}$ be a sequence of well-formed sigtrees such that $\mathcal{T}_{i+1}$ is an extension of $\mathcal{T}_i$, for any $i \geq 0$.
If for any $r \geq 0$, the number of nodes of rank $r$ in $\mathcal{T}_i$ is finite and bounded as $i\to \infty$,
then there is some $i\geq 0$ such that $\mathcal{T}_i = \mathcal{T}_{i+1}$.

Let $\mathcal{T}_\infty = \cup_{i\geq 0} \mathcal{T}_i$, with the label function $\lambda_\infty$
uniquely defined by $\lambda_\infty |_{\mathcal{T}_i} = \lambda_i$, and the rank function defined similarly.
Since each $\mathcal{T}_i$ is well-formed, we check easily that $\mathcal{T}_\infty$
satisfies <ref>, <ref>, and <ref>.
So $\mathcal{T}_\infty$ is a well-formed sigtree.

For a given $r\in \mathbb{N}$, the number of nodes of rank $r$ in $\mathcal{T}_\infty$ is the limit of the number of nodes of rank $r$ in $\mathcal{T}_i$, which is finite, by hypothesis.
Therefore Proposition <ref> applies and shows that $\mathcal{T}_\infty$ is finite.
So there is some $i \geq 0$ such that $\mathcal{T}_i = \mathcal{T}_{i+1} = \mathcal{T}_\infty$.

§.§ The F5 reductant selection strategy

In the original presentation of F5 Faugere_2002,
Faugère proposes to choose a reductant $a f$ where, among all possible choices, $f$ is the “most recent”.
This leads to Algorithm <ref>.
This selection strategy leads naturally to a well-formed sigtree.
So we can prove that the corresponding algorithm terminates, even if signatures are handled out of order.

input A finite prebasis $G$

output A finite sigsafe extension of $G$ which is a

$R\gets $ empty dictionary mapping sigpairs to integers

$r \gets 1$

for $g\in G$ do $R[g] \gets 0$

while $G$ is not a  at all $\sigma\in \Sigma(G)$ do
pick any $\sigma\in \SIG$ such that $G$ is not a  at $\sigma$

pick some $a \in A$ and $f\in G$ such that $a \sig f = \sigma$ and $R[f]$ maximal

$g \gets $ any $\to_G$-normal form of $af$

$G \gets G \cup \left\{ g \right\}$

$R[g] \gets r$

$r\gets r+1$
return $G$

Computation of a  with out-of-order signature processing and F5 selection strategy of the reductant

Algorithm <ref> is correct and terminates.

Correctness follows from Theorem <ref>.
For termination, consider the sigtree induced by the algorithm:
each sigpair $g$ inserted into $G$ on line <ref>
is the label of a node whose parent is the node labeled with $f$,
where $f$ is the sigpair picked on line <ref>.
The rank of a node is given by $R$.

At each iteration of the algorithm, this sigtree is well-formed. <ref> and <ref> follow by construction.
To check <ref>, we observe that the rank of a node is always greater than the rank of its parent.
So, on line <ref>,
if the node corresponding to $f$ has already a child whose signature divides $\sigma$, this child has a higher rank than that of $f$,
which contradicts the maximality of $R[f]$.

The number of node of a given rank is at most one, so Theorem <ref> applies and shows that the algorithm terminates.

§.§ Explicit management of the critical set

The presentation of Algorithms <ref>, <ref> and <ref>
takes advantage of the notation $\Sigma(G)$ to abstract the handling of set of signatures to be handled
from concrete questions that theory may ignore but not practical implementations.
There is a lot of room to design a proper handling of signatures, I simply show some possible variants.

while $Q$ is not empty do
$\sigma \gets $ some element of $Q$

$Q \gets Q \setminus \left\{ \sigma \right\}$

if $f$ is $\to_G$-reducible then
$g \gets $ a $\to_G$-normal form of $f$

$G \gets G\cup \left\{ g \right\}$;
$r\gets r+1$
return G

initinitialize signature queue and sigtree
$Q \gets \varnothing$ signature queue

$T \gets $ empty list maps a node to its children

$L \gets $ empty list maps a node to its label

$R \gets $ empty list maps a node to its rank

$T[0] \gets \varnothing$ ;
$R[0] \gets 0$ ;
$L[0] \gets \cn{Null}$ the root node has no label

$n \gets 1$ ; $r\gets 1$    node and rank counters

$k\gets 0$

for $g \in G$ do create root nodes

insertnodeinsert a node with label $g$, parent $k$ and rank $r$
$L[n] \gets g$ ;
$T[k] \gets T[k] \cup \{ n\}$ ;
$R[n] \gets r$ ;
$T[n] \gets \varnothing$

$n \gets n+1$

updatequeueupdate the queue with the new relation $g$
for $h\in G$ do
$Q \gets Q \cup \Sigma(g, h) \cup \Sigma(h, g)$

selectreductantselect a reductant $f$ in signature $\sigma$ with corresponding node $k$
$k \gets 0$             start the search from the root node

for $c \in T[k]$ do
if $\sig L[c]$ divides $\sigma$ then
$k \gets c$ go down the tree

goto <ref> continue the search from the new position
pick $a\in A$ such that $a \sig L[k] = \sigma$

$f \gets a L[k]$

Computation of a , with explicit construction of a well-formed sigtree and explicit handling of the critical set

§.§.§ Base algorithm

In this section, we assume that we know how to operate on $\basis$ and $\sig$ (that is compare, test divisibility, etc.) and we assume that we have a procedure to compute the critical set $\Sigma(f, \left\{ g \right\})$ of a pair of sigpairs $f$ and $g$ (simply denoted $\Sigma(f, g)$).
Without more information on $A$, $\basis$ and $\SIG$ we cannot go further down into the details.
In the polynomial setting, the set $\Sigma(f, g)$ may contain zero or one element and its computation amounts to a few operations on monomials, see Section <ref>,

There are many ways to proceed and Algorithm <ref> is one of them.
In this algorithm, the set $Q$ contains signatures, and, at the beginning of each iteration of the “while” loop,
we have the following invariant:

\begin{equation}
\label{eq:2}
\forall \sigma \in \Sigma(G), \sigma \in Q \text{ or $G$ is a \rb{} at~$\sigma$}.
\end{equation}

Indeed, when an element $g$ is inserted in $G$, we remove $\sig g$ from $Q$
and insert all the elements in the sets $\Sigma(g, h)\cup \Sigma(h, g)$, for $h\in G$.
Since $g$ is $\to_G$ reduced,
$G\cup \left\{ g \right\}$ is a  at $\sigma$
and the inclusion

\[ \Sigma(G \cup \left\{ g \right\}) \subseteq \Sigma(G) \cup \bigcup_{h\in G} \left( \Sigma(g, h) \cup \Sigma(h, g) \right) \]

proves that Invariant (<ref>) is preserved.
With Invariant (<ref>) in hand, it is clear that when Algorithm <ref> terminates,
it returns a , by Theorem <ref>.

Termination is ensured by design: the sigtree induced by the computation is explicitely constructed, through the lists $T$, $L$, and $R$,
and the selection procedure of reductants makes it sure that the sigtree is wellformed.
Each iteration of the “while” loop either removes an element of $Q$ or increase the size of the sigtree.
The latter cannot happen infinitely many times, in view of Theorem <ref>,
so $Q$ is eventually empty and the algorithm terminates.

§.§.§ F5 variant

We can specialize the reductant selection strategy to match the one of F5, exposed in Section <ref>.
In this variant, it is not necessary to maintain the sigtree explicitely, we may ignore the list $T$.

Similar to Algorithm <ref>, except for the following chunk

selectreductantf5-variantselect a reductant $f$ in signature $\sigma$ with corresponding node $k$
$k \gets 0$

for $1\leq j < n$ do
if $\sig L[j]$ divides $\sigma$ and $R[j] > R[k]$ then
$k \gets j$
pick $a\in A$ such that $a \sig L[k] = \sigma$

$f \gets a L[k]$

Variant of Algorithm <ref> with the F5 strategy for the reductant selection

§.§.§ A variant with signature pruning

In the set $Q$, we may remove any element that is divided by a different element of $Q$.
Instead of Invariant (<ref>), we maintain the following one:

\begin{equation}
\forall \sigma\in \Sigma(G), \left( \exists \tau\in Q, \tau \text{ divides } \sigma \right) \text{ or $G$ is a \rb{} at $\sigma$}.
\end{equation}

This leads to Algorithm <ref>.
Checking correctness is an easy exercise.

Similar to Algorithm <ref>, except for the following chunk

updatequeue-variantupdate the queue with the new relation $g$
for $h\in G$ do
$Q \gets Q \cup \Sigma(g, h) \cup \Sigma(h, g)$
for $\sigma\in Q$ do
if $\exists \tau \in Q\setminus \left\{ \sigma \right\}$, $\tau$ divides $\sigma$ then
$Q\gets Q\setminus \left\{ \sigma \right\}$

Variant of Algorithm <ref> with signature pruning

§.§ Simultaneous reduction

while $Q$ is not empty do
$S \gets $ some nonempty subset of $Q$

$Q\gets Q \setminus S$

$F \gets \varnothing$ set of reductants and corresponding nodes

for $\sigma\in S$ do selection of reductants

if $f$ is $\to_G$-reducible then
$F \gets F \cup \left\{ (f, k) \right\}$ we keep the information of the parent

$N \gets \varnothing$ set of newly computed relations

for $(f, k)\in F$ by increasing order of $\sig f$ do reduction of reductants
$g^\natural \gets $ a $\to$-normal form of $f^\natural$ w.r.t. $\AGlt \cup \left\{ \smash{h^\natural} \st h\in N \right\}$

$g \gets (g^\natural, \sigma)$

$N\gets N \cup \left\{ g \right\}$ insertion of $g$ in $G$ is delayed

$G \gets G\cup N$

$r\gets r+1$
return G

Computation of a , with simultaneous reduction. Pseudocode chunks are defined in Algorithm <ref>.

As another variation of Algorithm <ref>,
we may handle several signature at a time,
in the F4 style Faugere_1999,AlbrechtPerry_2010[13]EderFaugere_2017.
This has two aspects.
The first one: the sigset $G$ that is used to compute the reductions is only updated once in a while,
not each time a new element is discovered.
The new elements are inserted in a sigset $N$
and after a bunch of signatures is handled, the elements of $N$ are inserted in $G$.
On line <ref>, the reductant $g$ is reduced with respect to $G$ (and as usual, multiples of elements of $G$ can be used in reduction steps) and also with respect to $N$ (but multiples cannot be used in reduction steps). In other words, the polynomial part $g^\natural$ is reduced modulo the set $\AGlt \cup N^{< \sigma}$.

The second aspect of simultaneous reduction is not actually shown in the pseudo-code, but it is made possible by the first point:
it is possible to perform all the reductions
in the “for” loop by to reduction to linear algebra.
This second aspect is crucial for high-performance computations but it is a transparent transformation of the algorithm: it does not change what is computed.

Algorithm <ref> is correct and terminates.

Termination is clear because the algorithm produces a well-formed sigtree,
and at each iteration, either $Q$ diminishes or the sigtree grows.
Correctness follows from Invariant (<ref>) which also holds for this algorithm,
with a slightly different argument than the one in Section <ref>.

When an element $g$ is inserted into $G$,
if $g$ is $\to_G$-reduced, then
$G\cup \left\{ g \right\}$ is a  at $\sigma$
so we may remove $\sigma$ from $Q$ without breaking the invariant.
However, due to the nature of simultaneous reduction, it may happen that we insert an element that is not $\to_G$-reduced.
In this case, then there is some $h\in G$ which reduces $g$ and we check easily that $\Sigma(g, h) = \left\{ \sig g \right\}$.
So in this case, $\sig g$ is not actually removed from $Q$ and the invariant is preserved.

§.§ Counter example for termination

Proving termination with Theorem <ref> still poses some constraint on the choice of the reductant,
even though they are compatible with classical strategies.
We cannot lift them in the axiomatic setting presented here.

Consider the polynomial algebra $R = K[w,x,y,z]$
with the lexical monomial order with $w < x < y < z$.
Let $M = R$, $A = R\setminus \left\{ 0 \right\}$
and $S = R^4$, with a position-over-term order:
the signatures are pairs $(m, i)$ made of a monomial $m\in \mathcal{M}$ and an index $i \in \left\{ 1,\dotsc,4 \right\}$,
they are compared first with respect to the index, then to the monomial.
For brevity, a pair $(m, i)$ is denoted $m\mathbf i$, or just $\mathbf i$ if $m= 1$.
Consider the input set

\[ G = G_0 = \left\{ (x-w, \mathbf 1 ), (z^2, \mathbf 2), (yz, \mathbf 3), (z-y, \mathbf 4) \right\} \]

Consider a run of Algorithm <ref> but without contraint on the choice of the reductant:
at the $i$th iteration, we choose a signature $\sigma \in \Sigma(G_{i-1})$
at which $G_{i-1}$ is not a a , choose a reductant $af \in A  G_{i-1}$
with signature $\sigma$, reduce it modulo $G_{i-1}$
and insert it into $G_{i-1}$ to form $G_i$.

Table <ref> shows an infinite run where the signature $\sigma$, the base reductant $f$ and the multiplier $a$ are all poorly chosen (Run 1).
The same table also shows a run (Run 2) where the signature $\sigma$ and the multiplier $a$ are poorly chosen (as poorly as I could) but $f$ is chosen following the F5 strategy, see Section <ref>.

$\sigma$     $f^\natural$     $\sig f$     $a$     $\TopRed(af, AG^{\sigma})$
run 1      $z\mathbf 4$     $z-y$     $\mathbf 4$     $z-y$     $z^2-2yz+y^2 \to y^2$

$xz\mathbf 4$     $z-y$     $\mathbf 4$     $x(z-y^2)$     $x z^2 - x y^2 z - xyz + xy^3 \to xy^3 \to wy^3$

$x^2z\mathbf 4$     $z-y$     $\mathbf 4$     $x^2(z-y^3)$     $x^2 z^2 - x^2 y^3z - x^2 yz + x^2y^4 \to x^2y^4 \to w^2y^4$

$x^k z\mathbf 4$     $z-y$     $\mathbf 4$     $x^k(z-y^{k+1})$     $\dotsb \to w^k y^{k+2}$

run 2      $z\mathbf 4$     $z+y$     $\mathbf 4$     $z-y^{10}$     $z^2 - z y^{10} - zy + y^{11} \to y^{11}$

$xz\mathbf 4$     $y^{11}$     $z\mathbf 4$     $x$     $xy^{11} \to wy^{11} \to 0$

$z^2\mathbf 4$     $y^{11}$     $z\mathbf 4$     $z+y^{20}$     $zy^{20} + y^{31} \to y^{31} \to 0$

$z \mathbf 3$     $yz$     $\mathbf 3$     $z+y^{30}$     $z^2 y + z y^{31} \to 0$

$x \mathbf 3$     $xyz$     $\mathbf 3$     $x$     $xyz \to wyz \to 0$

$x \mathbf 2$     $xz^2$     $\mathbf 2$     $x$     $xz^2 \to wz^2 \to 0$

Two different tentative to compute a rewrite basis from the input sigset $G_0$, see Section <ref>.

§ SETTINGS

This section describes different monomial spaces coming from different settings in computer algebra. Some are noncommutative or non-Noetherian.

§.§ Polynomial ring

Let $M = K[x_1,\dotsc,x_n]$ be the polynomial ring in $n$ variables over $K$,
which we endow with a monomial order, so the function $\lm$ is well defined.
Let $A = \left\{ \smash{x_1^{i_1}\dotsb x_n^{i_n}} \st i_1,\dotsc,i_n \in \mathbb{N} \right\}$.
The axioms for monomial orders ensure that $M$ is a monomial module over $A$.
It is Noetherian.
Moreover, it satisfies the extra property <ref>,
so construction of prebases is easy, see Remark <ref>.

For sigpairs $f$ and $g$, the critical set $\Sigma(f, g)$ has zero or one element.
There is the trivial case where $f^\natural = 0$ or $g^\natural = 0$. In this case, every multiple of $f$ is $\to_{ \left\{ g \right\}}$-reduced, so $\Sigma(f, g) = \varnothing$.
When $f^\natural$ and $g^\natural$ are both nonzero,
there are monomials $a, b\in A$ such that $a\lm f = b \lm g = \mop{lcm}(\lm f, \lm g)$.
Then there are two cases, if $a \sig f \leq b \sig g$, then $\Sigma(f, \left\{ g \right\}) = \varnothing$;
on the contrary, if $b \sig g < a \sig f$, then $\Sigma(f, g) = \left\{ a\sig f \right\}$.

Note that we could also choose the monoid $A = K[x_1,\dotsc,x_n]$.

§.§ Modules over polynomial rings

Let $r$ be a positive integer and let $M = K[x_1,\dotsc,x_n]^r$,
which we endow with a term ordering – typically position-over-term, term-over-position, or Schreyer's order [1.4]KreuzerRobbiano_2000.
The monoid $A$ is the same as before.
$M$ is a Noetherian monomial module and satisfies the extra condition <ref>.

The computation of $\Sigma(f, g)$ is slightly different.
In the case where $f^\natural$ and $g^\natural$ are both nonzero, it may happen that no multiple of $\lm f$ and $\lm g$ coincide. Indeed, nonzero monomials in $\basis$ have an index in $ \left\{ 1,\dotsc,r \right\}$
which is unchanged under multiplication.
Therefore, if $f^\natural = 0$ or $g^\natural = 0$, or $\lm f$ and $\lm f$ have different indices, then $\Sigma(f, g) = \varnothing$.
Otherwise, there are monomial $a, b\in A$ such that $a\lm f = b\lm g$ (and $a\lm f$ minimal).
Depending on the comparison of $a\sig f$ and $b\sig g$, $\Sigma(f, g)$ is either $\varnothing$ or $\left\{ a\sig f \right\}$, as in the polynomial case.

§.§ Monoid algebras

Let $A$ be a submonoid of
$\left\{ \smash{x_1^{i_1}\dotsb x_n^{i_n}} \st i_1,\dotsc,i_n \in \mathbb{N} \right\}$
and let $M = K[A]$ be the ring of polynomials whose monomials are contained in $A$.
It is clear that $M$ is a Noetherian monomial module over $A$.
This case includes the “semigroup algebras” studied by BenderFaugereTsigaridas_2019.
It also includes some algebras that are interesting in singularity theory such that $K[x^2, xy, y^2]$,
that are polynomial ring with finitelty many monomials removed (in this case $x$, $y$, and $xy$).

The critical set $\Sigma(f, g)$ can contain more than one element.
Assume, for example, that $M = K[x^2, xy, y^2]$ – that is $A = \left\{ x^i y^j \st i+j \geq 2 \right\}$ –
and that $f^\natural = x^2$ and $g^\natural = xy$.
The set of all $a\in A$ such that $\lm(af^\natural)$ is divided by $\lm(g^\natural)$
is generated by $xy$ and $y^2$. It is not generated by $y$ because $y$ is not in $A$.
Assuming that $xy\sig f > x^2 \sig g$ and $y^2 \sig f > xy \sig g$, we have

\[ \Sigma(f, g) = \left\{ xy \sig f, y^2\sig f \right\}. \]

§.§ Weyl algebras

Let $M = K\langle x_1,\dotsc, x_n, \partial_1,\dotsc,\partial_n \rangle$ be the Weyl algebra on $n$ variables.
It is noncommutative.
We may define it as the subalgebra of $\mop{End}_K( K[X_1,\dotsc,X_n] )$
where $x_i$ is the multiplication by $X_i$ and $\partial_i$ is the differentiation with respect to $X_i$.
Concretely, $x_i x_j = x_j x_i$, $\partial_i \partial_j = \partial_j \partial_i$,
$\partial_i x_j = x_j \partial_i$ (if $i\neq j$)
and $\partial_i x_i = x_i \partial_i + 1$.
A basis of $M$ is given by the monomials $x_1^{i_1}\dotsb x_n^{i_n} \partial_1^{j_1} \dotsb \partial_n^{j_n}$
and we can consider the same monomial orderings as we would do for a commutative polynomial ring in $2n$ variables.

For the monoid $A$, we cannot choose the set of monomials because it is not closed under multiplication.
We choose instead $A$ to be the submonoid of $M$ generated by $x_1,\dotsc,x_n$ and $\partial_1,\dotsc,\partial_n$.
We could also choose $A = M$.
This turns $M$ into a Noetherian monomial module with the extra property <ref>,
so we can construct signature modules with Remark <ref>.
We could also choose $A$ to be the monoid of nonzero elements of $R$.
In spite of the noncommutativity, things behave similarly to the polynomial case.
It is in fact quasicommutative: for any $a, b \in M$, $\lm(ab) = \lm(ba)$.

§.§ Localization of Weyl algebra

Let $f \in K[X_1,\dotsc,X_n]$
be a non constant polynomial.
We consider $M$ to be the Weyl algebra as above, but with an extra variable $T$ which we think of as $1/f$.
So we have the following commutation rules: $x_i T= T x_i$ and $\partial_i T = T \partial_i - \frac{\partial f}{\partial x_i} T^2$.
The monomials $x_1^{i_1}\dotsb x_n^{i_n} \partial_1^{j_1} \dotsb \partial_n^{j_n} T^k$
form a basis of $M$.
We choose $A$ to be the submonoid of $M$ generated by $T$, $x_1,\dotsc,x_n$ and $\partial_1,\dotsc,\partial_n$.
If we choose a monomial ordering that considers first the total degree with respect to $\partial_1,\dotsc,\partial_n$, we are in a quasicommutative setting, $M$ is a Noetherian monomial module
and behaves similarly to the polynomial case.

However, for computing saturations, we may want to consider an elimination order for $T$, so we compare first the degree with respect to $T$.
In particular, we obtain that the leading monomial of $T \partial_i$ is $\lm \left( \frac{\partial f}{\partial x_i} \right) T^2$, it is not $\partial_i T$.
The action of $A$ on $\basis$ is well defined by the formula $a \lm(f) = \lm(af)$, but it is not given by adding the exponents.
Yet, $M$ is a monomial module. It is not Noetherian, even though $M$ is Noetherian as a ring, or even as a module over the Weyl algebra. It does not satisfy the extra condition <ref>.

§.§ Differential algebras

Let $M = K[t, x_0, x_1, x_2, \dotsc]$,
a polynomial ring in infinitely many variables
with a derivation defined by $t' = 1$ and $x_i' = x_{i+1}$.
Let $W = M\langle \partial \rangle$
be the subalgebra of $\mop{End}_K M$ where $M$ acts by multiplication
and $\partial$ be the derivation, similarly to the Weyl algebra case.
This turns $M$ into a left $W$-module
and differential ideals are defined to be the submodules of $M$.
We choose on $M$ a lexicographic ordering with $t < x_0 < x_1$...

We choose $A$ to be the monoid generated by $\partial, t, x_0, x_1$...
This turns $M$ into a monomial module. It is quasicommutative (that is $\lm(abm) = \lm(bam)$ for any $a,b\in W$ and $m\in M$) but not Noetherian.
However, it satisfies the extra condition <ref>
and the critical sets $\Sigma(f, G)$ are finite.
This example extends to several independent variables and several function variables.

§.§ Free algebras

Let $M$ be the free algebra generated by $n$ variables $x_1,\dotsc,x_n$.
A basis of $M$ is given by the set of words in $x_1,\dotsc,x_n$.
A monomial order may be given, for example, by comparing the degree first and then the lexicographic order.
We choose $A$ to be the monoid of words, which acts naturally on $M$ by left multiplication.
In this way we may deal with left ideals in $M$.
To deal with two-sided ideals of $M$, we choose $A$ to be the set of pairs of words, with the composition $(a, b) (a', b') = (aa', b'b)$
and the action on $M$ given by $(a, b)m = amb$.

In both cases, $M$ is a monomial module with the extra condition <ref>, but not Noetherian.
In the one-sided case, the critical sets are finite, but they are not in the two-sided case.
However, in the two-sided case, the critical sets contain only finitely many nonsyzygy signatures HofstadlerVerron_2022.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

journaltitleJ. Symb. Comput.
titleThe F5 Criterion Revised

journaltitleJ. Symb. Comput.
titleCorrigendum to “The F5 Criterion Revised”

seriesGraduate Texts in Mathematics
shorttitleGröbner Bases
titleGröbner Bases: A Computational Approach to Commutative Algebra

journaltitleProc. ISSAC 2019
shorttitleGröbner Basis over Semigroup Algebras
titleGröbner Basis over Semigroup Algebras: Algorithms and Applications for Sparse Polynomial Systems

journaltitleProc. ISSAC 2021
titleMsolve: A Library for Solving Polynomial Systems

journaltitleJ. Symb. Comput.
titleThe Magma Algebra System I: The User Language

Insbruck University

titleEin Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal

journaltitleJ. Symb. Comput.
seriesLogic, Mathematics and Computer Science: Interactions in Honor of Bruno Buchberger (60th Birthday)
shorttitleBruno Buchberger’s PhD Thesis 1965
titleAn Algorithm for Finding the Basis Elements of the Residue Class Ring of a Zero Dimensional Polynomial Ideal

seriesUndergraduate Texts in Mathematics
titleIdeals, Varieties, and Algorithms

titleSingular 4-3-0 — A Computer Algebra System for Polynomial Computations

journaltitleJ. Symb. Comput.
titleA Survey on Signature-Based Algorithms for Computing Gröbner Bases

titleA Signature-Based Algorithm for Computing the Nondegenerate Locus of a Polynomial System

journaltitleProc. ISSAC 2011
titleSignature-Based Algorithms to Compute Gröbner Bases

journaltitleProc. ISSAC 2013
titleSignature Rewriting in Gröbner Basis Computation

journaltitleJ. Pure Appl. Algebra
titleA new efficient algorithm for computing Gröbner bases $(F_4)$

World Scientific

eventtitleProceedings of the Fifth Asian Symposium (ASCM 2001)
journaltitleComput. Math.
titleFinding All the Solutions of Cyclic 9 Using Gröbner Basis Techniques

journaltitleProc. ISSAC 2002
titleA new efficient algorithm for computing Gröbner bases without reduction to zero ($F_5$)

journaltitleCRYPTO 2003
titleAlgebraic Cryptanalysis of Hidden Field Equation (HFE) Cryptosystems Using Gröbner Bases

journaltitleProc. ISSAC 2010
titleA New Incremental Algorithm for Computing Groebner Bases

issn0025-5718, 1088-6842
journaltitleMath. Comp.
titleA New Framework for Computing Gröbner Bases

journaltitleSymp. Symb. Algebr. Comput.
seriesSYMSAC '86
titleBuchberger's Algorithm and Staggered Linear Bases

journaltitleJ. Symb. Comput.
titleOn an Installation of Buchberger's Algorithm

journaltitleJ. Symb. Comput.
titleExtended F5 Criteria

World Scientific Publishing Co.

journaltitleJ. Algebra Appl.
titleOn the Construction of Staggered Linear Bases

journaltitleProc. Lond. Math. Soc.
titleOrdering by Divisibility in Abstract Algebras

journaltitleJ. Symb. Comput.
titleSignature Gröbner Bases, Bases of Syzygies and Cofactor Reconstruction in the Free Algebra

journaltitleJ. ACM
titleConfluent Reductions: Abstract Properties and Applications to Term Rewriting Systems

titleComputational Commutative Algebra 1

journaltitleProc. ISSAC 1992
titleGröbner Bases Computation Using Syzygies

journaltitleProc. PASCO 2015
titleA Compact Parallel Implementation of F4

Cambridge University Press

seriesEncyclopedia of Mathematics and Its Applications
titleSolving Polynomial Equation Systems

journaltitleProc. ISSAC 2012
titlePractical Gröbner Basis Computation

journaltitleActa Appl. Math.
titleMethods for Computing in Algebraic Geometry and Commutative Algebra

titleSolving Detachability Problem for the Polynomial Ring by Signature-Based Groebner Basis Algorithms

journaltitleSci. China Math.
titleA New Proof for the Correctness of the F5 Algorithm

journaltitleProc. ISSAC 2012
titleA Signature-Based Algorithm for Computing Gröbner Bases in Solvable Polynomial Algebras

journaltitleJ. Symb. Comput.
titleHilbert Functions and the Buchberger Algorithm

seriesTexts & Monographs in Symbolic Computation
titlePolynomial Algorithms in Computer Algebra