Logische und Funktionale Programmierung

Der Prädikatenlogik kommt in vielen Bereichen der Informatik eine zentrale Rolle zu. Im Zusammenhang mit Programmierung wurde Logik seit jeher zur Spezifikation und zum Beweis der Korrektheit von Programmen eingesetzt. Im Bereich der Künstlichen Intelligenz existieren seit den Arbeiten an automatischen Theorembeweisern Ansätze, den Vorgang des Programmierens zu automatisieren. Solche Arbeiten zur Programmsynthese starten zumeist von einer gegebenen Spezifikation eines Programmes in Prädikatenlogik erster Stufe. Die Aufgabe ist dann, daraus ein lauffähiges, effizientes Programm zu konstruieren, wozu in manchen Systemen auch Interaktion mit dem Benutzer zugelassen ist. Insofern ist offensichtlich Programmsynthese aus logischen Spezifikationen als logisches Programmieren aufzufassen; die Arbeiten auf diesem Gebiet werden auch unter diesem Anspruch in vielen aktuellen Forschungsprojekten betrieben.

In der Einführung wurde bereits deutlich gemacht, daß Programmieren in Logik nicht notwendigerweise mit Programmieren in Hornklausellogik gleichzusetzen ist. Im folgenden soll verdeutlicht werden, daß Programmieren in Hornklausellogik auch nicht notwendigerweise Programmieren in PROLOG bedeutet.

Die Diskussion über eine Charakterisierung von funktionalen Sprachen wird in verschiedenen Kontexten geführt. Sind z.B. real existierende LISP-Versionen funktionale Sprachen, wo doch hier durchaus imperative Konstrukte, wie SETQ vorhanden sind? Von einem puristischen Standpunkt aus gesehen, ist ein solches LISP-System prozedural, lediglich der Kern, also “pure”-LISP, kann als funktional, oder vielleicht besser als applikativ bezeichnet werden.

Eine Instantiierung des soeben eingeführten FHCL-Systems soll ausführlich vorgestellt und diskutiert werden. Dieses Programmiersystem ist bezüglich der Designentscheidungen sehr stark an LOGLISP [RS82] orientiert. In der Einleitung wurden bereits ausführlich die Vorteile der Verwendung von LISP als funktionalen Teil besprochen; im folgenden sei noch einmal auf einige Punkte hingewiesen:

In der Beschreibung des Deduktionszyklus von FHCL im vorigen Abschnitt wurde bereits erwähnt, daß durch die Verwendung der Hornklausellogik im kombinierten System FHCL zu erwarten ist, daß im Suchbaum des HCL-Interpreters viele ODER-Verzweigungen vorkommen. Der Aufbau des FHCL-Systems wurde derart vorgenommen, daß ein breadth-first-Durchlaufen des Suchbaumes unterstützt wird. Wichtig war auch, daß der “random-Modus”, in dem der Suchbaum auf nichtdeterministische Weise durchlaufen wird, ermöglicht wird.

An verschiedenen Stellen wurde bereits darauf hingewiesen, daß Termersetzungssysteme als ein wichtiges Paradigma der funktionalen Programmierung die funktionale Komponente einer Instantiierung des FHCL-Schemas bilden können.

Für die Einführung von Sorten in eine logische Programmiersprache können verschiedenartige Gründe genannt werden:

In diesem Abschnitt soll die Lösung einer anspruchsvolleren Programmieraufgabe in FHCL skizziert werden. Dabei soll jedoch nicht nur ein Programmierbeispiel besprochen werden, vielmehr steht das Aufzeigen einer weiteren Verwendungsmöglichkeit von kombinierten logischen und funktionalen Programmiersprachen im Vordergrund. Es zeigt sich nämlich, daß die systematische transformationeile Herleitung von Programmen aus ihrer Spezifikation durch FHCL auf natürliche Weise unterstützt werden kann.

Im Mittelpunkt dieses Buches steht die Kombination von funktionalen Programmiersprachen mit einem Hornklauselkalkül.

In diesem Anhang sind die vollständigen FHCL-Programme für die einzelnen Versionen von Smoothsort aus Abschnitt 7 angegeben.