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 und Unifikation. Wegbereiter dieser Schöpfung war λProlog in den Neunzigern. Andere, neuere funktionallogische Programmiersprachen sind Curry und Mercury.

Grundlagen

Die Beispiele sind in der Syntax von Curry.

Funktionale Programmierung

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. Einen Teilausdruck, der reduziert werden kann, wird auch als Redex (von englisch reducible expression ‚reduzierbarer Ausdruck‘) bezeichnet. Für die nächsten Beispiele sei die Funktion verdoppeln definiert durch

verdoppeln x  =  x + x

Der Ausdruck verdoppeln 1 ist ein Redex und wird durch 1 + 1 ersetzt, was wiederum durch 2 ersetzt werden kann, wobei man den +-Operator vereinfacht als eine unendliche Menge von Gleichungen der Form 1 + 1 = 2, 1 + 2 = 3 usw. auffasst. 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)  →  verdoppeln 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 (z. B. aufgrund von Seiteneffekten) von der Reihenfolge oder dem Zeitpunkt der Auswertung ab. Daher sind Beweise leichter zu führen und die Programme leicht wartbar.

Algebraische Datentypen

Ebenso wie funktionale Sprachen unterstützen viele funktionallogische Sprachen 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 Mustervergleich (Pattern Matching) definiert werden, meistens 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. Variablen für Listen enden oft mit S, vgl. die Pluralbildung in der englischen Sprache.

(++) :: [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

Logische Programmierung

Es sei zur Demonstration die Funktion last beschrieben, die das letzte Element einer nicht-leeren Liste zurückgibt. Für alle Listen xs und Elemente e gilt: last xs ergibt e genau dann, wenn ys ++ [e] gleich xs für eine geeignete Liste ys.

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 rein 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. Dann kann last wie folgt definiert werden:

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 und Vergleichen zu unterscheiden. Auf ähnliche Weise können zusätzliche Variablen gebunden werden, 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 Muster oder Ausdrücke vom Typ Bool sein können, unterstützen funktionallogische Sprachen außerdem das Lösen von Bedingungen durch das Erraten von Werten der Unbekannten in der Bedingung; Muster-Bedingungen sind ein Spezialfall davon. 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 es 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 SLD-Auflösungsstrategie von Prolog.

Funktionale Muster

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, wobei für ys und e beliebige Werte eingesetzt werden dürfen. Da auf einer Seite nur ein Parameter vorkommt, kann man das alternativ auch auf eine sehr prägnante Art ausdrücken:

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

Rein funktionale Sprachen erlauben eine derartige Definition nicht, da das Muster auf der linken Seite eine definierte Funktion enthält (nämlich den Operator ++), die nicht notwendig injektiv ist; ein solches Muster heißt funktionales Muster. Funktionale Muster werden durch die Kombination der funktionalen und logischen Eigenschaften sowie der Unterstützung von einfachen Aufgabendefinitionen, die tiefe Mustervergleiche in hierarchische Strukturen erfordern. In diesem Beispiel ist ++ allgemein nicht injektiv, denn jede nicht-leere Liste kann mit [] ++ l als auch l ++ [] erzeugt werden; jedoch können die freien Variablen hier nur auf eine mögliche Art gewählt werden, da sie Einschränkungen unterliegen.

Nichtdeterminismus

Da funktionallogische Sprachen in der Lage sind, Funktionsaufrufe mit unbekannten Parametern enthaltende Gleichungen zu lösen, baut das Ausführungssystem auf nichtdeterministischen 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 nichtdeterministischen Operationen ist der vordefinierte Infix-Operator ?, der Auswahl-Operator, der nichtdeterministisch einen seiner Operanden zurückliefert.

(?) :: 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 nichtdeterministischen 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 funktionallogischer Sprachen: Alle Regeln werden versucht um eine bestimmte Operation auszuwerten; insbesondere wird nicht die oberste realisierbare Gleichung angewendet. 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. In funktionalen Sprachen wäre die zweite Gleichung unerreichbar, weil die erste alle möglichen Parameter annehmen kann. Werden die Gleichungen vertauscht, würde die zweite Gleichung nur für leere Listen verwendet, weil die erste alle nichtleeren Listen angewendet wird. In der funktionallogischen Programmierung kann daher das Prinzip, schon in oberen Gleichungen behandelte Fälle nicht mehr zu beachten, nicht verwendet werden; in diesem Sinne muss jede Gleichung so betrachtet werden, als wäre sie die oberste.

Mit insert wird die Funktion perm durch

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

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

Weblinks

• Functional logic programming an der Universität Kiel