Beyond F5 and GVW: The Proper-Cover Algorithm for
Fast Ideal Basis Computation
July 10, 2026
Gröbner basis computation incurs heavy computational overhead, especially under lexicographic order. F5 and its GVW variant dominate efficient field-based Gröbner basis solving. The proper basis algorithm offers a parameterized ideal computation framework without leveraging modern signature-based optimizations. This work presents the Proper-Cover algorithm for zero-dimensional polynomial ideals by combining GVW’s cover optimization over signature with the proper basis theory. We generalize signature, cover, POT ordering, reduction and S-pair concepts to parameterized coefficients, design a two-phase algorithm with compatible factor construction and hungry refinement, and rigorously prove termination and output correctness. Accordingly, we propose a new framework for the efficient computation of polynomial ideal bases. Benchmark results show that Proper-Cover surpasses F5 under all monomial orderings and delivers clear speedups over GVW for lexicographic (plex) order.
Since Buchberger introduced his celebrated algorithm in his seminal PhD thesis, the theory of Gröbner bases has become a standard tool in computer algebra. However, the computation of Gröbner bases is often plagued by high complexity, especially with respect to the lexicographic order. Up to the present, Faugère’s F5 algorithm[1], [2] and its extended variants remain the most efficient approaches for computing Gröbner bases in practice. The GVW algorithm[3] revises and optimizes the cover mechanism inherent to F5, yielding drastically enhanced computational efficiency.
While Gröbner bases over a field have been generalized to settings over rings, especially principal ideal rings[4]–[6], these ring-based generalizations have not yet been applied to improve the computation of polynomial ideals over a field. The proper basis algorithm[7] defines and computes an ideal basis over variables \(\boldsymbol{\tilde{x}}=(x_2,\dots,x_n)\) with the least variable \(x_1\) acts as a parameter within the polynomial algebra \(K[x_1][\boldsymbol{\tilde{x}}]\). It outperforms Faugère’s F4 algorithm, Buchberger’s classical algorithm and Möller’s algorithm.
Theorem 1 (Main result). For every zero-dimensional input ideal \(I=\subset K[x_1][\boldsymbol{\tilde{x}}]\), the Proper-Cover algorithm terminates and outputs pairs \((q_j,\mathrm B_{q_j})\) such that the eliminant \(\chi=\prod_jq_j\) and \[\langle \operatorname{LT}(\pi_{q_j}(I))\rangle = \langle \operatorname{LT}(\mathrm{B}_{q_j})\rangle \quadin (K[x_1]/(q_j))[\boldsymbol{\tilde{x}}] \quadfor every j. \label{eq:intro-main-leading-term-equality}\qquad{(1)}\] Consequently, \(\mathcal{B}:=\bigcup_j(\mathrm{B}_{q_j}\cup\{q_j\})\) is a proper basis of \(I\).
In this paper we combine the GVW algorithm and the proper basis algorithm to develop the Proper-Cover algorithm. It delivers better computational performance than Faugère’s F5 algorithm for all monomial orderings, and clearly outperforms the GVW algorithm under lexicographic (plex) ordering.
In Section 2, we extend the notions of signature, cover and POT monomial ordering from the setting of base fields to parameterized coefficients over a principal ideal domain (PID). Within this section, we formalize the definitions of proper basis and regular reduction, and introduce \(S\)-pairs and semi-\(S\)-pairs as extensions of classical \(S\)-polynomials.
In Section 3, we introduce our two-phase algorithm consisting of Algorithm [alg:propercover-stage1] and Algorithm [alg:hungry-refinement]. Relying on this two-phase algorithm, we further introduce the notion of compatible factors.
In Section 4, we establish theoretical soundness of our Proper-Cover algorithm: termination and correctness of its output proper basis. We additionally demonstrate that the compatible factors generated by Algorithm [alg:propercover-stage1], combined with the hungry refinement from Algorithm [alg:hungry-refinement], produce the valid eliminant. The core insight in Lemma 2 is that the generalized cover together with regular reduction over semi-\(S\)-pairs enable us to represent all standard \(S\)-pairs in terms of the prebasis and pre-eliminants output by the first-stage algorithm.
We conduct extensive benchmark tests in Section 5 to benchmark our Proper-Cover algorithm alongside the GVW and F5 algorithms. Empirical evidence verifies that our method surpasses F5 across every monomial ordering, and exhibits clear performance advantages over GVW when lexicographic (plex) momomial ordering is used.
Let \(K\) be a field and let \(\boldsymbol{\tilde{x}}=(x_2,\ldots,x_n)\). We treat \(K[x_1,x_2,\ldots,x_n]\) as \(K[x_1][\boldsymbol{\tilde{x}}]\). The ideal \(I=\langle f_1,\ldots,f_m\rangle\subset K[x_1][\boldsymbol{\tilde{x}}]\) is zero-dimensional. Set \[\operatorname{Mon}(\boldsymbol{\tilde{x}})=\{\boldsymbol{\tilde{x}}^\alpha:\alpha\in\mathbb{N}^{n-1}\}.\] For a nonconstant \(q\in K[x_1]\), let \[\pi_q:K[x_1][\boldsymbol{\tilde{x}}]\longrightarrow (K[x_1]/(q))[\boldsymbol{\tilde{x}}] \label{eq:projection-mod-q}\tag{1}\] be the natural projection. Fix a monomial order \(\prec\) on \(\operatorname{Mon}(\boldsymbol{\tilde{x}})\). For \[f=\sum_\alpha c_\alpha(x_1)\boldsymbol{\tilde{x}}^\alpha\in R[\boldsymbol{\tilde{x}}], \qquad R\in\{K[x_1],K[x_1]/(q)\},\] set leading monomial \(\operatorname{lm}(f)\in\operatorname{Mon}(\boldsymbol{\tilde{x}})\), leading coefficient \(\operatorname{lc}(f)\in R\), and leading term \(\operatorname{lt}(f)=\operatorname{lc}(f)\operatorname{lm}(f)\). For \(B\subset R[\boldsymbol{\tilde{x}}]\), set \(\operatorname{LT}(B)=\{\operatorname{lt}(b): b\in B\setminus\{0\}\}\); thus \(\langle\operatorname{LT}(B)\rangle\) denotes the ideal generated by the leading terms of the elements of \(B\) in \(K[x_1][\boldsymbol{\tilde{x}}]\).
Definition 1 (Eliminant, multiplicity, and proper basis). For a zero-dimensional polynomial ideal \(I\subset K[x_1][\boldsymbol{\tilde{x}}]\), let \(\chi\) denote the monic generator of the principal ideal \(I\cap K[x_1]\); thus \(I\cap K[x_1]=(\chi)\). We call \(\chi\) the eliminant* of \(I\). For an irreducible factor \(p\) of a univariate polynomial \(a\in K[x_1]\setminus K\), define \[\operatorname{mult}_p(a):=\max\{i\in\mathbb{N}:\;a\in(p^i)\}.\]*
A modular basis* with respect to a nonconstant divisor \(q\mid\chi\) is a finite set \[\mathrm{B}_q\subset I_q:=\pi_q(I)\subset(K[x_1]/(q))[\boldsymbol{\tilde{x}}]\] such that \[\langle \operatorname{LT}(I_q)\rangle = \langle \operatorname{LT}(\mathrm{B}_q)\rangle \quadin (K[x_1]/(q))[\boldsymbol{\tilde{x}}]. \label{eq:proper-basis-leading-term-ideal}\tag{2}\] Let \(\Omega\) be a finite set of pairwise coprime nonconstant factors such that \(\chi=\prod_{q\in\Omega}q\). If \(\mathrm{ B}_q\) is a modular basis with respect to \(q\), then we define the following set: \[\mathcal{B}=\bigcup_{q\in\Omega}\bigl(\mathrm{B}_q\cup\{q\}\bigr)\] and call \(\mathcal{B}\) a proper basis of \(I\).*
Let \(F=(f_1,\ldots,f_m)\). It defines \[\varphi:(K[x_1][\boldsymbol{\tilde{x}}])^m\to K[x_1][\boldsymbol{\tilde{x}}], \qquad \varphi(\mathbf{u})=\sum_{i=1}^m u_i f_i \quadfor \mathbf{u}=(u_1,\ldots,u_m) \in (K[x_1][\boldsymbol{\tilde{x}}])^m. \label{eq:module-map}\tag{3}\] Let \((K[x_1][\boldsymbol{\tilde{x}}])^m\) have standard basis \(\mathbf{E}_1,\ldots,\mathbf{E}_m\). A term of \((K[x_1][\boldsymbol{\tilde{x}}])^m\) has the form \(c_\alpha\boldsymbol{\tilde{x}}^\alpha \mathbf{E}_i\), where \(c_\alpha\in K[x_1]\setminus\{0\}\). Its coefficient is \(c_\alpha\), and its monomial is \(\boldsymbol{\tilde{x}}^\alpha \mathbf{E}_i\). A labelled pair is an element \[\boldsymbol{f}=(\mathbf{u},f)\in(K[x_1][\boldsymbol{\tilde{x}}])^m\times K[x_1][\boldsymbol{\tilde{x}}] \quad \text{such that} \quad \varphi(\mathbf{u})=f.\] Denote the polynomial part of \(\boldsymbol{f}\) by \(\operatorname{poly}(\boldsymbol{f})=f\). If \(f=0\), then \(\boldsymbol{f}\) is a syzygy; otherwise it is an ideal element equipped with a module representation.
Definition 2 (POT order, signature). The POT order \(\prec_{\scriptscriptstyle \mathrm{POT}}\) on term \(c_\alpha\boldsymbol{\tilde{x}}^\alpha \mathbf{E}_i\) is defined by \[c_\alpha\boldsymbol{\tilde{x}}^\alpha \mathbf{E}_i\prec_{\scriptscriptstyle \mathrm{POT}}c_\beta\boldsymbol{\tilde{x}}^\beta \mathbf{E}_j \quad\Longleftrightarrow\quad i<j,\;ori=jand\boldsymbol{\tilde{x}}^\alpha\prec\boldsymbol{\tilde{x}}^\beta .\] For a labelled pair \(\boldsymbol{f}=(\mathbf{u},f)\), define its signature* as the leading term of \(\mathbf{u}\) under the POT order by \[\operatorname{sig}(\boldsymbol{f})=\operatorname{lt}_{\prec_{\scriptscriptstyle \mathrm{POT}}}(\mathbf{u})=c_\alpha\boldsymbol{\tilde{x}}^\alpha \mathbf{E}_i,\qquad c_\alpha\in K[x_1]\setminus\{0\}. \label{eq:signature-definition}\tag{4}\] Thus the leading coefficient and leading monomial of \(\operatorname{sig}(\boldsymbol{f})\) are \[\operatorname{lc}(\operatorname{sig}(\boldsymbol{f}))=c_\alpha, \qquad \operatorname{lm}(\operatorname{sig}(\boldsymbol{f}))=\boldsymbol{\tilde{x}}^\alpha \mathbf{E}_i.\]*
Definition 3 (\(S\)-pair and semi-\(S\)-pair). Let \(\boldsymbol{f}=(\mathbf{u},f)\) and \(\boldsymbol{g}=(\mathbf{v},g)\) denote labelled pairs with nonzero polynomial parts. We define \(M=\operatorname{lcm}(\operatorname{lm}(f),\operatorname{lm}(g))\) and set \(t_f=M/\operatorname{lm}(f)\), \(t_g=M/\operatorname{lm}(g)\). Similarly, let \(L=\operatorname{lcm}(\operatorname{lc}(f),\operatorname{lc}(g))\), and define \(\lambda_f=L/\operatorname{lc}(f)\), \(\lambda_g=L/\operatorname{lc}(g)\).
We define \[\boldsymbol{S} (\boldsymbol{f},\boldsymbol{g})=\lambda_ft_f\boldsymbol{f}-\lambda_gt_g\boldsymbol{g} \label{eq:proper32s-polynomial}\qquad{(2)}\] as the \(S\)-pair* of \(\boldsymbol{f}\) and \(\boldsymbol{g}\). And we define its polynomial part \(\operatorname{poly}(\boldsymbol{S}(\boldsymbol{f},\boldsymbol{g}))\) as the \(S\)-polynomial of \(f\) and \(g\) and denote it as \(S(f,g)\).*
We call \(\lambda_ft_f\boldsymbol{f}\) a semi-\(S\)-pair* if \(\operatorname{sig}(\boldsymbol{S} (\boldsymbol{f},\boldsymbol{g}))=\lambda_f t_f\operatorname{sig}(\boldsymbol{f})\), and vice versa for \(\lambda_gt_g\boldsymbol{g}\). Otherwise we do not define any semi-\(S\)-pair for \(\boldsymbol{f}\) and \(\boldsymbol{g}\) when \[\operatorname{sig}(\boldsymbol{S} (\boldsymbol{f},\boldsymbol{g})) \prec_{\scriptscriptstyle \mathrm{POT}} \max\{\lambda_f t_f\operatorname{sig}(\boldsymbol{f}),\lambda_g t_g\operatorname{sig}(\boldsymbol{g})\},\] in which case we call \(\boldsymbol{S}(\boldsymbol{f},\boldsymbol{g})\) a singular \(S\)-pair .*
In particular, when \(g\in K[x_1]\), we take \(\operatorname{lm}(g)=1\), \(M=\operatorname{lm}(f)\), \(\operatorname{lc}(g)=g\), \(L=\operatorname{lcm}(\operatorname{lc}(f),g)\), \(\lambda_f=L/\operatorname{lc}(f)\) and \(\lambda_g=L/g\). Then \[S(f,g)=\lambda_f(f-\operatorname{lm}(f)) =\frac{g(f-\operatorname{lm}(f))}{\gcd(\operatorname{lc}(f),g)}.\] In this case we call \(\gcd(\operatorname{lc}(f),g)\) the special multiplier* of the \(S\)-pair.*
Definition 4 (Term reduction and least multiplier). Let \(\boldsymbol{f}=(\mathbf{u},f), \boldsymbol{g}=(\mathbf{v},g)\) be labelled pairs, with \(f\ne0\). Suppose that a term \(c_\alpha\boldsymbol{\tilde{x}}^\alpha\) of the polynomial \(f\) satisfies \(\operatorname{lm}(g)\mid \boldsymbol{\tilde{x}}^\alpha\). The multipliers are \[\lambda=L/c_\alpha,\quad \mu=L/\operatorname{lc}(g), \quad \text{where} \quad L=\operatorname{lcm}(c_\alpha,\operatorname{lc}(g)). \label{eq:least-multiplier-identity}\qquad{(3)}\] Under the condition that \(\operatorname{sig}(t\boldsymbol{g})\prec_{\scriptscriptstyle \mathrm{POT}}\operatorname{sig}(\boldsymbol{f})\) with the monomial \(t\) satisfying \(\boldsymbol{\tilde{x}}^\alpha=t\operatorname{lm}(g)\), we use the following two kinds of regular term reductions.
The proper term reduction* is \[\boldsymbol{f}'=\lambda \boldsymbol{f}-\mu t \boldsymbol{g}.\] The term \(c_\alpha\boldsymbol{\tilde{x}}^\alpha\) is cancelled in \(\operatorname{poly}(\boldsymbol{f}')\), and \(\lambda\) is the least multiplier.*
For a nonconstant \(p\in K[x_1]\), if we allow the above term reduction only when \(\gcd(\lambda,p)=1\), then we call it the hungry term reduction* with respect to \(p\).*
Definition 5 (Reduced labelled pair). Let \(\boldsymbol{f}=(\mathbf{u},f)\) be a labelled pair with \(f\in R[\boldsymbol{\tilde{x}}]\), let \(B\) be a set of labelled pairs with nonzero polynomial parts in \(R[\boldsymbol{\tilde{x}}]\), and let \(p\in K[x_1]\) be irreducible. The labelled pair \(\boldsymbol{f}\) is properly (hungrily) reduced* with respect to \(B\) (and \(p\)) if \(\boldsymbol{f}\) admits no proper (hungry) term reduction by an element of \(B\) (with respect to \(p\)).*
Definition 6 (Regular reduction). Let \(\boldsymbol{f}=(\mathbf{u},f)\) be a labelled pair, and let \(B=\{\boldsymbol{b}_j=(\mathbf{u}_j,b_j):1\le j\le s\}\) be a finite set of labelled pairs. A regular reduction* of \(\boldsymbol{f}\) with respect to \(B\) is an identity of labelled pairs \[\label{eq:regular-reduction} \lambda\boldsymbol{f}=\sum_{j=1}^{s}q_j\boldsymbol{b}_j+\boldsymbol{r}\tag{5}\] with \(\operatorname{sig}(q_j\boldsymbol{b}_j) \prec_{\scriptscriptstyle \mathrm{POT}}\operatorname{sig}(\boldsymbol{f})\) for \(1\le j\le s\), where \(\lambda\in K[x_1]\setminus\{0\}\), \(q_j\in K[x_1][\boldsymbol{\tilde{x}}]\), and \(\boldsymbol{r}=(\mathbf{v},r)\) is reduced with respect to \(B\). Moreover, their polynomial parts are required to satisfy \[\operatorname{lm}(f)= \max\left\{ \max_{1\le j\le s}\{\operatorname{lm}(q_jb_j)\}, \operatorname{lm}(r) \right\}. \label{eq:leading-monomial-condition}\tag{6}\] Here \(\lambda\) is a product of the least multipliers for the corresponding term reductions.*
A regular reduction can be a proper (hungry) reduction that consists of proper (hungry) term reductions.
For monomials \(\boldsymbol{\tilde{x}}^{\alpha} \mathbf{E}_i\) and \(\boldsymbol{\tilde{x}}^{\beta}\mathbf{E}_j\), the divisibility relation \(\boldsymbol{\tilde{x}}^{\alpha}\mathbf{E}_i\mid \boldsymbol{\tilde{x}}^{\beta}\mathbf{E}_j\) means that \(i=j\) and \(\boldsymbol{\tilde{x}}^{\alpha}\mid \boldsymbol{\tilde{x}}^{\beta}\) in \(\operatorname{Mon}(\boldsymbol{\tilde{x}})\).
Definition 7 (proper cover and hungry cover). Let \[\boldsymbol{f}=(\mathbf{u},f), \qquad \boldsymbol{g}=(\mathbf{v},g)\] be labelled pairs, with \(f\ne0\). The pair \(\boldsymbol{f}\) is properly covered* by \(\boldsymbol{g}\) over the PID \(K[x_1]\) if the following conditions hold.*
\(\operatorname{lm}(\operatorname{sig}(\boldsymbol{g}))\mid\operatorname{lm}(\operatorname{sig}(\boldsymbol{f}))\).
Either \(g=0\), or \(\operatorname{lm}(\tau g)\prec\operatorname{lm}(f)\).
Let \(\operatorname{sig}(\boldsymbol{f})=c_f\boldsymbol{\tilde{x}}^\alpha \mathbf{E}_i\) and \(\operatorname{sig}(\boldsymbol{g})=c_g\boldsymbol{\tilde{x}}^\beta \mathbf{E}_i\) with the coefficients \(c_f,c_g \in K[x_1]\). Set \[\nu=\frac{L}{c_g}, \qquad L=\operatorname{lcm}(c_f,c_g).\] If besides the above two conditions for the proper cover, we further require that the following condition hold:
then we say that the pair \(\boldsymbol{f}\) is hungrily covered* by \(\boldsymbol{g}\) with respect to \(p\).*
The algorithms below follow the signature framework for semi-\(S\)-pairs. Based on the input labelled pairs, we construct semi-\(S\)-pairs and then remove those properly (hungrily) covered according to Definition 7. We reduce the remaining semi-\(S\)-pairs by regular reduction. A zero remainder contributes a syzygy with its signature, and a non-scalar remainder leads to more semi-\(S\)-pairs. Eventually the algorithm outputs a nonzero scalar remainder from which we can obtain the eliminant.
height .4pt
Algorithm : ProperCoverReduction
height .4pt
\(F=\{f_1,\ldots,f_m\}\subset K[x_1][\boldsymbol{\tilde{x}}]\), monomial order \(\prec\), POT order \(\prec_{\scriptscriptstyle \mathrm{POT}}\) pre-basis \(G_0\), pre-eliminant \(\chi_0\), multiplier set \(\Lambda\) \(G_0\): a list of pre-basis elements; \(S\): a list for \(\operatorname{sig}(\boldsymbol{s})\), where \(\boldsymbol{s}\) is a syzygy found so far; \(SP\): a list of semi-\(S\)-pairs \(\lambda t\boldsymbol{g}\). \(\Lambda\): a list of multipliers used for the proper cover and proper reduction; initialize labelled pairs \(\boldsymbol{f}_i=(\mathbf{E}_i,f_i)\), \(f_i \in F\) for \(1 \le i \le m\), discard zero inputs; \(G_0\gets\{\boldsymbol{f}_i:\;f_i\ne0\}\), \(S\gets\varnothing\), \(SP\gets\varnothing\), \(\Lambda\gets\varnothing\), \(\chi_0\gets0\) insert the initial principal syzygy signatures \(\operatorname{sig}(f_j\mathbf{E}_i-f_i\mathbf{E}_j)\) for \(1\le i<j\le m\) into \(S\) form the initial semi-\(S\)-pairs and insert them into \(SP\) select and remove \(\lambda t\boldsymbol{g}\) of minimal signature discard \(\lambda t\boldsymbol{g}\) record \(\alpha\) in \(\Lambda\); make a proper reduction on the semi-\(S\)-pair \(\lambda t\boldsymbol{g}\) to obtain a properly reduced remainder pair denoted as \(\boldsymbol{r}\); record all the least multipliers of the above proper reductions into \(\Lambda\) \(S\gets S\cup\{\operatorname{sig}(\boldsymbol{r}))\}\) replace \(\chi_0\) by \(\gcd(\chi_0,\operatorname{poly}(\boldsymbol{r}))\) add the labelled pair \(\boldsymbol{r}\) to \(G_0\); insert principal syzygy signatures \(\operatorname{sig}(\operatorname{poly}(\boldsymbol{r})\boldsymbol{g}-g\boldsymbol{r})\) into \(S\) for each \(\boldsymbol{g}\in G_0\) ; form semi-\(S\)-pairs using \(\boldsymbol{r}\) and each \(\boldsymbol{g}\in G_0\) and put them into \(SP\); insert the special multipliers \(\{\gcd(\operatorname{lc}(g),\chi_0)\notin K\colon \boldsymbol{g}\in G_0\}\) into \(\Lambda\). \(G_0,\chi_0,\Lambda\)
height .4pt
The multipliers in Algorithm 1, i.e., the ProperCoverReduction algorithm, lead to the inaccuracy of the pre-eliminant \(\chi_0\). Hence we need to make a refinement of \(\chi_0\) in the following Algorithm 2, i.e., HungryRefinement algorithm, so as to obtain the eliminant \(\chi\). The only difference between the two algorithms is that we use the hungry cover and hungry reduction in Algorithm 2 instead of the proper cover and proper reduction in Algorithm 1.
height .4pt
Algorithm : HungryRefinement
height .4pt
\(F=(f_1,\ldots,f_m)\subset K[x_1][\boldsymbol{\tilde{x}}]\), an irreducible \(p\in K[x_1]\), monomial order \(\prec\), POT order \(\prec_{\scriptscriptstyle \mathrm{POT}}\) pre-basis \(G_p\), pre-eliminant \(\chi_p\), multiplier set \(\Lambda\) \(G_p\): a list of pre-basis elements; \(S\): a list for \(\operatorname{sig}(\boldsymbol{s})\), where \(\boldsymbol{s}\) is a syzygy found so far; \(SP\): a list of semi-\(S\)-pairs \(\lambda t\boldsymbol{g}\). \(\Lambda\): a list of multipliers used for the hungry cover and hungry reduction; initialize labelled pairs \(\boldsymbol{f}_i=(\mathbf{E}_i,f_i)\), \(f_i \in F\) for \(1 \le i \le m\), discard zero inputs; \(G_p\gets\{\boldsymbol{f}_i:\;f_i\ne0\}\), \(S\gets\varnothing\), \(SP\gets\varnothing\), \(\Lambda\gets\varnothing\), \(\chi_p\gets0\) insert the initial principal syzygy signatures \(\operatorname{sig}(f_j\mathbf{E}_i-f_i\mathbf{E}_j)\) for \(1\le i<j\le m\) into \(S\) form the initial semi-\(S\)-pairs and insert them into \(SP\) select and remove \(\lambda t\boldsymbol{g}\) of minimal signature discard \(\lambda t\boldsymbol{g}\) record \(\alpha\) in \(\Lambda\); make a hungry reduction with respect to \(p\) on the semi-\(S\)-pair \(\lambda t\boldsymbol{g}\) to obtain a hungrily reduced remainder pair \(\boldsymbol{r}\); record all the nonconstant least multipliers of the above hungry reduction into \(\Lambda\) \(S\gets S\cup\{\operatorname{sig}(\boldsymbol{r})\}\) replace \(\chi_p\) by \(\gcd(\chi_p,\operatorname{poly}(\boldsymbol{r}))\) add the labelled pair \(\boldsymbol{r}\) to \(G_p\); insert principal syzygy signatures \(\operatorname{sig}(\operatorname{poly}(\boldsymbol{r})\boldsymbol{g}-g\boldsymbol{r})\) into \(S\) for each \(\boldsymbol{g}\in G_P\) ; form semi-\(S\)-pairs using \(\boldsymbol{r}\) and each \(\boldsymbol{g}\in G_P\) and put them into \(SP\); insert the special multipliers \(\{\gcd(\operatorname{lc}(g),\chi_p)\notin K\colon \boldsymbol{g}\in G_p\}\) into \(\Lambda\). \(G_p,\chi_p,\Lambda\)
height .4pt
The nonconstant multiplier sets \(\Lambda\) produced by Algorithm 1 and Algorithm 2 are from the proper (hungry) reductions, from proper (hungry) covers, and from the special multipliers. In this subsection we use \(\Lambda\) to define the compatible factor of the pre-eliminant \(\chi_0\) or \(\chi_p\) that is also a factor of the eliminant \(\chi\).
Definition 8 (Compatible factor). Let \(\Lambda\) be the nonconstant multiplier set produced by Algorithm 1 or Algorithm 2. For \(q\in K[x_1]\), we denote: \[\Theta(q) := \{ p \in K[x_1] \setminus K : \operatorname{mult}_p(q)>0,~p\text{ is irreducible and coprime to each multiplier in } \Lambda \}.\] If \(\Theta(\chi_0) \neq \varnothing\), we define the compatible factor of \(\chi_0\) as \[\chi_{0,c} := \prod_{p \in \Theta(\chi_0)} p^{\operatorname{mult}_p(\chi_0)}.\] If \(\Theta(\chi_p) \neq \varnothing\),we define the compatible factor of \(\chi_p\) as \[\chi_{p,c} := \prod_{p \in \Theta(\chi_p)} p^{\operatorname{mult}_p(\chi_p)}.\] Otherwise, we define \(\chi_{0,c}:= 1 \text{ or } \chi_{p,c} := 1\).
height .4pt
Algorithm : Main Proper-Cover algorithm
height .4pt
\(F\subset K[x_1][\boldsymbol{\tilde{x}}]\), monomial order \(\prec\), POT order \(\prec_{\scriptscriptstyle \mathrm{POT}}\) modular bases \(\mathrm{B}\) and pre-proper basis \(\mathcal{B}\) \((G_0,\chi_0,\Lambda)\gets\Call{ProperCoverReduction}{F,\prec,\prec_{\scriptscriptstyle \mathrm{POT}}}\) compute \(\chi_{0,c}\), set \(\widehat\chi\gets\chi_0\), and set \(\chi_q\gets\widehat\chi/\chi_{0,c}\) \(\mathrm{B}\gets\varnothing\); if \(\chi_{0,c}\ne1\), insert the modular basis \((\chi_{0,c},\pi_{\chi_{0,c}}(G_0)\setminus\{0\})\) into \(\mathrm{B}\) \(\chi_c \gets \chi_{0,c}\) Select an irreducible factor \(p\) of \(\chi_q\) with minimal \(\operatorname{mult}_p(\chi_q)\). \((G_p,\chi_p,\Lambda_p)\gets\Call{HungryRefinement}{F,p,\prec,\prec_{\scriptscriptstyle \mathrm{POT}}}\) set \(e\gets\operatorname{mult}_p(\chi_p)\); if \(e>0\), insert the modular basis \((p^e,\pi_{p^e}(G_p)\setminus\{0\})\) into \(\mathrm{B}\) compute \(\chi_{p,c}\) from \((\chi_p,\Lambda_p)\) \(\widehat\chi \gets \gcd(\widehat\chi,\chi_p)\), \(\chi_c \gets \operatorname{lcm}(\chi_c,\chi_{p,c})\) \(\chi_q\gets\widehat\chi/\chi_c\) set \(\chi\gets\prod_{(q,\mathrm{B}_q)\in\mathrm{B}}q\) and \(\mathcal{B}\gets\bigcup_{(q,\mathrm{B}_q)\in\mathrm{B}}(\mathrm{B}_q\cup\{q\})\) \(\mathrm{B},\mathcal{B}\)
height .4pt
In this section we prove the correctness and termination of our algorithm.
Definition 9 (Local basis below a signature \(T\)). Let \(G_0\) and \(G_p\) be the pre-bases obtained in Algorithm [alg:propercover-stage1] and Algorithm [alg:hungry-refinement] respectively. We name the subset of the pre-basis \(G_0\) or \(G_p\) the signatures of whose elements are smaller than a signature \(T\) as a local basis below \(T\).
The algorithm is incremental in nature because of the POT order. Hence every labelled pair with signature strictly smaller than a signature \(T\) can be properly (hungrily) reduced to a syzygy by the local basis below \(T\). This is the concept of “signature Gröbner basis below \(T\)” as in [1], [5] and “strong Gröbner basis” as in [3].
In this subsection we prove in Lemma 2 that the cover and regular reduction to a semi-\(S\)-pair in our algorithm yield a representation of the corresponding \(S\)-pair like the reduction of \(S\)-polynomials in Buchberger’s algorithm.
Lemma 1. Let \(\boldsymbol{f}=(\mathbf{u},f)\) and \(\boldsymbol{g}=(\mathbf{v},g)\) be labelled pairs that satisfy \(\operatorname{sig}(\boldsymbol{f})=\operatorname{sig}(\boldsymbol{g})\). Then their properly (hungrily) reduced forms share the same polynomial part and hence differ by a syzygy.
Proof. Since the signature of \(\boldsymbol{f}-\boldsymbol{g}\) is smaller than \(\operatorname{sig}(\boldsymbol{f})\), \(\boldsymbol{f}-\boldsymbol{g}\) is a syzygy with respect to the local basis below \(\operatorname{sig}(\boldsymbol{f})\). Thus follows the conclusion. ◻
Lemma 2. Let \(\lambda_f t_f\boldsymbol{f}\) be a semi-\(S\)-pair generated by labelled pairs \(\boldsymbol{f},\boldsymbol{h}\). Then the cover and regular reduction to \(\lambda_f t_f\boldsymbol{f}\) in Algorithm [alg:propercover-stage1] and Algorithm [alg:hungry-refinement] correspond to the following representation of \(\boldsymbol{S} (\boldsymbol{f},\boldsymbol{h})\): \[\label{eq:s-representation} \lambda \boldsymbol{S} (\boldsymbol{f},\boldsymbol{h})=\sum_{k=1}^s q_k\boldsymbol{g}_k+\boldsymbol{r}+\boldsymbol{s}\qquad{(4)}\] such that the leading monomial condition 6 holds without taking into account the syzygy \(\boldsymbol{s}\). Here \(\{\boldsymbol{g}_k\colon 1\le k\le s\}\) is the local basis below \(\operatorname{sig}(\lambda_f t_f\boldsymbol{f})\), and \(q_k,r\in K[x_1][\boldsymbol{\tilde{x}}]\) for \(1\le k\le s\).
Proof. When the semi-\(S\)-pair \(\lambda_f t_f\boldsymbol{f}\) is not covered, then we shall perform a regular reduction on it. If the first step of the regular reduction is through \(\boldsymbol{h}\) itself, then the result is exactly the \(S\)-pair \(\boldsymbol{S} (\boldsymbol{f},\boldsymbol{h})\). Hence the representation ?? holds for a regular reduction. Now assume that the first step of regular reduction is not through \(\boldsymbol{h}\) but a local basis element \(\boldsymbol{k}\). Then \(\operatorname{lm}(\lambda_f t_ff)=\operatorname{lcm}(\operatorname{lm}(f),\operatorname{lm}(h))\) is divisible by \(\operatorname{lm}(k)\) and hence by \(\operatorname{lcm}(\operatorname{lm}(f),\operatorname{lm}(k))\). Let us denote \(\tau=\operatorname{lcm}(\operatorname{lm}(f),\operatorname{lm}(h))/\operatorname{lcm}(\operatorname{lm}(f),\operatorname{lm}(k))\). If we denote the semi-\(S\)-pair generated by \(\boldsymbol{f}\) and \(\boldsymbol{k}\) as \(\boldsymbol{g}\), then there exist least multipliers \(\mu,\nu\) such that \(\mu\operatorname{sig}(\lambda_f t_f\boldsymbol{f})=\nu\tau\operatorname{sig}(\boldsymbol{g})\). According to Lemma 1, we have: \[\label{eq:tmp-coverIdentity} \eta\mu\lambda_ft_f\boldsymbol{f}=\rho\nu\tau\boldsymbol{g}+\sum_{k=1}^sq_k\boldsymbol{g}_k+\boldsymbol{s}.\tag{7}\] Here \(\boldsymbol{s}\) is a syzygy. The representation \(\sum_{k=1}^sq_k\boldsymbol{g}_k\) accounts for both the regular reductions of \(\mu\lambda_f t_f\boldsymbol{f}\) and \(\nu\tau\boldsymbol{g}\) with multipliers \(\eta,\rho\). The local basis elements \(\{\boldsymbol{g}_k\}\) satisfy \[\operatorname{sig}(q_k\boldsymbol{g}_k)\prec_{\scriptscriptstyle \mathrm{POT}}\operatorname{sig}(\mu\lambda_f t_f\boldsymbol{f})=\operatorname{sig}(\nu\tau\boldsymbol{g}), \qquad 1\le k\le s.\]
When \(\lambda_f t_f\boldsymbol{f}\) is covered by a labelled pair \(\boldsymbol{g}\) with cover multipliers \(\mu,\nu\) and monomial \(\tau\), then they also satisfy the identity 7 . Without loss of generality, suppose that \(\operatorname{lt}(\eta\mu\lambda_f t_ff)=\operatorname{lt}(q_1g_1)\). We construct the identity \[\eta\mu\boldsymbol{S} (\boldsymbol{f},\boldsymbol{h}) =\rho\nu\tau\boldsymbol{g}-\eta\mu\lambda_h t_h\boldsymbol{h} +\sum_{k=1}^sq_k\boldsymbol{g}_k+\boldsymbol{s}\] with \(\operatorname{lt}(\lambda_f t_ff)=\operatorname{lt}(\lambda_h t_hh)\). Since \(q_1\boldsymbol{g}_1-\eta\mu\lambda_h t_h\boldsymbol{h}\) is a labelled pair whose signature is smaller than \(\operatorname{sig}(t_f\boldsymbol{f})\), hence follows the identity: \[\label{eq:CoverIdentity} \eta\mu\boldsymbol{S} (\boldsymbol{f},\boldsymbol{h})=\rho\nu\tau\boldsymbol{g}+(q_1\boldsymbol{g}_1-\eta\mu\lambda_h t_h\boldsymbol{h})+\sum_{k=2}^sq_k\boldsymbol{g}_k+\boldsymbol{s}.\tag{8}\] Since the signatures of \(\boldsymbol{g}\) and \(q_1\boldsymbol{g}_1-\eta\mu\lambda_h t_h\boldsymbol{h}\) are both smaller than \(\operatorname{sig}(t_f\boldsymbol{f})\), they can be reduced to \(0\) by the local basis below \(\operatorname{sig}(t_f\boldsymbol{f})\), which leads to a representations in terms of the local basis. Thus follows the representation ?? if we substitute their representations into 8 . It is easy to see that the leading monomial condition 6 holds. ◻
In this subsection we prove in Lemma 4 that the compatible factor of the pre-eliminant \(\chi_0\) obtained in Algorithm [alg:propercover-stage1] is a factor of the eliminant \(\chi\). And the exact powers of the other factors of \(\chi\) can be recognized in the pre-eliminant \(\chi_p\) obtained in Algorithm [alg:hungry-refinement].
Lemma 3. Let \(F=\{f_j:1\le j\le s\}\subset K[x_1][\boldsymbol{\tilde{x}}]\setminus K[x_1]\) be a finite polynomial set. Suppose that all \(f_j\) have the same leading monomial \(\operatorname{lm}(f_j)=\boldsymbol{\tilde{x}}^\alpha\in\operatorname{Mon}(\boldsymbol{\tilde{x}})\) for \(1 \le j \le s\).
If \(f=\sum_{j=1}^{s}f_j\) satisfies \(\operatorname{lm}(f)\prec\boldsymbol{\tilde{x}}^\alpha\), then there exist multipliers \(b,b_j\in K[x_1]\setminus\{0\}\), \(1\le j<s\), such that \(bf=\sum_{1\le j<s} b_j S(f_j,f_s)\) with \(S(f_j,f_s)\) being \(S\)-polynomials.
For each irreducible polynomial \(p\in K[x_1]\setminus K\), we can relabell the elements of \(F\) so that the multiplier \(b\) is not divisible by \(p\).
Proof. This is Lemma 3.11 of [7]. ◻
Lemma 4. Let \(F\subset K[x_1][\boldsymbol{\tilde{x}}]\setminus K[x_1]\) be a finite polynomial set generating a zero-dimensional ideal \(I=\langle F\rangle\subset K[x_1][\boldsymbol{\tilde{x}}]\). After we input \(F\) into Algorithm [alg:propercover-stage1], suppose \(G_0=\{\boldsymbol{g}_k:1\le k\le s\}\) and \(\chi_0\) are the output pre-basis and pre-eliminant respectively with \(\boldsymbol{g}_k=(\mathbf{u}_k,g_k)\). Denote \(G=\{g_k:1\le k\le s\}\), and let \(\chi_{0,c}\) be the compatible factor of \(\chi_0\). Then for every \(f\in I\), there exist \(q_0,q_1,\ldots,q_s\in K[x_1][\boldsymbol{\tilde{x}}]\) and \(\lambda\in K[x_1]\setminus\{0\}\) with \(\gcd(\lambda,\chi_{0,c})=1\) such that \[\lambda f=\sum_{k=1}^{s}q_k g_k+q_0\chi_0 . \label{eq:compatible-representation}\qquad{(5)}\] Moreover, \[\operatorname{lm}(f)= \max\left\{ \max_{1\le k\le s}\{\operatorname{lm}(q_k g_k)\}, \operatorname{lm}(q_0) \right\}. \label{eq:compatible-leading-condition}\qquad{(6)}\] In particular, the eliminant \(\chi\in I\cap K[x_1]\) satisfies \(\lambda\chi=q_0\chi_0\) with \(q_0\in K[x_1]\setminus\{0\}\) and \(\gcd(\lambda,\chi_{0,c})=1\). Consequently, \(\chi_{0,c}\mid\chi\).
If we input \(F\) and an irreducible \(p\in K[x_1]\) into Algorithm [alg:hungry-refinement] with output \((G_p,\chi_p,\Lambda_p)\), then ?? and ?? also hold for \(G_p\) and \(\chi_p\) such that \(\gcd(\lambda,\chi_{p,c})=1\) in ?? . In particular, \(\chi_{p,c} \mid \chi\).
Proof. Fix an irreducible factor \(t\) of \(\chi_{0,c}\). For \(F=\{f_k:1\le k\le m\}\), suppose that \(f\) can be written as \(f=\sum_{k=1}^{m}h_kf_k\) with \(h_k\in K[x_1][\boldsymbol{\tilde{x}}]\) for \(1 \le k \le m\). Set \(\boldsymbol{\tilde{x}}^\beta:=\max_{1\le k\le m}\{\operatorname{lm}(h_kf_k)\}\). If \(\operatorname{lm}(f)=\boldsymbol{\tilde{x}}^\beta\), the conclusion already holds. Now we assume \(\operatorname{lm}(f)\prec\boldsymbol{\tilde{x}}^\beta\).
Let us denote \(\operatorname{lt}(h_k)=c_k\boldsymbol{\tilde{x}}^{\alpha_k}\), where \(c_k\in K[x_1]\setminus\{0\}\). Without loss of generality, suppose that \(\operatorname{lm}(\boldsymbol{\tilde{x}}^{\alpha_k}f_k) = \boldsymbol{\tilde{x}}^\beta\) holds for \(1 \le k \le m\). And we have: \[f=\sum_{k=1}^{m}c_k\boldsymbol{\tilde{x}}^{\alpha_k}f_k +\sum_{k=1}^{m}\bigl(h_k-\operatorname{lt}(h_k)\bigr)f_k . \label{eq:compatible-first-decomposition}\tag{9}\]
By Lemma 3 (1), there exist \(b,b_k\in K[x_1]\setminus\{0\}\) for \(1\le k<m\), that satisfy the identity: \[b\sum_{k=1}^{m}c_k\boldsymbol{\tilde{x}}^{\alpha_k}f_k = \sum_{1\le k<m} b_k S(c_k\boldsymbol{\tilde{x}}^{\alpha_k}f_k,c_t\boldsymbol{\tilde{x}}^{\alpha_t}f_m) = \sum_{1\le k<m} b_k n_k\boldsymbol{\tilde{x}}^{\beta-\gamma_k}S(f_k,f_m), \label{eq:compatible-spair-combination}\tag{10}\] where \(\boldsymbol{\tilde{x}}^{\gamma_k}:=\operatorname{lcm}(\operatorname{lm}(f_k),\operatorname{lm}(f_m))\) and \(n_k:={\operatorname{lcm}(c_k\operatorname{lc}(f_k),c_m\operatorname{lc}(f_m))} /{\operatorname{lcm}(\operatorname{lc}(f_k),\operatorname{lc}(f_m))}\) for \(1\le k<m\). Moreover, by Lemma 3 (2), we can relabel the subscripts of the elements in \(F\) such that \(\operatorname{mult}_t(b) = 0\).
Each \(S\)-polynomial \(S(f_k,f_m)\) in 10 is the polynomial part of an \(S\)-pair. When the \(S\)-pair is not singular, according to the representation ?? of \(S\)-pairs in Lemma 2, \(S(f_k,f_m)\) can be represented by the basis set \(G\), and \(\operatorname{lm}(S(f_k,f_m))\prec\boldsymbol{\tilde{x}}^{\gamma_k}\). It is easy to see that when the \(S\)-pair is singular this conclusion also holds. Combining these representations with the second summation in 9 , we obtain a representation \[\mu b f=\sum_{k=0}^{s}a_k g_k, \qquad g_0:=\chi_0,\] where the quotient \(a_k\in K[x_1][\boldsymbol{\tilde{x}}]\) for \(0 \le k \le s\) and \(\max_{0\le k\le s}\{\operatorname{lm}(a_kg_k)\}\prec\boldsymbol{\tilde{x}}^\beta\). The multiplier \(\mu\in K[x_1]\setminus\{0\}\) is a product of multipliers recorded in our algorithm. Since \(t\) is a factor of \(\chi_{0,c}\), none of these recorded multipliers is divisible by \(t\). Hence \(t\nmid \mu b\).
We repeat the above procedure on the new representation \(\mu b f=\sum_{k=0}^{s}a_k g_k\). The repetition halts in finite steps since the monomial ordering on \(\operatorname{Mon}(\boldsymbol{\tilde{x}})\) is a well-ordering. Thus, for the fixed factor \(t\), we obtain \(\lambda_t f=\sum_{k=1}^{s}q_{k,t}g_k+q_{0,t}\chi_0\) with \(t\nmid\lambda_t\), as well as the corresponding leading-monomial condition ?? .
Let \(t\) range over all irreducible factors of \(\chi_{0,c}\), and set \(\lambda:=\gcd\{\lambda_t\}\). Then \(\gcd(\lambda,\chi_{0,c})=1\). Since \(K[x_1]\) is a PID, there exist \(d_t\in K[x_1]\) such that \(\lambda=\sum_{t}d_t\lambda_t\). Multiplying the above representations by \(d_t\) and summing over all these \(t\), we get \[\lambda f=\sum_{k=1}^{s}q_kg_k+q_0\chi_0, \qquad \gcd(\lambda,\chi_{0,c})=1.\] There is no monomial larger than \(\operatorname{lm}(f)\) in the right-hand side. So follows ?? .
Finally, take \(f=\chi\). Since \(\chi\in K[x_1]\), according to ?? , we have \(\lambda\chi=q_0\chi_0\) with \(q_0\in K[x_1]\setminus\{0\}\) and \(\gcd(\lambda,\chi_{0,c})=1\). Hence \(\chi_{0,c}\mid\chi\). It is easy to see that all the above arguments apply to \(G_p \text{ and } \chi_{p,c}\). ◻
Proposition 10. Let \(p\) be an irreducible factor of \(\chi_0/\chi_{0,c}\) taken as an input of Algorithm [alg:hungry-refinement]. Suppose Algorithm [alg:hungry-refinement] outputs \((G_p,\chi_p,\Lambda_p)\). Then \(\operatorname{mult}_p(\chi_p)=\operatorname{mult}_p(\chi)\).
Proof. In Algorithm [alg:hungry-refinement], the hungry covers and hungry reductions are performed with multipliers coprime to the selected irreducible factor \(p\). Applying Lemma 4 to the output \((G_p,\chi_p,\Lambda_p)\) of Algorithm [alg:hungry-refinement] and to \(f=\chi\), we obtain \(\lambda\chi=q_0\chi_p\) with \(q_0\in K[x_1]\setminus\{0\}\). It is easy to see that we also have \(p\nmid\lambda\). Now \(\chi_p\) belongs to \(I\cap K[x_1]=(\chi)\) indicates that \(\chi\mid\chi_p\), and hence \(\operatorname{mult}_p(\chi)\le\operatorname{mult}_p(\chi_p)\). On the other hand, \(\lambda\chi=q_0\chi_p\) and \(p\nmid\lambda\) yields \[\operatorname{mult}_p(\chi)=\operatorname{mult}_p(q_0)+\operatorname{mult}_p(\chi_p) \ge\operatorname{mult}_p(\chi_p).\] Thus \(\operatorname{mult}_p(\chi_p)=\operatorname{mult}_p(\chi)\) as claimed. ◻
In this subsection we verify that the pre-bases obtained in our algorithm satisfy condition 2 in Definition 1 and prove the termination of our algorithm in Theorem 2.
Proposition 11. Let \((q,\mathrm B_q)\) be a modular basis output by the main algorithm. Then the modular basis condition 2 holds for \((q,B_q)\).
Proof. The inclusion \[\langle \operatorname{LT}(B_q)\rangle \subseteq \langle \operatorname{LT}(\pi_q(I))\rangle\] is immediate. We prove the reverse inclusion. Let \((G^\star,\chi^\star,\Lambda^\star)\) be an output of Algorithm [alg:propercover-stage1] or Algorithm [alg:hungry-refinement]. And \(G_0^\star=\{g_1,\dots,g_s\}\) is the polynomial part of \(G^\star\) that satisfies \(q\mid \chi\) and \(B_q=\{\pi_q(g_i):1\le i\le s,\;\pi_q(g_i)\neq 0\}\). By Proposition 10, \(\gcd(\chi/q,q)=1\).
Take \(0\neq \bar f\in \pi_q(I)\), we treat \(\bar f\) as in \(K[x_1][\boldsymbol{\tilde{x}}]\) and it satisfies \(\pi_q(\bar f)=\bar f\). Since \(\bar f\in \pi_q(I)\), there exists \(g\in I\) with \(\pi_q(g)=\bar f\), hence \(g-\bar f\in \langle q\rangle\). Put \(c=\chi/q\). Then \(c(g-\bar f)\in \langle \chi\rangle\subset I\), so \(c \bar f\in I\). By Lemma 4 on \(c \bar f\) for \((G^\star,\chi^\star,\Lambda^\star)\), we obtain \(a_0,a_1,\dots,a_s\in K[x_1][\boldsymbol{\tilde{x}}]\) and \(\lambda\in K[x_1]\setminus\{0\}\) with \(\gcd(\lambda,q)=1\), such that \[\lambda c\bar f=\sum_{i=1}^s a_i g_i+a_0\chi^\star\] and \[\operatorname{lm}(\bar f)= \max\bigl\{\max_{1\le i\le s}\{\operatorname{lm}(a_i g_i)\}, \operatorname{lm}(a_0)\bigr\}.\]
We get \[\pi_q(\lambda c)\bar f=\sum_{i=1}^s \pi_q(a_i)\pi_q(g_i).\] Since \(\gcd(\lambda c,q)=1\), the element \(\pi_q(\lambda c)\) is a unit in \(K[x_1]/(q)\). Hence the term with the monomial \(\operatorname{lm}(\bar f)\) in \(\sum_{i=1}^{s}\pi_q(a_i)\pi_q(g_i)\) has nonzero coefficient. If we set \[\Gamma=\{\,i:\operatorname{lm}(a_i g_i)=\operatorname{lm}(\bar f),\;\pi_q(\operatorname{lc}(a_i g_i))\neq 0\,\},\] then \(\Gamma\neq\varnothing\), and \[\operatorname{lt}(\bar f)=\pi_q(\lambda c)^{-1}\sum_{i\in\Gamma}\pi_q(\operatorname{lt}(a_i))\,\operatorname{lt}(\pi_q(g_i))\in \langle \operatorname{LT}(B_q)\rangle.\] Thus \[\langle \operatorname{LT}(\pi_q(I))\rangle \subseteq \langle \operatorname{LT}(B_q)\rangle,\] and the desired equality 2 follows. ◻
Theorem 2. Suppose the main algorithm outputs the pre-proper basis \(\mathcal{B}\). Then the main algorithm terminates, and \(\mathcal{B}\) is the proper basis of \(I\).
Proof. The termination of Algorithm [alg:propercover-stage1] and Algorithm [alg:hungry-refinement] follows from the fact that the algebra \(K[x_1][\boldsymbol{\tilde{x}}]\) is Noetherian. The main algorithm terminates due to the fact that \(\widehat\chi\) in the main algorithm has only finitely many irreducible and coprime factors.
Now we prove that the outputs of main algorithm are correct. By Lemma 4, the compatible factor \(\chi_{0,c}\) divides \(\chi\). For each irreducible factor \(p\) of \(\chi/\chi_{0,c}\), Proposition 10 shows that Algorithm [alg:hungry-refinement] outputs exactly the factor \(p^{\operatorname{mult}_p(\chi)}\). We enumerate \(\chi_{0,c}\) and all these factors \(p^{\operatorname{mult}_p(\chi)}\) as \(\{q_1,\ldots,q_N\}\) that are pairwise coprime and satisfy \[\chi=\prod_{k=1}^{N}q_k .\] For each pair \((q_k,B_{q_k})\), Proposition 11 gives \[\langle\operatorname{LT}(\pi_{q_k}(I))\rangle=\langle\operatorname{LT}(B_{q_k})\rangle\] in \((K[x_1]/(q_k))[\boldsymbol{\tilde{x}}]\). Thus the pre-proper basis \(\mathcal{B}=\bigcup_{k=1}^N(B_{q_k}\cup\{q_k\})\) is a proper basis of \(I\) by Definition 1. ◻
We can obtain the classical Gröbner basis of the ideal \(I\subset K[x_1,x_2,\dotsc,x_n]\) over the field \(K\) from the proper basis of \(I\subset K[x_1][\boldsymbol{\tilde{x}}]\) defined above. Please refer to [4] and [4] on this respect.
This section evaluates the computational efficiency of the Proper-Cover algorithm by comparing it with the GVW and the F5 algorithms on standard Cyclic and Katsura benchmark systems, together with seven random systems:
\(\langle -z^2(z+1)^3x^2+y^2,\;z^4(z+1)^6x-y^4,\;-x^2y^3+y^4+z^4(z-1)^5\rangle,\)
\(\langle -z^2(z+1)^3x^3+y^2,\;z^4(z+1)^6x-y^3,\;-x^2y^2+y^3+z^4(z-1)^5\rangle,\)
\(\langle -y^4z^2+x^3+x,\;y^6-x^2z(z-1)+z^4,\;y^5+z^2-x-1\rangle,\)
\(\langle -y^4z^2+x^2+x,\;-z^2x+y^5+2,\;-x+y^2+z^3-1\rangle,\)
\(\langle -y^4z^2+x^3+x,\;y^6-x^2z(z^3-2)+2z^4,\;y^5+z^4-x^2-z\rangle,\)
\(\langle 3x^3z+8x^2y^2+x^2yz+5xy^3,\; 2y^3z^2+13y^2z^3+5yz^4+x^3,\; xz^2+12y^3+8x^2+3,\\ \phantom{3x^3z+8x^2y^2+x^2yz+5xy^3,\;2y^3z^2+13y^2z^3+5yz^4+x^3,\;xz^2+12} 18xy^3z^2+y^3z^3+7x^2y^2\rangle,\)
\(\langle -z^2(z+1)^3x^3+y,\;z^4(z+1)^6x-y^3,\;-x^2y^3+y^3+z^4(z-1)^5\rangle.\)
The experiments are performed under three monomial orders and all algorithms are implemented in Maple without additional optimization. The time limit is 3600 seconds. All computations are carried out in Maple 18 on a 64-bit Windows 11 machine with an 11th Gen Intel(R) Core(TM) i7-11800H @ 2.30GHz processor and 16 GB RAM.
| 2-4 (lr)5-7 (lr)8-10 System | PC | GVW | F5 | PC | GVW | F5 | PC | GVW | F5 |
| Random-1 | 0.515 | 1.840 | timeout | 0.516 | 2.768 | timeout | 6.078 | 57.019 | timeout |
| Random-2 | 0.391 | 2.371 | timeout | 0.344 | 3.571 | timeout | 0.484 | 77.666 | timeout |
| Random-3 | 2.579 | 0.058 | 10.385 | 2.703 | 0.163 | 9.737 | 7.140 | 716.402 | timeout |
| Random-4 | 1.234 | 0.029 | 14.066 | 1.109 | 0.120 | 12.770s | 5.594 | 60.000 | timeout |
| Random-5 | 5.922 | 0.024 | 5.258 | 5.375 | 0.040 | 5.573 | 21.531 | 3548.083 | timeout |
| Random-6 | 44.875 | 4.083 | timeout | 59.468 | 3.507 | timeout | 310.735 | 80.583 | timeout |
| Random-7 | 0.266 | 4.426 | timeout | 0.593 | 7.961 | timeout | 0.985 | 95.732 | timeout |
| Katsura-2 | \(<10^{-3}\) | 0.038 | 0.183 | \(<10^{-3}\) | 0.024 | 0.045 | \(<10^{-3}\) | 0.045 | 0.057 |
| Katsura-3 | 0.016 | 0.058 | 0.184 | 0.016 | 0.078 | 0.903 | 0.156 | 0.197 | 116.300 |
| Katsura-4 | 0.297 | 0.151 | 3.507 | 0.485 | 2.014 | timeout | 14.734 | 19.500 | timeout |
| Katsura-5 | 3.969 | 0.782 | 148.100 | 22.453 | timeout | timeout | timeout | timeout | timeout |
| Cyclic-2 | 0.016 | 0.035 | 0.037 | \(<10^{-3}\) | 0.017 | 0.016 | \(<10^{-3}\) | 0.042 | 0.045 |
| Cyclic-3 | \(<10^{-3}\) | 0.031 | 0.044 | 0.016 | 0.019 | 0.021 | \(<10^{-3}\) | 0.041 | 0.018 |
| Cyclic-5 | 5.734 | 1.123 | timeout | 6.532 | 3.985 | timeout | timeout | 39.700 | timeout |
4.2pt
The experimental results validate the core contribution of this work: the Proper-Cover algorithm offers an efficient and robust framework for ideal basis computation, outperforming the classic F5 and GVW algorithms. Across all test cases, Proper-Cover consistently outperforms F5 in both computational speed and the number of solved instances.
Furthermore, Proper-Cover delivers prominent advantages on hard instances and complex monomial orders. As illustrated by the Katsura-5 benchmark with the grlex order, Proper-Cover finishes the computation in 22.453 seconds, whereas both GVW and F5 terminate due to time limits. And Proper-Cover delivers clear speedups over GVW for lexicographic (plex) order in most cases.