Blicke in die Unendlichkeit

9. April 2013, 18:35
posten

Stefan Hetzl erforscht eine Methode, mit der Mathematiker über endlos viele Fälle reden

Eines der grundlegendsten Probleme der Mathematik ist, wie man die Unendlichkeit in den Griff bekommt. Mit speziellen Regelwerken und Methoden, mit mathematischen "Tricks" muss man unendlicher Zahlenreihen, unendlich großer Mengen und unendlich vieler Rechenschritte Herr werden. Endliche Ausdrücke müssen genügen, um Unendliches zu beschreiben. Die Beweistheorie, ein Teilbereich der Logik, untersucht die Werkzeuge, vermöge deren man Aussagen für endlos viele Fälle tätigen will.

Stefan Hetzl vom Institut für Diskrete Mathematik und Geometrie der TU Wien untersucht eines dieser Werkzeuge: die Beweisführung mittels Vollständiger Induktion. Mit dieser mathematischen Methode können Aussagen über alle - also unendlich viele - natürlichen Zahlen bewiesen werden. Gleich einem Dominoeffekt überträgt man dabei eine mathematische Aussage von einer beliebigen Zahl auf die darauffolgende, um sie so für alle Zahlen zu beweisen. Hetzl will nun die Beweise selbst als mathematische Objekte - gleich geometrischen Körpern oder Funktionen - verwenden und so das Wissen über diese "Mathematik der Sprache der Mathematik" vertiefen. Dafür baut er mit Mitteln des Wiener Wissenschafts-, Forschungs- und Technologiefonds (WWTF), der sein Projekt mit 1,5 Millionen Euro im Rahmen des Programms Vienna Research Groups for Young Investigators fördert, in den nächsten Jahren eine Forschergruppe an der TU Wien auf.

Der Ansatzpunkt ist, Elemente der Sprachtheorie für die mathematische Beweistheorie zu verwenden. "In der Sprachtheorie kann man unterschiedliche Typen von Grammatiken beschreiben, die unterschiedliche Sprachen hervorbringen", sagt Hetzl. Grundlegende Mechanismen abstrakter, sogenannter formaler Sprachen sollen helfen, das Verständnis mathematischer Beweisführung zu vertiefen.

"Die Methode der Vollständigen Induktion ist gerade in der Informatik wichtig", sagt Hetzl. Wenn Programme etwa Schleifen durchlaufen, sei sie das richtige Beweiswerkzeug. Sogenannte Softwareverifikation, also das Überprüfen und mathematische Beschreiben von Programmen ist eines der Anwendungsgebiete, für das die Grundlagenforschung Hetzls relevant ist.

"Man will Computerprogramme haben, die sich richtig verhalten, egal welche der unendlich vielen denkbaren Eingaben sie bekommen", sagt Hetzl. Man müsse daher beweistheoretisch klug vorgehen: Eine endliche Anzahl von Schritten muss unendlich viele Möglichkeiten abdecken können. Am Ende des Projekts soll ein beispielhaftes Softwaretool stehen, das die theoretischen Erkenntnisse der Forschungsgruppe veranschaulicht.

Hetzl forschte zuletzt vier Jahre lang in Paris, wo, wie er sagt, universitäre Ausstattung und Forschungsmöglichkeiten jene von Wien weit übertreffen. Für das WWTF-Projekt kam er zurück an die TU, wo der 1981 geborene Wiener seine Hochschullaufbahn mit einem Informatikstudium begann. Erst als Student sei ihm klargeworden, was "richtige" Mathematik ist, sagt er, und es sei "dann von Jahr zu Jahr theoretischer geworden". Dass es generell in Richtung Informatik und Mathematik geht, sei aber schon früh, "seit dem ersten Commodore 64, den ich mit acht Jahren bekommen habe", klar gewesen, sagt Hetzl. (Alois Pumhösel, DER STANDARD, 10.4.2013)

  • Stefan Hetzl ist der Unendlichkeit auf der Spur.
    foto: hetzl

    Stefan Hetzl ist der Unendlichkeit auf der Spur.

Share if you care.