clUB III:

Sommersemester 2003
Helmut Schwichtenberg (Ludwig-Maximilians-Universität München): Konstruktive Analysis und Programmextraktion:

Aufbauend auf Brouwers Ideen einer konstruktiven Mathematik schrieb Errett Bishop 1967 ein sehr einflußreiches Buch mit dem Titel 'Foundations of Constructive Analysis'. Er versucht darin, im Stil eines gewöhnlichen Mathematik-Lehrbuchs -also informal- die Grundlagen der konstruktiven Analysis zu entwickeln.

In dem Vortrag soll es darum gehen, die Formalisierung dieser Überlegungen in einem geeigneten formalen System auf der Basis der Minimallogik zu erkunden. Dies eröffnet zumindest theoretisch die Möglichkeit, aus einem Existenzbeweis mit Hilfe der Realisierbarkeitsinterpretation ein Programm zu ertrahieren, das dann jedenfalls keine logischen Fehler mehr enthalten kann. Auch für die Numerik ist ein solcher Ansatz von Interesse, da man mit exakten reellen Zahlen arbeitet und deshalb Probleme mit der Fehlerfortpflanzung von vornherein ausgeschlossen sind.

Besonderes Gewicht wird darauf gelegt, die Typenstufe der extrahierten Programme niedrig zu halten. So ist zum Beispiel eine stetige Funktion bereits durch ihre Werte auf den rationalen Zahlen festgelegt und kann deshalb durch Daten der Typenstufe 1 beschrieben werden. Eine derartige Anreicherung der betrachteten Objekte durch Daten möglichst kleiner Typenstufe führt zu effizienteren extrahierten Programmen.


Last changed: June 10th, 2003