Funktionallogische Programmierung

Die Funktionallogische Programmierung ist die Vereinigung des funktionalen mit dem logischen Paradigma in einer Programmiersprache. Dies schließt die meisten starken Konzepte der Paradigmen mit ein, dazu gehören Funktionen höherer Ordnung, nicht-deterministische Ausführung, Unifikation. Wegbereiter dieser Schöpfung war λProlog in den Neunzigern. Andere, neuere Funktionallogische Programmiersprachen sind Curry and Mercury.

Grundlagen

Einfache Konzepte

Ein funktionales Programm ist eine Ansammlung von Funktionen oder Regeln. Eine funktionale Berechnung besteht aus dem Ersetzen von Teilausdrücken durch (unter Berücksichtigung der Funktionsdefinition) gleichwertige Teilausdrücke, solange bis keine Ersetzungen bzw. Reduktionen mehr möglich sind und ein Ergebnis bestimmt oder eine Normalform erreicht wird. Beispielsweise die Funktion verdoppeln, definiert als

verdoppeln x  =  x + x

Der Ausdruck verdoppeln 1 wird durch 1 + 1 ersetzt, was wiederum durch 2 ersetzt werden kann, wenn wir den +-Operator als eine unendliche Menge von Gleichungen der Form 1 + 1 = 2, 1 + 2 = 3, … auffassen. Auf ähnliche Weise können Teilausdrücke ausgewertet werden. Im Beispiel wird der zu ersetzende Teilausdruck kursiv hervorgehoben.

verdoppeln (1 + 2)  →  (1 + 2) + (1 + 2)  →  3 + (1 + 2)  →  3 + 3  →  6

Es gibt aber auch noch eine andere Reihenfolge in der die Ausdrücke ersetzt werden können:

verdoppeln (1 + 2)  →  (1 + 2) + (1 + 2)  →  (1 + 2) + 3  →  3 + 3  →  6

In diesem Fall führen beide Auswertungen zum gleichen Resultat. Diese Eigenschaft heißt Konfluenz und folgt aus der fundamentalen Eigenschaft reiner funktionaler Sprachen, der referenziellen Transparenz: der zu bestimmende Wert eines Ausdrucks hängt nicht aufgrund von Seiteneffekten von der Reihenfolge oder dem Zeitpunkt ab. Daher sind Beweise leichter zu führen und die Programme leicht wartbar.

Ebenso wie funktionale Sprachen unterstützt Curry die Definition von algebraischen Typen indem ihre Konstruktoren aufgelistet werden. Beispielsweise wird der Datentyp Bool für Wahrheitswerte mit den Konstruktoren True und False wie folgt definiert:

data Bool  =  True | False

Funktionen, deren Parameter solche Wahrheitswerte sind, können durch Pattern Matching definiert werden, z. B. durch mehrere definierende Gleichungen:

not True   =  False
not False  =  True

Das Vorgehen Ausdrücke durch gleichwertige zu ersetzen ist weiterhin gültig, wenn die Ausdrücke die entsprechende Form haben:

not (not False)  →  not True  →  False

Kompliziertere Datenstrukturen werden durch rekursive Datentypen dargestellt. Beispielsweise eine Liste über einem beliebigen Typen, deren Elemente ebendiesen Typ haben, ist entweder die leere Liste [] oder eine nicht-leere Liste mit einem ersten Element x und einem Restglied xs, dargestellt durch x : xs.

data List a  =  []           -- [] ist ein parameterloser Konstruktor (d. h. ein Literal), das die leere Liste darstellt.
             |  a : List a   -- Der Konstruktor wird infix notiert und ist der Doppelpunkt. Er hat zwei Parameter: ein Listenelement und ein Restglied, welches auch leer sein darf.

Üblicherweise notiert man den Typ List a mit [a] und endliche Listen x1 : x2 : … : xn : [] mit [x1, x2, …, xn]. Funktionen auf rekursiven Typen können induktiv definiert werden, wobei Pattern Matching bequemes Fallunterscheiden ermöglicht. Die Konkatenation kann wie folgt definiert werden. Die beiden konkatenierten Listen müssen vom gleichen Typen sein; die Typangabe des Operators ist optional.

(++) :: [a] -> [a] -> [a]          -- Typdefinition: Zwei Listen mit gleichem Typ werden zu einer.

[]       ++ ys  =  ys              -- Leere Liste mit beliebiger Liste konkatenieren
(x : xs) ++ ys  =  x : (xs ++ ys)  -- Nicht-leere Liste rekursiv konkatenieren

Über die direkte Verwendung hinaus ist der ++-Operator auch nützlich, um das Verhalten von anderen Funktionen zu spezifizieren. Es sei zur Demonstration die Funktion last, die das letzte Element einer nicht-leeren Liste zurückgibt. Für alle Listen xs und Elemente e gilt: last xs = e genau dann, wenn es ys derart gibt, dass ys ++ [e] = xs. (Das Gleichheitszeichen ist nicht als Sprachelement hervorgehoben, da es Identität vermitteln soll, und insbesondere nicht eine in der Programmiersprache definierte Gleichheitsoperation, auch wenn diese durch einen anderen Operator dargestellt wird.)

Basierend auf dieser Spezifikation können wir mittels logischer Programmiertechniken eine Funktion definieren, die diese erfüllt. Ähnlich wie logische Sprachen bieten funktionallogische Sprachen Lösungen für die Suche nach existentialquantifizierten Variablen. Im Gegensatz zu puren logischen Sprachen unterstützen sie das Lösen von Gleichungen mit funktionalen Teilausdrücken, sodass ys ++ [e]  =  [1, 2, 3] gelöst wird indem ys mit der Liste [1, 2] und e mit dem Wert 3 instantiiert wird. In Curry kann last wie folgt

last :: [a] -> a
last xs | ys ++ [e] =:= xs  =  e  where ys, e free

Hier wird das Symbol =:= für Gleichheitsbedingungen benutzt, um sie syntaktisch von definierenden Gleichheiten bzw. Zuweisungen und Vergleichen zu unterscheiden. Auf ähnliche Weise können zusätzliche Variablen gebunden indem sie explizit mit where … free deklariert werden. Die Deklaration ist notwendig und sinnvoll um Tippfehler zu vermeiden. Eine bedingte Gleichung der Form L | B  =  R kann angewendet werden, falls die Bedingung B gelöst wurde. Im Gegensatz zu rein funktionalen Sprachen, deren Bedingungen ausschließlich zu Bool ausgewertet werden, unterstützen funktionallogische Sprachen das Lösen von Bedingungen durch das Erraten von Werten der Unbekannten in der Bedingung. Einschränkungen, die im folgenden erklärt werden, werden dafür herangezogen.

Einschränkungen

Das Einschränken ist ein Mechanismus, bei dem eine Variable an einen Wert anhand von Alternativen, die von Einschränkungen auferlegt werden, gebunden wird. Alle möglichen Werte werden in einer bestimmten Reihenfolge ausprobiert, wobei der Rest des Programms aufgerufen wird, um die Korrektheit der Bindung zu überprüfen. Einschränkungen sind insofern eine Erweiterung des logischen Programmierens, dass sie eine ähnliche Suche ergeben, jedoch kann sie vielmehr Werte als Teil der Suche erzeugen als lediglich auf das Überprüfen beschränkt zu sein.

Das Einschränken ist insbesondere nützlich, da ermöglicht Funktionen wie Relationen zu handhaben; Werte können auf gewisse Art in beide Richtungen bestimmt werden. Unter anderem illustriert dies das vorhergehende Beispiel.

Wie bereits angemerkt können Einschränkungen wie eine Reduktion des Auswertegraphs aufgefasst werden und es gibt häufig viele verschiedene Wege (Strategien) einen Graphen zu reduzieren. Antoy et al. bewiesen in den Neunzigern, dass eine bestimmte Strategie, das needed narrowing, optimal ist mit möglichst wenigen Reduktionen eine Normalform zu erhalten. Needed narrowing ist eine Form von Bedarfsauswertung, im Gegensatz zur von Prolog.

Funktionale Patterns

Die Regel, mit der oben die Funktion last definiert wurde, zeigt die Tatsache, dass das eigentliche Argument das Ergebnis des Ausdrucks ys ++ [e] treffen muss. Curry kann dies auf eine sehr prägnante Art ausdrücken:

last :: [a] -> a
last (ys ++ [e])  =  e

Rein funktionale Sprachen wie Haskell erlauben eine derartige Regel nicht, da das Pattern auf der linken Seite eine definierte Funktion enthält; ein solches Pattern heißt funktionales Pattern. Funktionale Patterns werden durch die Kombination der funktionalen und logischen Eigenschaften von Curry sowie der Unterstützung von einfachen Aufgabendefinitionen, die tiefes Pattern Matching in hierarchische Strukturen erfordern.

Nicht-Determinismus

Da Curry in der Lage ist Funktionsaufrufe mit unbekannten Parametern enthaltende Gleichungen zu lösen, baut das Ausführungssystem auf nicht-deterministischen Berechnungen auf. Dieser Mechanismus ermöglicht auch die Definition von nicht-deterministischen Operationen, die mehrere verschiedene Ergebnisse zu einer gegebenen Eingabe liefern. Die Mutter der nicht-deterministischen Operationen ist der vordefinierte Infix-Operator ?, der Auswahl-Operator, der einen seiner Operanden zurückliefert. Er ist wie folgt definiert:

(?) :: a -> a -> a
x ? y  =  x
x ? y  =  y

Daher gibt die Auswertung des Ausdrucks 0 ? 1 sowohl 0 als auch 1 zurück. Das Rechnen mit nicht-deterministischen Operationen und das Rechnen mit freien Variablen unter Einschränkungen hat die gleiche Ausdrucksstärke.

Die Regeln, mit denen ? definiert wurde, zeigen ein wichtiges Merkmal von Curry: Alle Regeln werden versucht um eine bestimmte Operation auszuwerten. Daher kann man mit

insert :: a -> [a] -> [a]
insert x ys        =  x : ys
insert x (y : ys)  =  y : insert x ys

eine Operation definieren, die ein Element an eine unbestimmte Position einfügt, mit der die Operation perm, die durch

perm :: [a] -> [a]
perm []        =  []
perm (x : xs)  =  insert x (perm xs)

definiert ist, jede Permutation einer gegebenen Liste zurückgibt.

Weblinks

• Functional logic programming an der Uiversität Kiel