A generic and executable formalization of signature-based Gröbner basis algorithms. (September 2021)

• Record Type: Journal Article
• Authors: Maletzky, Alexander
• Is Part Of: Journal of symbolic computation. Volume 106(2021)
• Page Start: 23
• Page End: 47
• Publication Date: 2021-09
• Subjects: Gröbner bases -- Signature-based algorithms -- Interactive theorem proving -- Isabelle/HOL; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2020.12.001
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: We present a generic and executable formalization of signature-based algorithms (such as Faugère's F 5 ) for computing Gröbner bases, as well as their mathematical background, in the Isabelle/HOL proof assistant. Said algorithms are currently the best known algorithms for computing Gröbner bases in terms of computational efficiency. The formal development attempts to be as generic as possible, generalizing most known variants of signature-based algorithms, but at the same time the implemented functions are effectively executable on concrete input for efficiently computing mechanically verified Gröbner bases. Besides correctness the formalization also proves that under certain conditions the algorithms a-priori detect and avoid all useless reductions to zero, and return minimal signature Gröbner bases. To the best of our knowledge, the formalization presented here is the only formalization of signature-based Gröbner basis algorithms in existence so far.