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

The article describes a formalization of signature-based algorithms [\textit{C. Eder} and \textit{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'' [\textit{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 \textit{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.