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

prettyprinting of polynomials.

gbcoq2:
In this version, only the proven kernel of Buchberger
algorithm is used:
algorithms on polynomials are handwritten (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 Maplelike 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: