1. Accurate calculation of Euclidean Norms using Double-word arithmetic
- Author
-
Vincent Lefèvre, Nicolas Louvet, Jean-Michel Muller, Joris Picot, Laurence Rideau, Arithmétiques des ordinateurs, méthodes formelles, génération de code (ARIC), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), Université Claude Bernard Lyon 1 (UCBL), Université de Lyon, Centre National de la Recherche Scientifique (CNRS), École normale supérieure de Lyon (ENS de Lyon), Sûreté du logiciel et Preuves Mathématiques Formalisées (STAMP), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), ANR-20-CE48-0014,NuSCAP,Sûreté numérique pour les preuves assistées par ordinateur(2020), Arithmetic and Computing (ARIC), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), École normale supérieure - Lyon (ENS Lyon), Muller, Jean-Michel, and Sûreté numérique pour les preuves assistées par ordinateur - - NuSCAP2020 - ANR-20-CE48-0014 - AAPG2020 - VALID
- Subjects
Formalization ,Euclidean norms ,Applied Mathematics ,[INFO.INFO-AO]Computer Science [cs]/Computer Arithmetic ,Square-root ,[INFO.INFO-OH]Computer Science [cs]/Other [cs.OH] ,Floating-Point arithmetic ,[INFO.INFO-OH] Computer Science [cs]/Other [cs.OH] ,Underflow ,[INFO.INFO-MS] Computer Science [cs]/Mathematical Software [cs.MS] ,Overflow ,Coq ,Double-double arithmetic ,[INFO.INFO-AO] Computer Science [cs]/Computer Arithmetic ,Hardware_ARITHMETICANDLOGICSTRUCTURES ,Proof assistant ,Software ,Double-word arithmetic ,[INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS] - Abstract
We consider the computation of the Euclidean (or L2) norm of an n -dimensional vector in floating-point arithmetic. We review the classical solutions used to avoid spurious overflow or underflow and/or to obtain very accurate results. We modify a recently published algorithm (that uses double-word arithmetic) to allow for a very accurate solution, free of spurious overflows and underflows. To that purpose, we use a double-word square-root algorithm of which we provide a tight error analysis. The returned L2 norm will be within very slightly more than 0.5 ulp from the exact result, which means that we will almost always provide correct rounding.
- Published
- 2023