Ableitung von Programmeigenschaften aus polymorphen Typen in funktional-logischen Sprachen
Final Report Abstract
Sowohl Programmierer als auch Entwickler von Programmiersprachen und zugehörigen Implementationen benötigen Techniken, um effektiv und präzise Schlussfolgerungen über das Verhalten von Programmen zu ziehen. In bestimmtem Programmiersprachen erlaubt die Theorie relationaler Parametrizität die Herleitung von entsprechenden Aussagen allein aus (polymorphen) Typangaben. Klassisch wurde dieser Ansatz vor allem für rein funktionale Programmiersprachen verfolgt. Sogenannte funktional-logische Programmiersprachen fügen diesen Eigenschaften rein logischer Programmiersprachen hinzu, insbesondere Möglichkeiten für Berechnungen mit unvollständigen Informationen und sogar ohne Vorfestlegung auf die Rollen von Ein- und Ausgabedaten. Solche Programmiersprachen sind jedoch sowohl theoretisch (etwa zu semantischen Grundlagen) also auch pragmatisch (etwa zur Ausführungseffizienz) weniger weit erforscht. In der hier zu berichtenden Projektphase wurde eine neue Semantik für den Kern der funktionallogischen Programmiersprache Curry aufgestellt und an Hand dieser die Theorie relationaler Parametrizität vom funktionalen auf das funktional-logische Szenario übertragen. Anwendungsperspektiven ergeben sich insbesondere im Bereich der Transformation von Programmen zur Effizienzsteigerung. Bei der Implementation von rein funktionalen Programmiersprachen werden solche Methoden zur Vermeidung von kostenintensiven Berechnungen und Zwischenergebnissen bereits erfolgreich eingesetzt, wobei deren Korrektheit durch die Theorie relationaler Parametrizität garantiert werden kann. Nach unserer Übertragung dieses Ansatzes in das funktional-logische Szenario können entsprechende Transformationen nun auch für Curry-Implementationen untersucht werden.
Publications
- An Adequate, Denotationed, Functional-Style Semantics for Typed FlatCurry without Letrec. Forschungsbericht, Technical Report ISSN 0944-8535; IAI-TR-2011-1. Institut für Informatik I I I Universität Bonn Römerstraße 164 D-53117 Bonn, 2011
Jan Christiansen, Daniel Seidel, and Janis Voigtländer
