Login
- Document type:
- Masterarbeit
- Author(s):
- Schulz, Jakob
- Title:
- A Verified Functional Implementation of the Schönhage-Strassen-Algorithm
- Translated title:
- Eine Verifizierte Funktionale Implementierung des Schönhage-Strassen-Algorithmus
- Abstract:
- The Schönhage-Strassen-Algorithm multiplies two integers of length n in O(n log n log log n) steps on a multitape Turing machine. The main goal of this thesis is to give a verified implementation of the algorithm as well as verified runtime bounds. Integers are represented as LSBF (least significant bit first) boolean lists, on which simple algorithms for addition, subtraction and grid multiplication are given as well as a verified implementation of the Karatsuba-Multiplication with runtime O(nlog23). The already existing AFP-entry for Number Theoretic Transforms is adapted to a more general setting, which allows its application to certain quotient rings used in the Schönhage-Strassen-Algorithm. After some final preparations, an implementation of the Schönhage-Strassen-Algorithm with runtime O(n log n log log n) based on the original paper is given.
- Translated abstract:
- Der Schönhage-Strassen-Algorithmus multipliziert zwei ganze Zahlen der Länge n in O(n log n log log n) Schritten auf einer mehrbändigen Turing-Maschine. Zentrales Ziel dieser Arbeit ist es, eine verifizierte Implementierung sowie verifizierte Laufzeitschranken anzugeben. Als Repräsentation der Zahlen wählen wir boolsche Listen, auf denen zunächst grundlegende Algorithmen zur Addition, Subtraktion und klassischen Multiplikation angegeben werden, sowie eine verifizierte Implementierung der Karatsuba-Multiplikation mit Laufzeit O(nlog23). Der bereits vorhandene AFP-Eintrag zu Zahlentheoretischen Transformationen wird angepasst, um für bestimmte Restklassenringe anwendbar zu sein, die im Schönhage-Strassen-Algorithmus benötigt werden. Schließlich wird eine Implementierung des Schönhage-Strassen-Algorithmus mit der erwähnten Laufzeit von O(n log n log log n) basierend auf dem Original-Paper gegeben.
- Subject:
- MAT Mathematik
- DDC:
- 510 Mathematik
- Advisor:
- Karayel, Emin; Nipkow, Tobias (Prof. Dr.)
- Year:
- 2023
- Pages:
- 47
- Language:
- en
- Language from translation:
- de
- University:
- Technische Universität München
- Faculty:
- TUM School of Computation, Information and Technology
BibTeX