Normalization and Partial Evaluation of Functional Logic Programs

The functional logic programming paradigm combines the two most important fields of declarative programming, namely functional and logic programming, in an integrated way to allow the concise notation of high-level programs. However, the variety of syntactic constructs and conciseness of programs may also impact their efficiency. To reduce the syntactic complexity of functional logic languages, a typical compilation scheme incorporates a normalization phase to subsequently replace complex constructs by simpler ones until a minimal language subset is reached. The efficiency of normalized programs can then be improved by means of different optimization techniques. A very powerful optimization technique is the partial evaluation of programs. Partial evaluation basically anticipates the execution of certain program fragments at compile time and computes a semantically equivalent program, which is usually more efficient at run time. Since partial evaluation is a fully automatic optimization technique, it can also be incorporated into the normal compilation scheme of programs. In this work we consider the language Curry as a representative of the functional logic programming paradigm. We develop a formal representation of the normalization process of Curry programs into a kernel language, while respecting the interference of different language constructs. We then define the dynamic semantics of this kernel language, before we subsequently develop a partial evaluation scheme and show its correctness and termination. Due to the previously described normalization process, this scheme is then directly applicable to arbitrary Curry programs. Furthermore, the implementation of a practical partial evaluator is sketched based on the partial evaluation scheme, and its applicability and usefulness is documented by a variety of typical partial evaluation examples.

Das Paradigma der funktional-logischen Programmierung kombiniert die beiden wichtigsten Bereiche der deklarativen Programmierung, die funktionale und die logische Programmierung, um ausdrucksstarke Programme zu entwickeln. Jedoch erschweren die Vielzahl syntaktischer Konstrukte und der hohe Abstraktionsgrad auch die Übersetzung in effiziente Zielprogramme. Zur Reduktion der syntaktischen Komplexität beinhalten gängige Kompilierungsschemata eine Normalisierungsphase, in der komplexe Konstrukte schrittweise durch einfachere ersetzt werden, bis eine minimale Teilsprache erreicht wird. Die Effizienz normalisierter Programme kann dann mittels verschiedener Optimierungstechniken verbessert werden. Eine sehr mächtige Technik ist hierbei die partielle Auswertung, bei der zur Kompilierungszeit die Ausführung bestimmter Programmteile simuliert wird, um so ein semantisch äquivalentes Programm zu berechnen, das zur Laufzeit üblicherweise effizienter ausgeführt wird. Da die partielle Auswertung eine vollautomatische Optimierung darstellt, kann sie zudem in bestehende Kompilierungsschemata eingebunden werden. Diese Arbeit betrachtet die Sprache Curry als Repräsentanten für das funktional-logische Programmierparadigma. Zunächst wird eine formale Darstellung der Normalisierung von Curry-Programmen entwickelt, um die korrekte Transformation unterschiedlicher Sprachkonstrukte festzulegen. Für die resultierende Kernsprache wird dann deren dynamische Semantik definiert, um darauf aufbauend ein grundlegendes Schema zur partiellen Auswertung zu entwickeln und dessen Korrektheit und Terminierung zu zeigen. Aufgrund der Normalisierung eignet sich dieses Schema bereits zur partiellen Auswertung beliebiger Curry-Programme. Des Weiteren wird die Implementierung eines praktischen partiellen Auswerters skizziert und dessen Anwendbarkeit und Vorteilhaftigkeit anhand einiger typischer Beispiele demonstriert.

Rechte

Nutzung und Vervielfältigung:

Keine Lizenz. Es gelten die Bestimmungen des deutschen Urheberrechts (UrhG).

Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.