Skip to main content
SpringerLink
Log in

Gröbner Bases of Modules and Faugère’s \(F_4\) Algorithm in Isabelle/HOL

  • Conference paper
  • First Online:
Intelligent Computer Mathematics (CICM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11006))

Included in the following conference series:

Abstract

We present an elegant, generic and extensive formalization of Gröbner bases, an important mathematical theory in the field of computer algebra, in Isabelle/HOL. The formalization covers all of the essentials of the theory (polynomial reduction, S-polynomials, Buchberger’s algorithm, Buchberger’s criteria for avoiding useless pairs), but also includes more advanced features like reduced Gröbner bases. Particular highlights are the first-time formalization of Faugère’s matrix-based \(F_4\) algorithm and the fact that the entire theory is formulated for modules and submodules rather than rings and ideals. All formalized algorithms can be translated into executable code operating on concrete data structures, enabling the certified computation of (reduced) Gröbner bases and syzygy modules.

A. Maletzky—The research was funded by the Austrian Science Fund (FWF): P 29498-N31.

F. Immler—The research was funded by DFG Koselleck Grant NI 491/16-1.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
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 EPUB and 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

Notes

  1. 1.

    \(\beta \texttt {{\texttt {:}{} \texttt {:}}zero}\) is a type-class constraint on type \(\beta \), stipulating that there must be a distinguished constant 0 of type \(\beta \). See [9] for information on type classes in Isabelle/HOL.

  2. 2.

    This representation is also suggested in [10].

  3. 3.

    unit contains only one single element, so \(\alpha \times \texttt {unit}\) is isomorphic to \(\alpha \).

  4. 4.

    We take the liberty to use standard mathematical notation here, because Isabelle syntax does not integrate so well with informal text.

  5. 5.

    Abusing notation, \(x\in xs\), for a list xs, means that x appears in xs.

  6. 6.

    We use 0-based indexing of lists, vectors and matrices, just as Isabelle/HOL.

  7. 7.

    A polynomial is called monic if and only if its leading coefficient is 1.

  8. 8.

    The performance issues mainly concern the non-optimal representation of polynomials by unordered associative lists. We are currently working on a much more efficient representation by ordered associative lists.

References

  1. Ballarin, C.: Tutorial to locales and locale interpretation. In: Lambán, L., Romero, A., Rubio, J. (eds.) Contribuciones Científicas en Honor de Mirian Andrés Gómez, pp. 123–140. Servicio de Publicaciones de la Universidad de La Rioja (2010). Part of the Isabelle documentation: https://isabelle.in.tum.de/dist/Isabelle2017/doc/locales.pdf

  2. Bentkamp, A.: Expressiveness of deep learning. Archive of Formal Proofs (2016). Formal proof development: http://isa-afp.org/entries/Deep_Learning.html

  3. Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenrings nach einem nulldimensionalen Polynomideal. Ph.D. thesis, Mathematisches Institut, Universität Innsbruck, Austria (1965). English Translation in J. Symb. Comput. 41(3–4), 475–511 (2006)

    Google Scholar 

  4. Buchberger, B.: Towards the automated synthesis of a Gröbner bases algorithm. RACSAM, Serie A: Math. 98(1), 65–75 (2004)

    MathSciNet  MATH  Google Scholar 

  5. Chaieb, A., Wenzel, M.: Context aware calculation and deduction. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM 2007. LNCS (LNAI), vol. 4573, pp. 27–39. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_3

    Chapter  Google Scholar 

  6. Craciun, A.: Lazy thinking algorithm synthesis in Gröbner bases theory. Ph.D. thesis, RISC, Johannes Kepler University Linz, Austria (2008)

    Google Scholar 

  7. Faugère, J.C.: A new efficient algorithm for computing Gröbner bases (\(F_4\)). J. Pure Appl. Algebra 139(1), 61–88 (1999). https://doi.org/10.1016/S0022-4049(99)00005-5

    Article  MathSciNet  MATH  Google Scholar 

  8. Haftmann, F.: Code Generation from Isabelle/HOL Theories. Part of the Isabelle documentation: http://isabelle.in.tum.de/dist/Isabelle2017/doc/codegen.pdf

  9. Haftmann, F.: Haskell-Like Type Classes with Isabelle/Isar. Part of the Isabelle documentation: http://isabelle.in.tum.de/dist/Isabelle2017/doc/classes.pdf

  10. Haftmann, F., Lochbihler, A., Schreiner, W.: Towards Abstract and Executable Multivariate Polynomials in Isabelle (2014). Contributed talk at Isabelle Workshop 2014, associated with ITP 2014, Vienna, Austria: http://www.risc.jku.at/publications/download/risc_5012/IWS14.pdf

  11. Harrison, J.: Complex quantifier elimination in HOL. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001: Supplemental Proceedings, pp. 159–174. Division of Informatics, University of Edinburgh (2001). http://www.informatics.ed.ac.uk/publications/report/0046.html

  12. Immler, F., Maletzky, A.: Gröbner bases theory. Archive of Formal Proofs (2016). Formal proof development: http://isa-afp.org/entries/Groebner_Bases.html

  13. Immler, F., Maletzky, A.: Gröbner Bases of Modules and Faugère’s \(F_4\) Algorithm (formalization) (2018). Compatible with Isabelle 2017: http://www.risc.jku.at/people/amaletzk/CICM2018.html

  14. Jorge, J.S., Guilas, V.M., Freire, J.L.: Certifying properties of an efficient functional program for computing Gröbner bases. J. Symb. Comput. 44(5), 571–582 (2009). https://doi.org/10.1016/j.jsc.2007.07.016

    Article  MATH  Google Scholar 

  15. Kreuzer, M., Robbiano, L.: Computational Commutative Algebra 1. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-540-70628-1

    Book  MATH  Google Scholar 

  16. Maletzky, A.: Computer-assisted exploration of Gröbner bases theory in Theorema. Ph.D. thesis, RISC, Johannes Kepler University Linz, Austria (2016)

    Google Scholar 

  17. Maletzky, A., Immler, F.: Gröbner bases of modules and Faugère’s \(F_4\) algorithm in Isabelle/HOL (extended version). Technical report (2018). arXiv:1805.00304 [cs.LO]

  18. Medina-Bulo, I., Palomo-Lozano, F., Ruiz-Reina, J.L.: A verified common lisp implementation of Buchberger’s algorithm in ACL2. J. Symb. Comput. 45(1), 96–123 (2010). https://doi.org/10.1016/j.jsc.2009.07.002

    Article  MathSciNet  MATH  Google Scholar 

  19. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  20. Persson, H.: An integrated development of Buchberger’s algorithm in Coq. Technical report 4271. INRIA Sophia Antipolis (2001)

    Google Scholar 

  21. Schwarzweller, C.: Gröbner bases – theory refinement in the Mizar system. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol. 3863, pp. 299–314. Springer, Heidelberg (2006). https://doi.org/10.1007/11618027_20

    Chapter  Google Scholar 

  22. Sternagel, C., Thiemann, R.: Abstract rewriting. Archive of Formal Proofs (2010). Formal proof development: http://isa-afp.org/entries/Abstract-Rewriting.html

  23. Sternagel, C., Thiemann, R., Maletzky, A., Immler, F.: Executable multivariate polynomials. Archive of Formal Proofs (2010). Formal proof development: http://isa-afp.org/entries/Polynomials.html

  24. Théry, L.: A machine-checked implementation of Buchberger’s algorithm. J. Autom. Reason. 26(2), 107–137 (2001). https://doi.org/10.1023/A:1026518331905

    Article  MathSciNet  MATH  Google Scholar 

  25. Thiemann, R., Yamada, A.: Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs (2015). Formal proof development: http://isa-afp.org/entries/Jordan_Normal_Form.html

Download references

Acknowledgments

We thank the anonymous referees for their valuable comments.

Author information

Authors and Affiliations

  1. RISC, Johannes Kepler Universität Linz, Linz, Austria

    Alexander Maletzky

  2. Institut für Informatik, Technische Universität München, Munich, Germany

    Fabian Immler

Authors
  1. Alexander Maletzky
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabian Immler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Maletzky .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Bayern, Germany

    Florian Rabe

  2. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada

    William M. Farmer

  3. University of Cambridge, Cambridge, United Kingdom

    Grant O. Passmore

  4. Department of Computer Science, The George Washington University, Washington, District of Columbia, USA

    Abdou Youssef

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Maletzky, A., Immler, F. (2018). Gröbner Bases of Modules and Faugère’s \(F_4\) Algorithm in Isabelle/HOL. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-96812-4_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-96811-7

  • Online ISBN: 978-3-319-96812-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation