The computational content of abstract algebra and analysis

Wiesnet, Franziskus (2021): The computational content of abstract algebra and analysis. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik

Abstract

In this dissertation we discuss several forms of proof interpretation based on examples in algebra and analysis. Our main goal is the construction of algorithms or functions out of proofs - constructive proofs and classical proofs. At the beginning of this dissertation the constructive handling of Zorn's lemma in proofs of algebra plays a main role. We consider maximal objects and their approximations in various algebraic structures. The approximation is inspired by Gödel's functional interpretation and methods from proof mining. Proof mining is a branch of mathematical logic which analyses classical existence statements to get explicit bounds. We describe a recursive algorithm which constructs a sequence of approximations until they become close enough. This algorithm will be applied to Krull's lemma and its generalisation: the universal Krull-Lindenbaum lemma. In some case studies and applications like the theorem of Gauß-Joyal and Kronecker's theorem we show explicit uses of this algorithm. By considering Zariski's lemma we present how a manual construction of an algorithm from a constructive proof works. We present a constructive proof of Zariski's lemma, and use this proof as inspiration to formulate an algorithm and a computational interpretation of Zariski's lemma. Finally, we prove that the algorithm indeed fulfils the computational interpretation. As an outlook we sketch how this algorithm could be combined with our state-based algorithm from above which constructs approximations of maximal objects, to get an algorithm for Hilbert's Nullstellensatz. We then take a closer look at an example of an algorithm which is extracted out of a constructive proof by using the proof assistant Minlog. We use coinductively defined predicates to prove that the signed digit representation of real numbers is closed under limits of convergent sequences. From a formal proof in Minlog, the computer generates an algorithm, a soundness theorem and a proof of the soundness theorem corresponding to the convergence theorem out of our formalisation. The convergence theorem is applied to Heron's method to get an algorithm which computes the signed digit representation of the square root of a non-negative real number out of its signed digit representation. Here we use the programming language Haskell to display the computational content. As second application we show that the signed digit code is closed under multiplication and state the corresponding algorithm. The dissertation is concluded by an example of proof mining in analysis. We consider one convergence lemma with a classical proof, use techniques of proof mining to get a new lemma with a rate of convergence, and apply the new lemma to various fixed-point theorems for asymptotically weakly contractive maps and their variants. In the last step, beside extracting quantitative information - in our case rates of convergence - from proofs, we also discuss the usage of proof mining to generalise or combine theorems.

Abstract

In dieser Dissertation diskutieren wir verschiedene Formen der Beweisinterpretation anhand von Beispielen aus der Algebra und Analysis. Unser Ziel ist dabei immer die Konstruktion von Algorithmen oder Funktionen aus Beweisen – sowohl klassischen wie auch konstruktiven Beweisen. Am Anfang der Dissertation gehen wir auf eine konstruktive Behandlung von Zorns Lemma in Beweisen der Algebra ein. Insbesondere betrachten wir maximale Objekte und deren Approximationen in verschiedenen algebraischen Strukturen. Die Approximation ist dabei inspiriert durch Gödels Funktionalinterpretation und Methoden des Proofminings. Proofmining ist ein Teilgebiet der mathematischen Logik, welches klassische Existenzbeweise analysiert, um explizite Schranken zu extrahieren. Wir geben einen rekursiven Algorithmus an, welcher eine Folge von Approximationen konstruiert bis diese hinreichend genau sind. Dieser Algorithmus wird anschließend auf Krulls Lemma und seine Verallgemeinerung angewandt: dem universellen Krull-Lindenbaum-Lemma. In einigen Fallstudien und Beispielen wie dem Satz von Gauß-Joyal und Kroneckers Lemma zeigen wir ganz explizite Anwendungen des Algorithmus. Anhand von Zariskis Lemma zeigen wir, wie man einen Algorithmus von Hand ohne Computerhilfe aus einem konstruktiven Beweis extrahieren kann. Hierbei geben wir zunächst einen konstruktiven Beweis von Zariskis Lemma an. Diesen Beweis nutzen wir als Inspiration, um einen Algorithmus und eine rechnerische Interpretation von Zariskis Lemma zu formulieren. Abschließend beweisen wir, dass der Algorithmus tatsächlich die rechnerische Interpretation erfüllt. Als Ausblick skizzieren wir, wie dieser Algorithmus angewandt werden kann, um einen Algorithmus für Hilberts Nullstellensatz zu erhalten. Dabei verwenden wir auch den zuvor entwickelten Algorithmus, welcher Approximationen von maximalen Objekten konstruiert. Nach dieser manuellen Extraktion eines Algorithmus aus einem konstruktiven Beweis kommen wir zu einem Beispiel automatischer Beweisextraktion mit Hilfe von Computerunterstützung. In unserem Fall verwenden wir den Beweisassistenten Minlog. Unter Verwendung von coinduktiven Prädikaten zeigen wir, dass die Binärdarstellung mit Vorzeichen abgeschlossen unter der Bildung von Grenzwerten konvergenter Folgen ist. Nach der Formalisierung in Minlog erzeugt der Computer einen Algorithmus, eine Korrektheitsaussage und einen Beweis dieser Aussage für unser Konvergenztheorem. Dieses Konvergenztheorem wird anschließend auf das Heron-Verfahren angewandt, um einen Algorithmus zu erhalten, welcher die Binärdarstellung mit Vorzeichen einer nicht-negativen reeller Zahl zu der Binärdarstellung mit Vorzeichen ihrer Wurzel transformiert. Um diesen Algorithmus anzuwenden, verwenden wir die Programmiersprache Haskell. Als zweite Anwendung zeigen wir, dass die Binärdarstellung mit Vorzeichen abgeschlossen unter Multiplikation ist, und geben dazu einen Algorithmus an. Im letzten Kapitel diskutieren wir ein Beispiel von Proofmining in der Analysis. Hierbei betrachten wir ein Konvergenzlemma und verwenden Techniken des Proofminings, um eine Konvergenzrate zu erhalten. Wir wenden das neue Lemma auf verschiedene Fixpunktsätze für asymptotisch schwach kontraktive Abbildungen und deren Varianten an. Bei dem letzten Schritt diskutieren wir nicht nur die Extraktion von quantitativen Informationen - in unserem Fall Konvergenzraten - aus Beweisen, sondern auch die Anwendung von Proofmining, um Sätze zu verallgemeinern und zu kombinieren.

• Dokumententyp: Dissertationen (Dissertation, LMU München)
• Themengebiete: 500 Naturwissenschaften und Mathematik
• Fakultäten: Fakultät für Mathematik, Informatik und Statistik
• Sprache der Hochschulschrift: Englisch
• Datum der mündlichen Prüfung: 3. August 2021
• 1. Bericht­erstatter:in: Schwichtenberg, Helmut