Einleitung

Die funktional-logische Programmierung führt die Vorteile der funktionalen und der logischen Programmierung in einem gemeinsamen Konzept zusammen. Beide Sprachkonzepte sind deklarativ, d.h. ein Programm enthält keine algorithmische Beschreibung des Lösungsweges wie in prozeduralen Sprachen sondern eine Beschreibung des Problemes: funktionale oder kausale Abhängigkeiten werden in einer mathematischen Notation formuliert, und die Semantik eines Programmes kann über diese Notation leichter definiert werden als dies bei prozeduralen Programmen der Fall ist. Dies erleichtert nicht nur die Programmierung selbst, sondern ermöglicht auch die Überprüfung der Korrektheit. In ihren reinen Formen sind diese Sprachen frei von Nebeneffekten, die das Verhalten eines Programmes unübersichtlich machen.

Funktionale Programmiersprachen wie Miranda, Haskell, Gofer, LISP, Scheme oder ML erlauben die Definition von Funktionen höherer Ordnung und basieren auf Termersetzungssystemen zur Reduktion funktionaler Ausdrücke. Durch verzögernde Auswertungsstrategien sind unendliche Datenstrukturen möglich, welche immer nur soweit ausgewertet werden, wie dies erforderlich ist. Die Konzepte der Abstraktion und Applikation des $\l$-Kalküls werden unterstützt, Pattern Matching als Alternative zur Verwendung von Test- und Selektionsoperatoren erlaubt eine vereinfachte Darstellung funktionaler Programme. Funktionen können auch rekursiv definiert werden, so daß alle $\mu$-rekursiven Funktionen und damit alle Turing-berechenbaren Funktionen durch funktionale Programme berechenbar sind.

Logische Programmiersprachen wie Prolog verwenden Klauseln mit logischen Prädikaten und basieren auf Unifikation und dem Resolutionsprinzip von Robinson. Die mathematische Grundlage dieser Programmiersprachen ist die Prädikatenlogik erster Stufe, für die es einen Resolutionsalgorithmus gibt, der die Entscheidbarkeit der Unifikation erster Ordnung ausnutzt. Erweiterungen auf Prädikatenlogik höherer Stufen erfordern auch Unifikation höherer Ordnung, die im allgemeinen unentscheidbar ist. Die Abwesenheit von Funktionsdefinitionen erschwert eine deterministische Auswertung, da die Suche nach Lösungen für eine Anfrage nicht-deterministisch erfolgt.

In der funktional-logischen Programmierung werden diese Konzepte nun zusammengeführt. Operationale Grundlage ist hier das Narrowing, eine Übersicht gibt [Hanus94JLP], [Pre95] vergleicht eine Reihe von Narrowing-Verfahren und präsentiert verschiedene Anwendungen. Beispiele funktional-logischer Programmiersprachen sind ALF [HanusSchwab91Impl], BABEL [MorenoRodriguez92], K-LEAF [BoscoEtAl87] und SLOG [Fribourg85]. Die jüngste Entwicklung in diesem Bereich ist die Programmiersprache Curry [HanusKuchenMoreno-Navarro95ILPS], [Hanus:Curry-Report], deren Narrowing-Strategie mit definierenden Bäumen [Antoy92ALP, AntoyEchahedHanus94POPL, HanPre96] arbeitet. Diese Sprache wurde mittlerweile auch in einer Vorlesung über Deklarative Programmiersprachen an der RWTH Aachen eingesetzt -- ein Konzept zur gleichzeitigen Einführung in die funktionale und Logikprogrammierung mit Hilfe von Curry enthält [Hanus97DPLE].

Nach jedem Narrowing-Schritt erfolgt eine implizite $\beta\eta$-Reduktion des Terms im $\l$-Kalkül: so wird etwa $(\l x.s) t$ zu $\{ x \mapsto t \} s$, und die Substitution $\{ x \mapsto t \}$ erfolgt implizit. Dadurch sind die $\beta$- und $\eta$-Regeln des $\l$-Kalküls keine Termersetzungsregeln erster Ordnung. $\l$-Kalküle mit \emph{expliziten Substitutionen} ersetzen die klassischen $\beta$- und $\eta$-Regeln durch neue Regeln, so daß Terme der Form $t[s]$ entstehen, wobei die eckigen Klammern und $s$ syntaktische Objekte sind. Es werden dann Termersetzungsregeln erster Ordnung eingeführt, mit denen die Substitution bewerkstelligt wird. Dadurch wird ein $\beta$- oder $\eta$-Reduktionsschritt zu einer Folge von Reduktionsschritten, an deren Ende wieder ein \emph{reiner} Term steht, d.h. ein Term ohne Substitutionsanteil $[s]$. Zwei dieser Kalküle sind $\l\sigma$ [ACCL91,DHK95] und $\l\upsilon$ [Lescanne94, BBLRD95]. Eine Einführung und Übersicht über verschiedene $\l$-Kalküle mit expliziten Substitutionen gibt [Rose96] -- dieses Papier enthält auch eine sehr ausführliche, teilweise kommentierte Bibliographie.

Aufgabe der vorliegenden Diplomarbeit ist es, einen dieser Kalküle mit expliziten Substitutionen auf das Narrowing-Verfahren LNT [HanPre96] anzuwenden, um so durch das Ersetzen der impliziten Substitutionen die Grundlage für eine effiziente Implementierung zu schaffen. Wir stellen das Narrowing-Verfahren LNT$\l\upsilon$ vor, welches eine modifizierte Version des $\l\upsilon$-Kalküls verwendet und dabei äquivalent zu LNT bleibt.

Die Arbeit gliedert sich wie folgt: In Kapitel 2 geben wir die grundlegenden Definitionen des (einfach getypten) $\l$-Kalküls. Wir betrachten Unifikationsprobleme höherer Ordnung und erklären Narrowing-Verfahren. Kapitel 3 führt in das Narrowing-Verfahren LNT ein, das in dieser Arbeit weiterentwickelt wird. Kapitel 4 stellt $\l$-Kalküle mit expliziten Substitutionen vor: Wir betrachten die $\l\sigma$- und $\l\upsilon$-Kalküle, in denen $\beta$-Reduktion internalisiert, d.h. zu einer Reduktionsregel auf der syntaktischen Ebene gemacht wird, und geben für letzteren eine Ergänzung um eine explizite $\eta$-Regel an. In Kapitel 5 kombinieren wir das LNT-Verfahren mit dem $\l\upsilon$-Kalkül und weisen die Äquivalenz des neuen Verfahrens zu LNT nach. Kapitel 6 schließt die Arbeit mit einer Zusammenfassung und einem Ausblick ab.