Observational Correctness of Programming Languages Translations

• Applicant: Professor Dr. David Sabel
• Subject Area: Theoretical Computer Science ; Software Engineering and Programming Languages
• Term: from 2015 to 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 289510568

• Final Report Year: 2020

Final Report Abstract

Das Projekt behandelte die Korrektheit von Übersetzungen und Transformationen von Programmiersprachen. Hierbei wurden syntaktisch umfangreiche Metasprachen zur Darstellung der Programmiersprachenmodelle entworfen und ein Werkzeug entwickelt, welches den Korrektheitsnachweis für Transformationen mithilfe syntaktischer Methoden (Unifikation, Matching und Rewriting) automatisiert nachweisen kann. Als wichtige Neuerung wurden hierbei sogenannte Non-Capture-Constraints als Repräsentationsmittel eingeführt. Diese bestehen aus Paaren von Metaausdrücken und Metakontexten. Sie können die Menge der repräsentierten Programme einschränken, da sie nur für jene Instanziierungen erfüllt sind, für die gilt: Der Kontext fängt keine Variablen des Ausdrucks ein, wenn der Ausdruck in den Kontext eingesetzt wird. Mit diesen Non-Capture-Constraints können viele gebräuchliche Nebenbedingungen für Transformationen und Übersetzungen leicht dargestellt werden. Die benötigten Unifikations- und Matchingverfahren wurden entwickelt, als korrekt und vollständig nachgewiesen und bezüglich ihrer Komplexität analysiert. Die zugehörigen Entscheidungsprobleme wurden als Letrec-Unifikationsproblem und -Matchingproblem formuliert und deren NP-vollständig konnte jeweils nachgewiesen werden. Da die konsistente Umbenennung von gebundenen Variablen mit frischen Variablen dabei benötigt wurde, wurden auch hierzu Methoden entwickelt, um diese auf der Metasprache symbolisch zu repräsentieren und durchzuführen. Damit war es u.a. möglich für eine Kernsprache von Haskell einer größere Menge von Programmtransformationen automatisch als korrekt nachweisen zu lassen. Mit dem Ziel der Automatisierung weiterer solcher Beweise wurde auch der Stand der Technik zur sogenannten nominalen Unifikation erweitert, so dass diese Terme mit Atomvariablen und mit Metasymbolen für Kontexte (mit linearem Vorkommen) behandeln kann. Dabei wurden sogenannte Distinct-Variable-Constraints in die Inferenzprozedur aufgenommen, welche die Menge von erlaubten Ausdrücken auf solche einschränken, deren Variablennamen einer gewissen Variablenkonvention unterliegen: Gebundene und freie Variablen sind verschieden und gebundene Variablen sind untereinander ebenfalls verschieden. Für das Unifikationsproblem mit nominalen Termen und Atomvariablen konnte dessen NP-Vollständigkeit nachgewiesen werden. Für das um Kontextvariablen erweiterte Problem könnte ein Algorithmus angegeben werden, der ohne Erfüllbarkeitsprüfung der Distinct-Variable-Constraints nichtdeterministische Polynomialzeit benötigt. Für die Erfüllbarkeitsprüfung wurde ein in nichtdeterministischer Exponentialzeit arbeitender Algorithmus angegeben. Neben der automatischen Widerlegung von Übersetzungen und einem entsprechenden Werkzeug dazu, wurden im Projekt mehrere korrekte Übersetzungen zur Einbettung des π-Kalküls in die Programmiersprache Concurrent Haskell entworfen und als korrekt nachgewiesen. Schließlich trug das Projekt (auch mithilfe korrekter Übersetzungen) dazu bei, Verbesserungseigenschaften von Programmtransformationen für funktionale Programmiersprachen nachzuweisen und neue korrekte und vollständige Verfahren zum Terminierungsnachweis sogenannter Kreisersetzungssysteme zu entwerfen.

Publications

• Unification of program expressions with recursive bindings. In Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP ’16, pp. 160–173, 2016. ACM
  M. Schmidt-Schauß and D. Sabel
  
• Alpha-renaming of higher-order meta-expressions. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, PPDP ’17, pp. 151–162, 2017. ACM
  D. Sabel
  
• Termination of cycle rewriting by transformation and matrix interpretation. Logical Methods in Computer Science, Volume 13, Issue 1, 2017
  D. Sabel and H. Zantema
  
• Nominal unification with atom and context variables. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, volume 108 of LIPIcs, pp. 28:1–28:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018
  M. Schmidt-Schauß and D. Sabel
  
• Sequential and parallel improvements in a concurrent functional programming language. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP ’18, pp. 20:1–20:13, 2018. ACM
  M. Schmidt-Schauß, D. Sabel, and N. Dallmeyer
  
• Nominal unification with atom-variables. J. Symb. Comput., 90:42–64
  M. Schmidt-Schauß, D. Sabel, and Y. D. K. Kutz