Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleGröbner Bases in Type Theory
Author(s) Thierry Coquand, Henrik Persson
TypeBook, Chapter in Book, Conference Proceeding
AbstractWe describe how the theory of Groebner bases, an important part of
computational algebra, can be developed within Martin-Löf's type
theory. In particular, we aim for an integrated development of the
algorithms for computing Groebner bases: we want to prove,
constructively in type theory, the existence of Groebner 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 Groebner bases.
JournalLectures Notes in Computer Science
Pagesp. 33
PublisherSpringer-Verlag GmbH
EditorT. Altenkirch, W. Naraschewski, B. Reus
Translation No
Refereed No
BookTypes for Proofs and Programs: International Workshop, TYPES '98