Mathematisches Institut der Universität MünchenUniversität MünchenMathematisches Institut der Universität München

Konstruktive Analysis

Dozent: Helmut Schwichtenberg.


Proseminar: Di 16-18, Hörsaal 251. Beginn 20. April.
Tutorium: Do 16-18, Hörsaal K 35. Beginn 22. April.
Sprechstunde: Schwichtenberg Do 15-16, Zimmer 415.


Helmut Schwichtenberg, Constructive Logic, 27. April.
Maximilian Niklas, Real Numbers (pp.3-6), 4. Mai.
Eckhard Maass, Uncountability, Completeness, Limits and Inequalities (pp.9-13), 11. Mai.
Michael Lubasch, Series, Convergence Tests, Redundant Dyadic Representation (pp.13-18), 18. Mai.
Alexander Mathis, Exponential Series, Complex Numbers (pp.18-23), 8. Juni.
Christian Reiher, Continuous Functions (pp.23-30), 15. und 22. Juni.
Alex Schreiber, Intermediate Value Theorem (pp.30-33), 29. Juni.
Thomas Nowak, Differentiation (pp.33-36), 6. Juli.
Holger Blasum, Integration (pp.37-42), 13. Juli.
Parmenides Garcia Cornejo, Sequences of Functions (pp.47-53), 19. Juli (!), 14-16, Hörsaal E27.
Richard McKnight, ODEs (pp.54-58), 20. Juli.


Constructive Analysis (ps/pdf)



The goal is to develop the basics of real analysis in such a way that from a proof of an existence formula one can extract a program. For instance, from a proof of the intermediate value theorem we want to extract a program that, given an arbitrary error bound $2^{-k}$, computes a rational $x$ where the given function is zero up to the error bound. We will treat most subjects covered in the first year of standard calculus, including existence and uniqueness proofs of ODEs. Why should we be interested in logic in a study of constructive analysis? There are at least two reasons. (1) Obviously we need to be aware of the difference of the classical and the constructive existential quantifier, and try to prove the stronger statements involving the latter whenever possible. Then one is forced to give `constructive' proofs, whose algorithmic content can be `seen' and then used as a basis to formulate a program for computing the solution. (2) However, one can go one step further and automatize the step from the (formalized) constructive proof to the corresponding program. This can be done by means of the so-called realizability interpretation, whose existence was clear from the beginnings of constructive logic. The desire to have `mathematics as a numerical language' in this sense was clearly expressed by Bishop (in an article with just that title). Parallel there will be a separate (optional) 2 hour Praktikum, where the students should experiment with program extraction from particular proofs. There we will work with the Minlog System


For interactive generation of proofs we use the Minlog System, written in Scheme.


A protocol of what has been done is in tut.scm.

More detailed information on the general setup is available in numbers.scm. Some lemmata of Chapter 1: Real Numbers of the manuscript are proved formally in real.scm.

Helmut Schwichtenberg [Last updated 13.07.2004]