Programmiersprachliche Aspekte sublinearer Platzkomplexitätsklassen
Final Report Abstract
In diesem Projekt wurden Komplexitätsklassen, die durch geringen Speicherplatz gekennzeichnet sind, maschinenunabhängig und ressourcenfrei durch Venwendung von logischen und programmiersprachlichen Konzepten charakterisiert. Neben theoretischen Einsichten über die Natur dieser Klassen ist dies bei der Entwicklung automatischer Analysen zur Abschätzung von Laufzeit und Platzverbrauch von Programmen nützlich. Eine andere Anwendung ist die Entwicklung spezifischer Optimierungen, die sich aus der komplexitätstheoretischen Analyse ergeben. Für polynomielle Rechenzeit und höhere Klassen waren solche Charakterisierungen seit längerer Zeit bekannt. In diesem Projekt wurden Charakterisierungen für logarithmischen Speicherplatz entwickelt. Die bestehenden rudimentären Ansätze wurden zu einer funktionalen Programmiersprache SBAL mit Funktionen höherer Ordnung, Polymorphie und induktiven Datentypen weiterentwickelt. Neben der Entwicklung neuer Charakterisierungen für logarithmischen Platz wurde auch die Ausdrucksstärke des für diese Klasse typischen Ansatzes der zeigerbasierten Programmierung untersucht. Dazu wurde eine geeignete Programmiersprache PURPLE entwickelt. Hauptergebnis des Projekts war die Entwicklung und eingehende Untersuchung dieser Formalismen SBAL und PURPLE, welche im Folgenden kurz beschrieben werden. SBAL. Ein erfolgreicher Ansatz zur Charakterisierung von Komplexitätsklassen besteht darin, das Typsystem des polymorphen A-KalkOls mithilfe Girards linearer Logik so einzuschränken, dass nur die Funktionen in einer bestimmten Komplexitätsklasse zugelassen sind. Mit Stratified Bounded Affine Logic (SBAL) haben wir die erste Logik dieser Art definiert, mit der sich die in logarithmischem Platz berechenbaren Funktionen erfassen lassen. Interessant ist, dass in SBAL nicht nur, wie in einschlägigen Arbeiten üblich, die Kopiermodalität „T der linearen Logik eingeschränkt ist, sondern auch der Allquantor V. Die für den Korrektheitsbeweis von SBAL benötigten Methoden wurden ebenfalls im Laufe dieses Projekts entwickelt. PURPLE. PURPLE (PURe Pointer LanguagE) ist eine imperative Programmiersprache für Algorithmen auf verzeigerten Datenstrukturen wie Graphen, Bäumen oder Objekthierarchien. Im Gegensatz zur Turingmaschine greift ein PURPLE Programm auf die Eingabestruktur über abstrakte Befehle zu, wie Verfolgen eines Zeigers oder Testen zweier Zeiger auf Gleichheit. Der lokale Zustand eines Programms umfasst eine konstante Zahl von Booleschen Variablen und Zeigervariablen. Die Kontrollstrukturen sind Schleifen, Fallunterscheidungen, sowie eine forall-Schleife, die ihrem Rumpf alle Objekte der Eingabestruktur in einer unspezifizierten Reihenfolge anbietet. Diese forall-Schleife ist die entscheidende Innovation; wiewohl ihre Funktionalität in Laufzeitbibliotheken und Datenbanksprachen zur Verfügung steht, wurde sie in theoretischen Formalismen noch nicht studiert. Es zeigte sich, dass PURPLE Programme in logarithmischem Platz auf einer Turingmaschine ausgewertet werden können und viele, aber nicht alle, Algorithmen, die logarithmischen Platz benötigen, auch in natürilcher Weise in PURPLE dargstellt werden können. Beispiele für Algorithmen, für die das nicht möglich ist, sind solche, die explizit Boolesche Arrays logarithmischer Größe benötigen. Hierzu gehört Reingolds Algorithmus für Erreichbarkeit in ungerichteten Graphen und wir zeigen auch, dass diese Aufgabenstellung durch keinen wie auch immer gearteten anderen Algorithmus in PURPLE gelöst werden kann. Dieses Resuftat beantwortet eine bisher offene Frage über die Ausdrucksstärke einer bestimmten Logik (DTC-Logik auf lokal geordneten Graphen), da Formeln in dieser Logik mithilfe von PURPLE Programmen ausgewertet werden können.
Publications
- Space-Efficient Computation by Interaction - A Type System for Logarithmic Space. In Computer Science Logic 2006 (CSL06), S. 606-621, Springer LNCS 4207, 2006
U. Schöpp
- Stratified Bounded Affine Logic for Logarithmic Space. In Logic in Computer Science 2007 (LICS07), S 411-420, 2007
U. Schöpp
- A Formalised Lower Bound on Undirected Graph Reachability. In Logic for Programming, Artificial Intelligence and Reasoning 2008 (LPAR08), S. 621-635, Springer UNAI 5330. 2008
U. Schöpp
- A Semantic Proof of Polytime Soundness of Light Affine Logic. In Computer Science Symposium in Russia 2008 (CSR081 S. 134-145, Springer LNCS 5010, 2008
U. Dal Lago und M. Hofmann
- Pointer Programs and Undirected Reachability. ECCO Technical Report TR08-090, 2008
U. Schöpp und M. Hofmann
- Pure Pointer Programs with Iteration. In Computer Science Logic 2008 (CSL08), S. 79-93, Springer LNCS 5213, 2008
M. Hofmann und U. Schöpp
