Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

 

Title: Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
Authors: Ralph Bottesch, Jose Divasón and René Thiemann (rene /dot/ thiemann /at/ uibk /dot/ ac /dot/ at)
Submission date: 2021-03-12
Abstract: We verify two algorithms for which modular arithmetic plays an essential role: Storjohann's variant of the LLL lattice basis reduction algorithm and Kopparty's algorithm for computing the Hermite normal form of a matrix. To do this, we also formalize some facts about the modulo operation with symmetric range. Our implementations are based on the original papers, but are otherwise efficient. For basis reduction we formalize two versions: one that includes all of the optimizations/heuristics from Storjohann's paper, and one excluding a heuristic that we observed to often decrease efficiency. We also provide a fast, self-contained certifier for basis reduction, based on the efficient Hermite normal form algorithm.
BibTeX:
@article{Modular_arithmetic_LLL_and_HNF_algorithms-AFP,
  author  = {Ralph Bottesch and Jose Divasón and René Thiemann},
  title   = {Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Hermite, Jordan_Normal_Form, LLL_Basis_Reduction, Show, Smith_Normal_Form
Status: [skipped] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.