Seminar: Konstruktive Analysis
Zeit und Ort
Mo 14-16, B252; Beginn Montag, 23. Oktober 2023. Am 30. Oktober fällt das Seminar aus, und der 6. November ist reserviert für Aufnahmeprüfungen. Die Vorträge beginnen am 13. November.Inhalt
Es sollen die Grundlagen der konstruktiven Analysis erarbeitet und Anwendungsbeispiele behandelt werden, unter anderem die Funktionalgleichung der Exponentialfunktion. Die Beweise sollen auch in formalisierter Form geführt werden, um die Extraktion von Programmen zu ermöglichen. Vorausgesetzt werden Grundkenntnisse in Mathematischer 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
In den Vorträgen soll jeweils ein Teil der Implementierung in librea16.scm vorgestellt werden. Dazu gehören die Begriffe (Konstanten mit ihren Berechnungsregeln, induktiv definierte Prädikate, Variablennamen). Es soll eine Übersicht über ihre Eigenschaften (Theoreme) gegeben werden, und an einer oder mehreren Stellen der Beweis am Rechner geführt werden. Ausserdem soll eine Textfassung der behandelten Gegenstände angefertigt werden, die dann als Abschnitt in das Seminarskript eingefügt werden kann.- 20.11. Testino, Simone
nat: Natürliche Zahlen. *: Erweiterung einer endlichen Injektion zu einer Permutation. Eigenschaften von NatLeast. Textfassung - 27.11. Slimani, Mohammed
pos: Binärdarstellung natürlicher Zahlen. *: NatToPos, Rekursion nach einer Masszahl (GRec). Textfassung - 04.12. Schröter, Elias
rat: Ganze und rationale Zahlen. *: Dyadische rationale Zahlen (Nenner 2^n), siehe libdy.scm. Textfassung - 11.12. Grabmann, Konstantin
rea: Reelle Zahlen: Vergleich. *: RealEq aus RealLe definieren. Textfassung - 18.12. Schropp, Leon
rseq, 1: Vollständigkeit, Konvergenz. *: Metrische Räume. Textfassung - 08.01 (ausgefallen). Yang, Tiansheng
rseq, 2: Summen. *: Bedingte Summen - 15.01. Gruben, Niko
rseq, 3-5: Doppelsummen. *: Paarkodierung. Textfassung - 22.01. Herrmann, Valentin
rseq, Rest: Die Exponentialreihe. *: Eigenschaften von exp(x): >=0, >0. e^x. Textfassung - 29.01 und 05.02. Bondarenko, Dymytro
Komplexe Zahlen. *: sin, cos. Textfassung
Minlog
Eine ausführliche Einführung in Minlog (von Franziskus Wiesnet) ist hier. 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-ZweigMinlogpad (von Valentin Herrmann) erlaubt das Arbeiten mit Minlog ohne das System zu installieren.
Um sich über Minlog auszutauschen, Fragen zu stellen oder auch Fragen zu beantworten, können Sie der Minlog Community auf Zulip (minlog.zulipchat.com) beitreten. Zulip läuft direkt im Browser, ist aber auch als Desktopanwendung oder App erhältlich. In der Community können Sie beispielsweise im #questions Stream Fragen stellen und andere Minlognutzer dabei unterstützen, ihre Wissenslücken zu schliessen.
Literatur
Allgemein
- Bishop/Bridges, Constructive Analysis. Springer 1985.
- A. Bauer, Five stages of accepting constructive mathematics (Bull AMS, 2016)
- Handbook of Constructive Mathematics. Cambridge UP, 2023
Speziell
- Skript Constructive analysis with witnesses
- librseq16.scm
- libnat.scm
- liblist.scm
- librea.scm
- libnatrootpair.scm
- fphind.scm
- libdy.scm
Sprechstunde
- Helmut Schwichtenberg, Mi 13-14, B434.