University of Twente Student Theses
Error bounds for floating points in Isabelle/HOL
Beekman, BSc Lammert Jan Douwe (2024) Error bounds for floating points in Isabelle/HOL.
|
PDF
1MB |
| Abstract: | In computer calculations, floating point numbers are commonly used to represent real numbers. The downside of this is that these numbers cannot represent each real number exactly since the numbers are stored in a finite space and thus a rounding operation is necessary. There are multiple methods to know how big the error is for a calculation. This research expresses the errors in ulps (unit in last place). A single ulp is the distance between two numbers where only the least significant bit is different. Using this measurement we prove a bound on how the error increases after operations like addition and multiplication. The goal of this research includes proving all the conclusions in Isabelle/HOL. We also apply the theorems to an algorithm. The algorithm for which we prove an error bound is iterative matrix multiplication. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/99869 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page