Seminar: Konstruktive Analysis

Zeit und Ort

Mo 14-16, B252; Beginn Montag, 17. Oktober 2016

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 Kenntnisse in Mathematischer Logik (s. etwa Logik II). Ferner wird vorausgesetzt, daß die Teilnehmer das Tutorium des Beweisassistenten Minlog durchgearbeitet haben.
Nach erfolgreichem Besuch des Seminars ist es möglich, eine Bachelorarbeit zu einem Thema aus diesem Umkreis zu schreiben.

Vorträge

Die Vorträge wurden in der ersten Seminarsitzung am 17. Oktober verteilt.

• Reelle Zahlen: Gleichheit, Archimedische Eigenschaft. Franziskus Wiesnet, 24. Oktober
• Nicht-negative und positive reelle Zahlen. Alexander Schiefner, 31. Oktober
• Arithmetische Funktionen. Konstantin Schlagbauer (1), 7. November
• Vergleich reeller Zahlen. Nils Köpp (1), 21. November ( realari.scm, compreal.scm, RealNNegTimesCompat.scm)
• Vollständigkeit. Anton Bachschneider, 28. November
• Suprema und Infima. Quirin Schroll, 5. Dezember ( SupInf.pdf, SupremaInfima.scm)
• Stetige Funktionen, Zwischenwertsatz. Dieu Linh Tran (1), 12. Dezember
• Infima strikt konvexer Funktionen. Dieu Linh Tran (2), 19. Dezember
• Mittelwert reeller Zahlen in SD-Kodierung. Johanna Geins (1), 9. Januar
• Multiplikation reeller Zahlen in SD-Kodierung. Nils Köpp (2), 16. Januar
• Gray-Kodierung reeller Zahlen. Konstantin Schlagbauer (2), 23. Januar
• Multiplikation reeller Zahlen in Gray-Kodierung. Johanna Geins (2), 30. Januar

Sondertermine

• Tutorium zu Minlog, Mittwoch 19. Oktober, 16:00-17:30, B252
• Division mit Rest für Binärzahlen.
• Euklidischer Algorithmus für Binärzahlen.

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 (zuletzt aktualisiert am 19. Oktober)

Literatur

Allgemein

• Bishop/Bridges, Constructive Analysis, Kapitel 2. Springer 1985.
• Bridges/Vita, Techniques of Constructive Analysis. Springer 2006.
• A. Bauer, Five stages of accepting constructive mathematics (Bull AMS, 2016)

Speziell

• Skript Constructive analysis with witnesses (Stand 20. Dezember).
• Skript Logic for exact real arithmetic (Stand 30. Januar).
• Logic for Gray-code computation.
• Program extraction in exact real arithmetic.
• Program extraction for exact real arithmetic: Stream multiplication (Bachelorarbeit Till Überrück-Fries).
• cnt.scm (Stand 7. Dezember).
• grayrealeq20170113.scm (Stand 13. Januar).
• grayrealeq20170110.scm (Stand 10. Januar).
• grayrealeq20170104.scm (Stand 4. Januar).
• grayrealeq20161220.scm (Stand 20. Dezember).
• grayrealeq20161202.scm (Stand 2. Dezember).
• grayrealeq20161123.scm (Stand 23. November).
• grayrealeq.scm (Stand 17. Oktober).
• intqr.scm (Stand 28. Oktober).

Sprechstunde

• Helmut Schwichtenberg, Mi 13-14, B421.

Studienordnungen

Das Seminar ist unter P8 und WP6.3 (bzw. P15.1 und WP6.3) 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

30. Januar 2017