Email Gateway (Mar 14 2021 at 11:13): Email Gateway (Mar 14 2021 at 11:13):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
I'm happy to announce another AFP entry this week:
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal
form computation
by Ralph Bottesch, Jose Divason and Rene Thiemann
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.
https://www.isa-afp.org/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html
Andreas
Last updated: Jul 15 2022 at 23:21 UTC