Eine High-Level-Sprache für monadenbasierte Prozesse

• Antragsteller: Privatdozent Dr.-Ing. Sergey Goncharov; Professor Dr. Lutz Schröder
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2012 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 215418801

Seiteneffekte treten bei der Programmierung in den verschiedensten Formen auf, z.B. Zugriff auf lokalen oder globalen Speicher, Ausnahmen, Nichtdeterminismus oder wiederaufnehmbare Berechnungen sowie Kombinationen mehrerer solcher Effekte. In der Semantik von Programmiersprachen ist die Modellierung von Seiteneffekten mittels Monaden weit verbreitet, und in der Tat findet sich dieses Paradigma bei einigen modernen Programmiersprachen wie etwa Haskell und F# auch in der Sprachsyntax selbst. Eine Monade ist, grob gesagt, ein Typkonstruktor, der jedem Typ von Werten einen Typ von seiteneffektbehafteten Berechnungen über solchen Werten zuordnet. Auf diesem Wege lassen sich Funktionen mit Seiteneffekten als reine (also seiteneffektfreie) Funktionen auffassen, die aber als Ergebnis eine Berechnung statt eines Wertes zurückgeben. Neben der so entstehenden Eingrenzung des Wirkungsbereichs von Seiteneffekten durch das Typsystem ist ein weiterer Vorteil der monadenbasierten Programmierung, dass sie Generizität über Seiteneffekten ermöglicht, d.h. Programme können über Monaden parametrisiert und später auf konkrete Seiteneffekte instanziiert werden; in den Haskell-Bibliotheken wird dies z.B. für generische Schleifenkonstrukte verwendet.Ziel von HighMoon ist es vor diesem Hintergrund, die Entwicklung von generischen Metasprachen und Verifikationslogiken für monadenbasierte Programme voranzutreiben. Die zweite Projektphase zielt darauf ab, aufbauend auf Grundlagenresultaten aus der ersten Projektphase generische Verifikationsmethoden für seiteneffektbehaftete nebenläufige Prozesse zur Verfügung zu stellen. Das Hauptaugenmerk unserer Forschung liegt dabei auf sogenannten Elgot-Monaden, also solchen Monaden, die (unbewachte) Iteration unterstützen, in Kombination mit freien Operatoren, die reaktives Verhalten wie z.B. wiederaufnehmbare Berechnungen und Interprozesskommunikation modellieren. Monaden, die diese Aspekte kombinieren, lassen sich als aus zwei Ebenen bestehend ansehen: eine extensionale Ebene, die den Nettoeffekt einzelner Berechnungsschritte widerspiegelt, und eine intensionale Ebene, die reaktive Aspekte modelliert. Zentrale Problemstellungen hinsichtlich Elgot-Monaden sind unter anderem die Charakterisierung der zugehörigen Algebren und die Entwicklung von Konstruktionen auf Elgot-Monaden, die es erlauben, systematisch Beispiele zu identifizieren. Wir beabsichtigen, in der ersten Projektphase entwickelte generische Verifikationslogiken für sequentielle monadenbasierte Programme hinsichtlich Ausdrucksstärke und Anwendbarkeit auszubauen sowie zu generischen Verifikationslogiken für nebenläufige monadenbasierte Programme weiterzuentwickeln. Für die so entstehenden Logiken werden wir (relativ) vollständige Beweiskalküle sowie Entscheidungsprozeduren für geeignet eingeschränkte Fragmente entwickeln.

• DFG-Verfahren: Sachbeihilfen