| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |