The Buchberger Algorithm as a Tool for Ideal Theory of Polynomial Rings in Constructive Mathematics

Fichier ps. Fichier pdf. Fichier dvi.
avec Hervé Perdry, in: Gröbner Bases and Applications (Proc. of the Conference 33 Years of Gröbner Bases),
Cambridge University Press, London Mathematical Society Lecture Notes Series, vol. 251, (1998), 393-407.

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.

L'algorithme de Buchberger comme un outil dans la théorie constructive des idéaux dans les anneaux de polynomes

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".