Effectful Programming in Declarative Languages with an Emphasis on Non-Determinism: Applications and Formal Reasoning

Diese Arbeit beschäftigt sich mit der deklarativen Programmierung mit Effekten und legt dabei besonderen Fokus auf Nichtdeterminismus als Effekt. Einerseits möchten wir Anwendungen entwickeln, deren zugrundeliegende Implementierungsidee auf Nichtdeterminismus basiert. Wir stellen dazu zwei beispielhafte Anwendungen vor, die in der funktional logischen Programmiersprache Curry implementiert sind. Die Kernidee dieser Implementierungen ist dabei die Kombination von Nichtstriktheit und Nichtdeterminismus, die Curry unterliegen, gewinnbringend auszunutzen. Für die erste Anwendung untersuchen wir Sortierfunktionen, die über eine Vergleichsfunktion parametrisiert sind, und wenden diese Funktionen auf ein nichtdeterministisches Prädikat an. Dabei entsteht eine Funktion, die Permutationen der Eingabeliste berechnet. Wir vergleichen unsere Implementierung in Curry mit einer Implementierung in Haskell, die den Nichtdeterminismus monadisch modelliert. Als zweite Anwendung werden wir über eine Bibliothek zur probabilistischen Programmierung diskutieren. Statt der üblichen Modellierung von Wahrscheinlichkeitsverteilungen als Liste von Paaren von Ereignis- und korrespondierenden Wahrscheinlichkeitswerten modellieren wir diese Verteilungen mithilfe von Currys nativem Nichtdeterminismus. Beide Implementierungen haben durch die Kombination von Nichtdeterminismus und Nichtstriktheit Vorteile gegenüber einer Implementierung, die den Nichtdeterminismus durch Listen repräsentiert. Andererseits möchten wir eine Möglichkeit schaffen, über die Programme, die wir in effektbehafteten deklarativen Programmiersprachen entwickelt haben, in einem formalen Rahmen zu argumentieren. Dabei fangen wir mit der Teilmenge der rein funktionalen Effekte an, das heißt, wir interessieren uns zunächst für totale und partielle Programme. Die zugrundeliegende Idee zur Modellierung dieser zwei Effekte kann dann auch für weitere Effekte genutzt werden. Als natürlichen nächsten Schritt betrachten wir den Effekt, der bei der Sprache Curry zusätzlich hinzukommt: nicht-strikter Nichtdeterminismus mit call-time choice Semantik. Dabei geben wir eine Übersicht darüber, warum die aktuelle Repräsentation call-by-name modelliert, sowie erste Ideen, wie die für Curry erforderliche call-by-need Semantik modelliert werden könnte.