Abstract :
One of the aims of Constructive Mathematics is to provide effective
methods (algorithms) to compute objects whose existence is asserted by
Classical Mathematics. Moreover, all proofs should be constructive, i.e.,
have an underlying effective content. E.g. the classical proof of the
correctness of Buchberger algorithm, based on noetherianity, is
non constructive~: the closest consequence is that we know that the algorithm \
ends, but we don't know when.
In this paper we explain how the Buchberger algorithm can be
used in order to give a constructive approach to the Hilbert basis theorem and
more generally to the constructive content of ideal theory in polynomial rings
over "discrete" fields .
More precisely we give a
constructive version of Dickson's Lemma, we deduce constructively the
correctness of Buchberger algorithm and
from this result we get the Hilbert basis theorem in a constructive form.
Résumé :
Nous donnons une version constructive du lemme de Dickson. Nous en
déduisons une preuve constructive de correction pour l'algorithme de
Buchberger. Nous obtenons comme conséquence une version constructive du
théorème "de la base" de Hilbert dans les anneaux de polynomes sur un
corps "discret".