Neue Methoden in der Quantitativen Universellen Algebra

• Antragsteller: Professor Dr. Stefan Milius; Dr. Henning Urbat
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 569130867

Programmgleichungen, die die Verhaltensgleichheit zwischen syntaktisch unterschiedlichen Programmen ausdrücken, sind in der Informatik allgegenwärtig. Sie bilden die Grundlage für die Definition von Programmsemantiken, Programmtransformationen, Optimierungen usw. Das Gebiet der universellen Algebra (UA) stellt mathematische Methoden für den Umgang mit Gleichungen bereit. In vielen Anwendungen sind jedoch feinere Beschreibungsmittel erwünscht, die es erlauben auszudrücken, dass zwei Programme zwar verschiedenes aber sehr ähnliches Verhalten aufweisen. Die quantitative universelle Algebra (QUA), eine Verallgemeinerung der UA, die kürzlich von Mardare, Panangaden und Plotkin in einer einflussreichen Arbeit vorgeschlagen wurde, entwickelt die mathematischen Grundlagen für solche feineren Beschreibungen durch quantitative Programmgleichungen. In der QUA wird Verhaltensähnlichkeit quantitativ und numerisch durch das Konzept der metrischen Distanz erfasst. Man könnte beispielsweise in einem Programm einige Codezeilen durch andere, aber unter einer geeigneten Metrik hinreichend nahe, ersetzen und erwarten, dass das Ergebnis zum gegebenen Programm einen geringen Abstand hat. Quantitative algebraische Methoden erscheinen auch im Kontext von KI oder IoT sehr vielversprechend. In diesen Gebieten ist es wünschenswert, zuverlässige Ergebnisse zu erwarten, selbst wenn Eingaben, Parameter oder Sensordaten durch kleine Störungen beeinflusst werden könnten, z.B. durch Rauschen. Seit den ersten Arbeiten hat QUA beträchtliches Forschungsinteresse stimuliert und ist nun ein aktives Forschungsthema in der theoretischen Informatik. Die zwei an diesem ANR PRCI/DFG-Projekt beteiligten Forschungsgruppen haben dazu beide mit einer Reihe von Forschungsergebnissen beigetragen, die auf Top-Konferenzen publiziert wurden. Das Hauptziel dieses Projekts ist es nun, die Theorie und Anwendungen der quantitativen universellen Algebra zu einer umfassenden Theorie mit Ergebnissen, Konstruktionen und Werkzeugen für die mechanisierbare deduktive und algorithmische Behandlung von Spezifikationen mit quantitativen Aspekten voranzutreiben. Ein besonderer Schwerpunkt liegt auf der Spezifikation von Programmiersprachen mit quantitativer Struktur und kompositionaler Semantik sowie auf der Entwicklung effizienter Methoden zur Bestimmung von oberen und unteren Schranken für die Verhaltensabstände von Programmen. Ein weiterer wichtiger Zweck des Projekts ist die Förderung einer nachhaltigen Synergie zwischen den beiden Forschungsgruppen an der ENS Lyon und der FAU. Wir erwarten, dass diese weit über die Dauer des Projekts hinaus bestehen wird. Darüber hinaus wird die systematische und enge wissenschaftliche Zusammenarbeit der beiden Forschungsgruppen im Laufe des Projekts insbesondere den geförderten Forschern (zwei Postdoktoranden an der ENS-Lyon und ein Doktorand an der FAU) helfen, ein wissenschaftliches Netzwerk sowie internationale Kontakte und Kooperationen aufzubauen.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Frankreich
• Kooperationspartner: Dr. Matteo Mio