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

Proseminar Konstruktive Analysis

Dozent: Helmut Schwichtenberg.

Termine

Proseminar: Di 16-18, Hörsaal 252. Beginn 12. April 2005.
Sprechstunde: Schwichtenberg Mo 14-15, Zimmer 415.

Vorträge

1. Free algebras, recursion (mlcf 2.1-2), 19. April.
2. Languages for algebras, induction (mlcf 2.4.1-4), 26. April.
3. Constructive logic (Skript Mathematical Logic I, van Dalen), 3. Mai. Emil Wiedemann
4. Program extraction from constructive proofs (mlcf 4.2-4.3.1), 10. Mai.
5. Examples: Binary numbers, Euclidean algorithm (numbers.scm, gcd.scm), 24. Mai. Andreas Wadhwa
6. Real numbers (constr, pp.4-10), 7. Juni. Andreas Lauer
7. Real numbers: Uncountability, completeness, limits and inequalities (constr, pp.11-15), 14. Juni. Luba Stein
8. Continuous functions (constr, pp.25-30) (2 Termine), 21. und 28. Juni. Aniko Öry
9. Intermediate value theorem (constr, pp.30-32), 5. Juli. Judith Gampe

Schriftliches Material zu den Vorträgen

1. Free algebras, recursion (ps/pdf)
2. Languages for algebras, induction (ps/pdf)
4. Program extraction from constructive proofs (ps/pdf)

Skripten

Literatur

Contents

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 $a$ where the given function is zero up to the error bound. We will treat most subjects covered in the first year of standard calculus.

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. This amounts to something like `mathematics as a numerical language' (a term due to Bishop).

Helmut Schwichtenberg [Last updated 14.06.2005]