Skip to main content

Gröbner Bases in Type Theory

  • Conference paper
  • First Online:
Types for Proofs and Programs (TYPES 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1657))

Included in the following conference series:

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

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

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

    Google Scholar 

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

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  8. D. Cox, J. Little, and D. O’Shea. Ideals, varieties, and algorithms. Undergraduate Texts in Mathematics. Springer-Verlag, New York, second edition, 1997. 34

    Google Scholar 

  9. R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986. 35

    Google Scholar 

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

    Google Scholar 

  11. C. Coquand. The homepage of the Agda type checker. Homepage: http://www.cs.chalmers.se/~catarina/Agda/, 1998. 42

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

    Article  MathSciNet  Google Scholar 

  13. P. Dybjer. Comparing integrated and external logics of functional programs. Science of Computer Programming, 14:59–79, 1990. 33

    Article  MATH  MathSciNet  Google Scholar 

  14. R. Fröberg. An introduction to Gröbner bases. John Wiley & Sons, 1997. 34

    Google Scholar 

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

    Google Scholar 

  16. G. Huet, G. Kahn, and C. Paulin-Mohring. The Coq proof assistant: A tutorial. Technical report, Rapport Technique 204, INRIA, 1997. 34

    Google Scholar 

  17. P. B. Jackson. Enhancing the Nuprl proof development system and applying it to computational abstract algebra. PhD thesis, Cornell University, 1995. 35, 41

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  19. P. Martin-Löf. Notes on Constructive Mathematics. Almqvist & Wiksell, 1968. 37

    Google Scholar 

  20. R. Mines, F. Richman, and W. Ruitenburg. A course in constructive algebra. Universitext. Springer-Verlag, New York, 1988. 39

    MATH  Google Scholar 

  21. B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf’ s Type Theory. An Introduction. Oxford University Press, 1990. 33

    Google Scholar 

  22. C. Nash-Williams. On well-quasi-ordering finite trees. Proceedings of the Cambridge Philosophical Society, 59:833–835, 1963. 41

    Article  MATH  MathSciNet  Google Scholar 

  23. LÖc Pottier. Dixon’s lemma. URL: ftp://www.inria.fr/safir/pottier/MON, 1996. 34

  24. J-C. Raoult. Proving open properties by induction. Information processing letters, 29:19–23, 1988. 33, 34, 37, 39

    Article  MATH  MathSciNet  Google Scholar 

  25. F. Richman. Constructive aspects of noetherian rings. In Proc. AMS 44, pages 436–441, 1974. 39

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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

Publish with us

Policies and ethics