Seminar: Konstruktive Analysis

Zeit und Ort

Mo 14-16, B252; Beginn Montag, 25. Oktober 2021

Inhalt

Es sollen die Grundlagen der konstruktiven Analysis erarbeitet werden. Die Beweise sollen auch in formalisierter Form geführt werden, um die Extraktion von Programmen zu ermöglichen. Vorausgesetzt werden Grundkenntnisse in Mathematischer Logik (in der Regel die Vorlesung Logik II vom SS 2021, mindestens aber der gleichzeitige Besuch der einführenden Vorlesung "Mathematische Logik"). Ferner wird vorausgesetzt, daß die Teilnehmer das Tutorium des Beweisassistenten Minlog durchgearbeitet haben.
Nach erfolgreichem Besuch des Seminars ist es möglich, eine Bachelor- oder Masterarbeit zu einem Thema aus diesem Umkreis zu schreiben.

Vorträge

Die Vorträge werden in der ersten Seminarsitzung am 25. Oktober verteilt.

• Einführung: Zahlsysteme, Programmextraktion. 8. November 2021 (intronum.scm)
• Reelle Zahlen: Gleichheit, nicht-negative und positive reelle Zahlen. Meike Beatrice Lorenz, 15. November 2021. (1.2-1.4 im Skript1) (Bickford-Skript)
• Arithmetische Funktionen. Tobias Schwaiger, 29. November 2021. (1.5)
• Vergleich reeller Zahlen. Armin Heydari, 6. Dezember 2021. (1.6)
• Vollständigkeit. Meike Beatrice Lorenz, 13. Dezember 2021. (2.1) und Teil 1 (Completeness) von rseq.scm
• Konvergenz reeller Folgen. Armin Heydari, 20. Dezember 2021. Teil 2 (Convergence) von rseq.scm
• Vektorverbände. Charlotte Dorneich, 10. Januar 2022.
• TBA. Tobias Schwaiger, 17. Januar 2022.

Weitere Themen (ursprüngliche Planung)

• Vervollständigung metrischer Räume. (2 im Skript2)
• Schrittfunktionen als Vektorverband. (1 im Skript2, vlat.scm)
• Integration. (3 im Skript2, vlat.scm)
• Dyadische rationale Zahlen. (dy.scm)
• Reelle Zahlen basierend auf dyadischen rationalen Zahlen
• Konvergenz reeller Folgen basierend auf dyadischen rationalen Zahlen

Minlog

Minlog ist auf den CIP-Rechnern des Mathematischen Instituts installiert (Aufruf: minlog). Falls git auf Ihrem Rechner installiert ist, können Sie die jeweils aktuelle Version von Minlog erhalten durch Ausführen von
git clone http://www.math.lmu.de/~minlogit/git/minlog.git
Bitte verwenden Sie (via git checkout dev) den dev-Zweig (Stand 25. Oktober 2021).

Literatur

Allgemein

• Bishop/Bridges, Constructive Analysis. Springer 1985.
• Bridges/Vita, Techniques of Constructive Analysis. Springer 2006.
• A. Bauer, Five stages of accepting constructive mathematics (Bull AMS, 2016)
• Link zu der Bishop/Bridges-version von nuprl:
  www.nuprl.org/MathLibrary/ConstructiveAnalysis/Constructive_Analysis_Ch2.html

Speziell

• H. Ishihara, The constructive Hahn-Banach theorem, revisited
• N. Köpp, Automatically verified program extraction from proofs with applications to constructive analysis
• Skript1 Constructive analysis with witnesses
• Skript2 Constructive integration
• Referenzbaum rea.rtr zu rea.scm.
• Referenzbaum rseq.rtr zu rseq.scm.

Sprechstunde

• Helmut Schwichtenberg, Mi 13-14, B434.

Studienordnungen

Das Seminar ist unter P8 und WP6.3 (bzw. WP7) in der Bachelorstudienordnung Mathematik (bzw. Wirtschaftsmathematik) aufgelistet (3 ECTS Punkte). Im Masterstudium Mathematik (bzw. Wirtschaftsmathematik) kann es als Teilmodul 14.2 (zusammen mit 14.1 Tutorentraining) oder 16.2 (zusammen mit 16.1 Seminar) eingebracht werden.

Letzte Änderung

10. Januar 2021