Théry , Loïc
CROAP project, INRIA Sophia
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.
Three versions are provided:
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
operations on coefficients
parsing of polynomials
pretty-printing of polynomials.
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.
Identical to gbcoq2, except that coefficients
are now integers (big_int of ocaml).
The executable commands are gbcoq, gbcoq2, and gbcoq2int,
used with the following syntax:
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 - 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
(1456 K: ocaml sources and binaries for Linux, Dec , and Sun)
Browse the Coq Development
Here are some computation times on a PC 300MHz
and Computing: a certified version of the Buchberger's algorithm '',
Rapport de Recherche INRIA 3275, Octobre 1997.