Certified Gröbner bases computations
Laurent Théry , Loïc Pottier
CROAP project, INRIA Sophia Antipolis

This page gives certified implementations of Buchberger algorithm for Gröbner bases computations, running on Linux, Sun, and Dec platforms.

These programs are certified:
all algorithms have been written in the Coq system, have been proven to be correct, and by an automatic mechanism, their translations into ocaml programs have been produced, and then compiled into native code.

Description:
Three versions are provided:

• gbcoq:

• It is a fully proven version of Buchberger algorithm on multivariate polynomials (where we only suppose that coefficients of polynomials are in an abelian field). The implementation works with modular coefficients (modulo 31991). Then the only algorithms which are not proven are:
• operations on coefficients
• parsing of polynomials
• pretty-printing of polynomials.
• gbcoq2:

• In this version, only the proven kernel of Buchberger algorithm is used:
algorithms on polynomials are hand-written (addition, division, etc) in a more efficient representation than in the extracted code from Coq. (hence they are not formally proven):
• Polynomials are lists of pairs (coefficient, monomial).
• Coefficients are in the field Z/pZ, with p=31991.
• Monomials are arrays of integers, with total degree in position 0.
• gbcoq2int:
Identical to gbcoq2, except that coefficients are now integers (big_int of ocaml).
Use:
The executable commands are gbcoq, gbcoq2, and gbcoq2int, used with the following syntax:

gbcoq -file <filename>

gbcoq2 -file <filename>

gbcoq2int -file <filename>

where the file <filename> contains a list of variables, and a list of polynomials, in a Maple-like syntax, for instance (cyclic5 problem):

[a,b,c,d,e]

[a*b*c*d*e - 1,
a*b*c*d + b*c*d*e + c*d*e*a + d*e*a*b + e*a*b*c,
a*b*c + b*c*d + c*d*e + d*e*a + e*a*b,
a*b + b*c + c*d + d*e + e*a,
a+b+c+d+e]

Download gbcoq (1456 K: ocaml sources and binaries for Linux, Dec , and Sun)

Browse the Coq Development

Benchs:
Here are some computation times on a PC 300MHz -128Meg:

 gbcoq2 gbcoq2int gbcoq cyclic 5 0.15s 0.31s 1.04s cyclic 6 3.95s 61.71s 52.09s cyclic 7 816.92s

References:

Laurent Théry,
``Proving and Computing: a certified version of the Buchberger's algorithm '',
Rapport de Recherche INRIA 3275, Octobre 1997.

Related works: