Komplexitätsanalyse von Ersetzungssystemen höherer Ordnung

Wir setzen zunehmend auf Computer-Systeme, während die Komplexität solcher Systeme in den letzten Jahrzehnten stetig zugenommen hat. Durch die Begrenztheit von Rechenkapazitäten wie Platz (dh Speicher) oder Zeit ist eine Analyse des Ressourcenverbrauches ein zentrales Thema in der Software-Verifikation. Um robuste Systeme produzieren zu können, benötigen wir nach Möglichkeit vollautomatische Werkzeuge in diesem Bereich. Dieses Projekt beschäftigt sich mit der Entwicklung neuer Methoden zur automatischen Analyse der Laufzeitkomplexität von Funktionalen Programmen. Solche Verfahren sollen nützlich Schranken auf die Laufzeit (dh die Anzahl der Rechenschritte) von Programmen in Abhängigkeit von der Größe der Eingabedaten ermitteln. Um sicherzustellen, dass Ergebnisse breit anwendbar sind, verwendet man in der Regel ein abstraktes mathematisches Berechnungsmodell anstelle einer spezifischen Programmiersprache. Termersetzungssysteme sind hierfür besonders gut geeignet, auch weil die Komplexitätsanalyse von Ersetzungssystemen ein aktives Forschungsgebiet darstellt und umfassende Methoden bereits vorhanden sind. Die Schwierigkeit der getreuen Modellierung von Funktionen höherer Ordnung, welche vor allem in funktionalen Programmen wie etwa in Haskell oder OCaml sehr gebräuchlich sind, hat die Komplexitätsanalyse von funktionalen Programmen über Termersetzungssysteme weitgehend verhindert. Um diese Situation zu überwinden, stützen wir unsere Untersuchungen auf Ersetzungssysteme höherer Ordnung,eines unter den allgemeinsten mathematischen Modellenfunktionaler Sprachen. Ersetzungssysteme höherer Ordnung erweitern Termersetzungssysteme mit Operationen zur Abstraktion und Applikation. Bis heute sind fast keine Ergebnisse im Gebiet der Komplexitätsanalyse von diesen Ersetzungssystemen bekannt. Allerdings können wir Inspiration aus verwandten Forschungsbereichen, etwa das Gebiet der Programm-Analyse und der impliziten Berechenbarkeitskomplexität (ICC), beziehen. Die ICC-Gemeinschaft hat langjährige Erfahrung in der Definition von alternativen Charakterisierungen bedeutender Komplexitätsklassen, insbesondere imBezugauf spezifischer Instanzen von Ersetzungssystemen höherer Ordnung wie etwa dem Lambda-Kalkül. Unter anderem werden wir aus solchen impliziten Charakterisierungen Analysetechniken zur Laufzeitabschätzung von Ersetzungssysteme höherer Ordnung synthetisieren. Dies sollte nicht zu schwierig sein, jedoch werden die erhaltenen Techniken sehr unpräzise und wahrscheinlich nur auf sehr beschränkten Klassen von Ersetzungssystemen höherer Ordnung anwendbar sein. Damit die erhaltenen Methoden in der Praxis Anwendung finden können, müssen wir diese auf Präzision und Effektivität kalibrieren. Um die Realisierbarkeit der entwickelten Methoden zu ergründen werden wir Prototypen parallel zu den theoretischen Untersuchungen implementieren. Dies wird auch Aufschluss über die Ausdruckskraft der entworfenen Methoden geben. Abschließend werden diese Prototypen dann in TCT, einem modernen und modularenSoftwarewerkzeugzurautomatischenAnalyse des Ressourcenverbrauchesvon Termersetzungssystemen, integrieren. Unsere Ergänzungen werden TCT eine vollautomatische Analyse der Laufzeitkomplexität von funktionalen Programmen mittels Abstraktionen zu Ersetzungssystemen höherer Ordnung ermöglichen.

Wir leben in einer Welt, in der wir mehr und mehr von Computersystemen abhängig sind. Insbesondere die Komplexität unserer Softwaresysteme hat sich in den letzten Jahrzehnten drastisch erhöht. Es ist daher von größter Wichtigkeit, Softwareentwicklern eine Reihe von Werkzeugen zur Verfügung zu stellen, mit denen sich überprüfen lässt, ob der geschriebene Code bestimmten Standards entspricht, noch bevor die entwickelte Software in der Produktion verwendet wird. Ein Aspekt den man hier analysieren möchte ist die Effizienz bzw. der Ressourcenverbrauch, insbesondere die Laufzeit (d. H. die Anzahl der ausgeführten Instruktionen) in Relation zu der Größe der eingegebenen Daten. Innerhalb dieses Projekts sind wir an der Entwicklung solcher Programmanalyseverfahren interessiert. Die Analyse sollte statisch, d. h. bereits während des Entwicklungszyklus anwendbar, sein. Dies steht im Gegensatz zu herkömmlichen Profilierungs- und Überwachungstechniken. Darüber hinaus streben wir Push-Button-Technologien an, in dem Sinne, dass keine Interaktion vom Entwickler erforderlich ist. Hauptergebnisse. Im Laufe des Projektes haben wir Methoden für die automatisierte Laufzeitanalyse von funktionalen Programmen entwickelt. Wir konnten auch unser Verständnis über die Auswirkung von Evaluierungstechniken, wie etwa Sharing und Memoisierung, auf die Effizienz solcher Programme erweitern. Funktionale Programmierung ist ein aufstrebendes Programmierparadigma in dem Berechnungen als Auswertung von mathematischen Funktionen behandelt werden. Daher sind funktionale Programme prinzipiell gut für statische Verifikationstechniken geeignet. Die Natur funktionaler Programme, bei denen Funktionen im Zuge der Evaluierung erstellt und weitergegeben werden, macht unser Ziel jedoch besonders herausfordernd. Im Rahmen der automatisierten Laufzeitanalyse haben wir zwei Ansätze verfolgt. Im ersten Ansatz transformieren wir das analysierte Programm in ein äquivalentes, aber viel einfacher zu analysierendes Programm, sodass herkömmlichere Analysetechniken angewendet werden können. Im zweiten Ansatz haben wir ein feinkörniges Typsystem entwickelt welches in der Lage ist Größenbeziehungen zwischen Eingaben und Ausgaben von Funktionen auszudrücken. Durchschleifen eines Befehlszählers erlaubt dann die Laufzeitanalyse mittels diesem Typsystems. Ein bemerkenswertes Merkmal dieses Systems ist die zugrunde liegende Inferenzprozedur: geeignete Typen können vollständig von einem Computer bestimmt werden. Die im Zuge dieses Projektes entwickelten Methoden wurden ebenfalls in das Tyrolean Complexity Tool integriert, das heutzutage zu den leistungsfähigsten Werkzeugen für die Laufzeitanalyse funktionaler Programme zählt. Sachliche Informationen. Dieses Schrödinger-Stipendium startete am 27. April 2014 und wurde für 24 Monate an der Universität Bologna und für weitere 12 Monate an der Universität Innsbruck durchgeführt.