Abstract
We describe how the theory of Gröbner 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 Gröbner bases: we want to prove, constructively in type theory, the existence of Gröbner bases and from such proofs extract the algorithms. Our main contribution is a reformulation of the standard theory of Gröbner 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 Gröbner bases.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
P. Aczel. An Introduction to Inductive Definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. North-Holland Publishing Company, 1977. 34, 37, 38
L. Augustsson. Cayenne-a language with dependent types. Technical report, Department of Computing Science, Chalmers University of Technology, 1998. Homepage: http://www.cs.chalmers.se/~augustss/cayenne/. 42
U. Berger and H. Schwichtenberg. The greatest common divisor: a case study for program extraction from classical proofs. In Proceedings of the Workshop TYPES’ 95, Torino, Italy, June 1995, number 1158 in Lecture Notes in Computer Science. Springer-Verlag, 1996. 34
B. Buchberger. An Algorithm for Finding a Basis for the Residue Class Ring of a Zero-Dimensional Polynomial Ideal (German). PhD thesis, University of Innsbruck, 1965. 33
B. Buchberger. Gröbner bases: An algorithmic method in polynomial ideal theory. In N. K. Bose, editor, Multidimensional systems theory, pages 184–232. Reidel Publ. Co., 1985. 33, 34
B. Buchberger. Introduction to Gröbner bases. In B. Buchberger and F. Winkler, editors, Gröbner bases and applications, pages 3–31. Cambridge University Press, 1998. 34
T. Becker and V. Weispfenning. Gröbner bases, volume 141 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1993. In cooperation with H. Kredel. 34, 35, 39, 42
D. Cox, J. Little, and D. O’Shea. Ideals, varieties, and algorithms. Undergraduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1997. 34
R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986. 35
Th. Coquand. Constructive topology and combinatorics. In proceeding of the conference Constructivity in Computer Science, San Antonio, LNCS 613, pages 28–32, 1992. 33, 34, 37, 38, 39
C. Coquand. The homepage of the Agda type checker. Homepage: http://www.cs.chalmers.se/~catarina/Agda/, 1998. 42
L. E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Am. J. Math., 35:413–422, 1913. 34
P. Dybjer. Comparing integrated and external logics of functional programs. Science of Computer Programming, 14:59–79, 1990. 33
R. Fröberg. An introduction to Gröbner bases. John Wiley & Sons, 1997. 34
J-Y Girard. Linear logic and parallelism. In M. Venturini Zilli, editor, Mathematical Models for the Semantics of Parallelism, number LNCS 280, pages 166–182. Springer-Verlag, September 1986. 33
G. Huet, G. Kahn, and C. Paulin-Mohring. The Coq proof assistant: A tutorial. Technical report, Rapport Technique 204, INRIA, 1997. 34
P. B. Jackson. Enhancing the Nuprl proof development system and applying it to computational abstract algebra. PhD thesis, Cornell University, 1995. 35, 41
C. Jacobsson and C. Löfwall. Standard bases for general coefficient rings and a new constructive proof of Hilbert’s basis theorem. J. Symbolic Comput., 12(3):337–371, 1991. 34, 39
P. Martin-Löf. Notes on Constructive Mathematics. Almqvist & Wiksell, 1968. 37
R. Mines, F. Richman, and W. Ruitenburg. A course in constructive algebra. Universitext. Springer-Verlag, New York, 1988. 39
B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf’ s Type Theory. An Introduction. Oxford University Press, 1990. 33
C. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society, 59:833–835, 1963. 41
LÖc Pottier. Dixon’s lemma. URL: ftp://www.inria.fr/safir/pottier/MON, 1996. 34
J-C. Raoult. Proving open properties by induction. Information processing letters, 29:19–23, 1988. 33, 34, 37, 39
F. Richman. Constructive aspects of noetherian rings. In Proc. AMS 44, pages 436–441, 1974. 39
L. Théry. Proving and computing: A certified version of the Buchberger’s algorithm. In proceeding of the 15th International Conference on Automated Deduction, Lindau, Germany, LNAI 1421, 1998. 34, 41
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coquand, T., Persson, H. (1999). Gröbner Bases in Type Theory. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds) Types for Proofs and Programs. TYPES 1998. Lecture Notes in Computer Science, vol 1657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48167-2_3
Download citation
DOI: https://doi.org/10.1007/3-540-48167-2_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66537-3
Online ISBN: 978-3-540-48167-6
eBook Packages: Springer Book Archive