[FOM] Groebner bases

[Bas Spitters]

On Wednesday 28 May 2008 17:34:07 Timothy Y. Chow wrote:
> What really is needed to prove that, say, Buchberger's algorithm for
> computing a Groebner basis always terminates, for rings of the kind that
> software packages like Magma or Macaulay know about?

It seems that you are interested in this article:

 Grobner Bases in Type Theory
by Thierry Coquand, Henrik Persson 
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.2400

Abstract. We describe how the theory of Grobner bases, an important part of 
computational algebra, can be developed within MartinL of's type theory. In 
particular, we aim for an integrated development of the algorithms for 
computing Grobner bases: we want to prove, constructively in type theory, the 
existence of Grobner bases and from such proofs extract the algorithms. Our 
main contribution is a reformulation of the standard theory of Grobner bases 
which uses generalised inductive definitions. We isolate the main 
non--constructive part, a minimal bad sequence argument, and use the open 
induction principle [Rao88,Coq92] to interpret it by induction. This leads to 
short constructive proofs of Dickson's lemma and Hilbert's basis theorem, 
which are used to give an integrated development of Buchberger's algorithm. 
An important point of this work is that the elegance and brevity of the 
original proofs are maintained while the new proofs also have a direct 
constructive content. In the appendix we present a computer formalisation of 
Dickson's lemma and an abstract existence proof of Grobner bases.

Bas