Berechnungen mit infiniten Daten: Programmextraktion aus Beweisen in einer um (ko)induktive Definitionen erweiterten konstruktiven Logik, die Berechnungsstärke und Anwendungen

• Antragsteller: Professor Dr. Dieter Spreen
• Fachliche Zuordnung: Theoretische Informatik ; Mathematik
• Förderung: Förderung seit 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 549144494

Die Berechenbarkeit mit endlichen Objekten wie den natürlichen Zahlen ist ein gut entwickeltes Forschungsgebiet, erste Untersuchungen reichen bis in die erste Hälfte des letzten Jahrhunderts zurück. Im Gegensatz dazu ist das Interesse am Rechnen mit unendlichen Objekten viel jünger. Ein Paradebeispiel für unendliche Daten sind die reellen Zahlen, die am häufigsten als unendliche Ziffernfolgen aufgefasst werden. Da die reellen Zahlen in der Mathematik von grundlegender Bedeutung sind, muss jeder Versuch, Objekte von mathematischem Interesse zu berechnen, auf einer Implementierung reeller Zahlen basieren. Bei Anwendungen in Wissenschaft und Technik werden die reellen Zahlen normalerweise durch Gleitkommazahlen mit fester endlicher Genauigkeit ersetzt. Allerdings ist diese Zahlenmenge noch nicht einmal unter den Grundrechenarten abgeschlossen. Folglich muss man sich mit Problemen auseinandersetzen, die sich aus der Rundung von Rechenergebnissen und den damit verbundenen Fehlern ergeben. Der Ansatz in diesem Projekt ist anders: Exakte reelle Zahlen bilden einen Basisdatentyp und obwohl jede Berechnung nur einen endlichen Teil ihrer Eingabe in endlicher Zeit verwenden kann, ist durch die Fortsetzung des Berechnungsprozesses immer eine höhere Genauigkeit erreichbar. Die Trennung zwischen der mathematischen Theorie und ihrer Umsetzung in Computerprogrammen wird umso problematischer, wenn die Korrektheit von Software in wissenschaftlichen Berechnungen formal nachgewiesen werden muss, was insbesondere bei der zunehmenden Zahl ingenieurwissenschaftlicher Anwendungen in sicherheitskritischen Bereichen der Fall ist. Das vorgeschlagene Projekt zielt darauf ab, den Umfang der Berechnungen mit unendlichen Daten auszudehnen und so den Anwendungsbereich zu erweitern. Es befasst sich mit grundlegenden Problemen, die gelöst werden müssen, um Algorithmen zu erhalten, die gleichzeitig effizient und formal als korrekt erwiesen sind. Ein Hauptthema wird die Berechenbarkeit auf hochdimensionalen Räumen und eine Fortführung des vom Antragsteller entwickelten Ansatzes zu Berechnungen auf dem Raum kompakter Mengen sein. Frühere Arbeiten zur Programmextraktion aus induktiven und koinduktiven Beweisen werden erweitert, um diese Probleme zu lösen und die Korrektheit der erhaltenen Algorithmen zu gewährleisten. Das Problem der Effizienz wird durch die Integration linearer Logik, die eine Kontrolle der Ressourcen ermöglicht, sowie Taylor-Modellen, die sich besonders gut für die Bearbeitung hochdimensionaler Rechenprobleme eignen, angegangen.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Frankreich, Großbritannien
• Kooperationspartner: Dr. Ulrich Berger; Dr. Jules Chouquet