A generic and executable formalization of signature-based Gröbner basis algorithms. (English) Zbl 1467.13050

Maletzky, Alexander

J. Symb. Comput. 106, 23-47 (2021).

The article describes a formalization of signature-based algorithms [C. Eder and J.-C. Faugère, J. Symb. Comput. 80, Part 3, 719–784 (2017; Zbl 1412.68306)] to compute Gröbner bases for the proof assistant Isabelle, “a framework for implementing different object logics, such as first-order logic or higher-order logic, in one single system,” using Isabelle/HOL, “a concrete object [higher-order predicate] logic implemented in Isabelle” [T. Nipkow et al., Isabelle/HOL. A proof assistant for higher-order logic. Berlin: Springer (2002; Zbl 0994.68131)]. Isabelle includes a capability to generate code that effectively computes Gröbner bases, though the resulting code is (unsurprisingly) slower than existing implementations. As the author reports, this seems to be the first formalization of signature-based computation in any proof assistant.
The formalization has shown that an algorithm to compute a generic formalization called rewrite bases terminates correctly for all inputs, and for certain inputs avoids all zero reductions. It allows for arbitrary term- and rewrite-orders. Correctness depends on certain details that implementations typically follow, such as selecting for processing the signature-pair with minimal signature.
The article attempts to be self-contained, and includes an overview of the Isabelle/HOL proof assistant. However, it omits many mathematical details for the sake of brevity, and recommends that readers not already familiar with the topic refer to the 2017 survey by Eder and Faugère cited in this review’s first sentence.
The article is a relatively straightforward read. The introduction explains the structure of the exposition, and much of the article consists simply of reviewing definitions and theorems from Eder and Faugère, then explaining how they are “translated” into Isabelle’s language. A link is provided to the code, which includes a proof outline, a proof document (243 pages!), and Theories used in the proof. The conclusion points the reader to related work, both in Isabelle and other proof assistants, and outlines possibilities for future work.

Reviewer: John Perry (Hattiesburg)

MSC:

13P10	Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases)
68W30	Symbolic computation and algebraic computation
68V20	Formalization of mathematics in connection with theorem provers

Keywords:

Gröbner bases; signature-based algorithms; interactive theorem proving; Isabelle/HOL

Citations:

Zbl 1412.68306; Zbl 0994.68131

Software:

Coq; Isar; Isabelle; Isabelle/Isar; Isabelle/HOL; F5C; HOL; Mizar

References:

[1]	Ballarin, C., Tutorial to locales and locale interpretation, (Lambán, L.; Romero, A.; Rubio, J., Contribuciones Científicas en Honor de Mirian Andrés Gómez (2010), Servicio de Publicaciones de la Universidad de la: Servicio de Publicaciones de la Universidad de la Rioja), 123-140, Part of the Isabelle documentation · Zbl 1215.68208
[2]	Bancerek, G.; Byliński, C.; Grabowski, A.; Korniłowicz, A.; Matuszewski, R.; Naumowicz, A.; Pąk, K.; Urban, J., Mizar: state-of-the-art and beyond, (Kerber, M.; Carette, J.; Kaliszyk, C.; Rabe, F.; Sorge, V., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Proceedings of CICM 2015, Washington D.C., US, July 13-17 (2015), Springer), 261-279 · Zbl 1417.68201
[3]	Bertot, Y.; Castéran, P., Interactive theorem proving and program development - Coq’Art: the calculus of inductive constructions, (Texts in Theoretical Computer Science. Texts in Theoretical Computer Science, An EATCS Series (2004), Springer) · Zbl 1069.68095
[4]	Buchberger, B., Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal (An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal), Special Issue on Logic, Mathematics, and Computer Science: Interactions. Special Issue on Logic, Mathematics, and Computer Science: Interactions, J. Symb. Comput., 41, 3-4, 475-511 (2006), University of Innsbruck: University of Innsbruck Austria, English translation
[5]	Buchberger, B., Towards the automated synthesis of a Gröbner bases algorithm, RACSAM - Rev. R. Acad. Cienc., Ser. A: Math., 98, 65-75 (2004) · Zbl 1088.68187
[6]	Buchberger, B.; Jebelean, T.; Kutsia, T.; Maletzky, A.; Windsteiger, W., Theorema 2.0: computer-assisted natural-style mathematics, J. Formaliz. Reason., 9, 149-185 (2016) · Zbl 1451.68319
[7]	Chaieb, A.; Wenzel, M., Context aware calculation and deduction: ring equalities via Gröbner bases in Isabelle, (Kauers, M.; Kerber, M.; Miner, R.; Windsteiger, W., Towards Mechanized Mathematical Assistants. Towards Mechanized Mathematical Assistants, Proceedings of Calculemus’2007, Hagenberg, Austria, June 27-30 (2007), Springer), 27-39 · Zbl 1202.68375
[8]	Crăciun, A., Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory (2008), Johannes Kepler University: Johannes Kepler University Linz, Austria, Ph.D. thesis. RISC
[9]	Eder, C.; Faugère, J. C., A survey on signature-based algorithms for computing Gröbner bases, J. Symb. Comput., 80, 719-784 (2017) · Zbl 1412.68306
[10]	Eder, C.; Perry, J., F5C: a variant of Faugère’s \(F_5\) algorithm with reduced Gröbner bases, J. Symb. Comput., 45, 1442-1458 (2010) · Zbl 1227.13018
[11]	Eder, C.; Roune, B. H., Signature rewriting in Gröbner basis computation, (Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation (2013), ACM), 331-338 · Zbl 1360.68929
[12]	Faugère, J. C., A new efficient algorithm for computing Gröbner bases \(( F_4)\), J. Pure Appl. Algebra, 139, 61-88 (1999) · Zbl 0930.68174
[13]	Faugère, J. C., A new efficient algorithm for computing Gröbner bases without reduction to zero \(( F_5)\), (Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation (2002), ACM), 75-83 · Zbl 1072.68664
[14]	Galkin, V., Termination of original \(F_5 (2012)\)
[15]	Haftmann, F.; Bulwahn, L., Code Generation from Isabelle/HOL Theories. Part of the Isabelle Documentation (2018)
[16]	Haftmann, F.; Krauss, A.; Kunčar, O.; Nipkow, T., Data refinement in Isabelle/HOL, (Blazy, S.; Paulin-Mohring, C.; Pichardie, D., Interactive Theorem Proving. Interactive Theorem Proving, Proceedings of ITP’2013, Rennes, France, July 22-26 (2013), Springer), 100-115 · Zbl 1317.68212
[17]	Harrison, J., Complex quantifier elimination in HOL, (Boulton, R. J.; Jackson, P. B., TPHOLs 2001: Supplemental Proceedings, Division of Informatics (2001), University of Edinburgh), 159-174
[18]	Immler, F.; Maletzky, A., Gröbner bases theory (2016), Formal proof development
[19]	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, 571-582 (2009) · Zbl 1159.13016
[20]	Kaufmann, M.; Manolios, P.; Moore, J. S., Computer-Aided Reasoning: An Approach (2000), Kluwer Academic Publishers
[21]	Maletzky, A., Computer-Assisted Exploration of Gröbner Bases Theory in Theorema (2016), Johannes Kepler University Linz, Ph.D. thesis. RISC
[22]	Maletzky, A., Signature-based Gröbner basis algorithms (2018), Formal proof development
[23]	Maletzky, A.; Immler, F., Gröbner bases of modules and faugère’s \(F_4\) algorithm in Isabelle/HOL, (Rabe, F.; Farmer, W.; Passmore, G.; Youssef, A., Intelligent Computer Mathematics. Intelligent Computer Mathematics, Proceedings of CICM 2018, Hagenberg, Austria, August 13-17 (2018), Springer), 178-193 · Zbl 1417.68189
[24]	Maletzky, A.; Immler, F., Gröbner Bases of Modules and Faugère’s \(F_4\) Algorithm in Isabelle/HOL (extended version) (2018), RISC, JKU Linz, Technical Report · Zbl 1417.68189
[25]	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, 96-123 (2010) · Zbl 1194.68155
[26]	Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL—a Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer · Zbl 0994.68131
[27]	Pan, S.; Hu, Y.; Wang, B., The termination of algorithms for computing Gröbner bases (2012)
[28]	Paulson, L. C., Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science., vol. 828 (1994), Springer · Zbl 0825.68059
[29]	Persson, H., An Integrated Development of Buchberger’s Algorithm in Coq (2001), INRIA Sophia Antipolis, Technical Report 4271
[30]	Roune, B. H.; Stillman, M., Practical Gröbner basis computation, (Proceedings of the 37th International Symposium on Symbolic and Algebraic Computation (2012), ACM), 203-210 · Zbl 1308.68185
[31]	Schwarzweller, C., Gröbner bases – theory refinement in the Mizar system, (Kohlhase, M., Mathematical Knowledge Management. Mathematical Knowledge Management, 4th International Conference, Bremen, Germany, July 15-17 (2006), Springer), 299-314 · Zbl 1151.68673
[32]	Stegers, T., Faugère’s \(F_5\) Algorithm Revisited (2006), Technische Universität Darmstadt: Technische Universität Darmstadt Germany, Master’s thesis
[33]	Sternagel, C.; Thiemann, R.; Maletzky, A.; Immler, F.; Haftmann, F.; Lochbihler, A.; Bentkamp, A., Executable multivariate polynomials (2010), Formal proof development
[34]	Théry, L., A machine-checked implementation of Buchberger’s algorithm, J. Autom. Reason., 26, 107-137 (2001) · Zbl 0964.03012
[35]	Wenzel, M., The Isabelle/Isar Reference Manual. Part of the Isabelle Documentation (2018)