Relational cost analysis

Abstract

Programming languages research has made great progress towards statically estimating the execution cost of a program. However, when one is interested in how the execution costs of two programs compare to each other (i.e., relational cost analysis), the use of unary techniques does not work well in many cases. In order to support a relational cost analysis, we must ultimately support reasoning about not only the executions of a single program, but also the executions of two programs, taking into account their similarities. This dissertation makes several contributions to the understanding and development of such a relational cost analysis. It shows how: • Refinement types and effect systems can express functional and relational quantitative properties of pairs of programs, including the difference in execution costs. • Relational cost analysis can be adapted to reason about dynamic stability, a measure of the update times of incremental programs as their inputs change. • A sound and complete bidirectional type system can be developed (and implemented) for relational cost analysis.

Die Programmiersprachen-Forschung hat große Fortschritte bei der statischen Einschätzung der Ausführungskosten von Programmen gemacht.Wenn man allerdings wissen möchte, wie die Ausführungskosten zweier Programme sich zueinander verhalten (relationale Kostenanalyse), funktionieren unäre Methoden in vielen Fällen nicht gut. Eine relationale Analyse muss insbesondere nicht nur die Ausführung eines einzelnen Programmes betrachten, sondern die Ausführung beider Programme, um Ähnlichkeiten berücksichtigen zu können. Diese Dissertation liefert mehrere Beiträge zum Verständnis und zur Entwicklung solcher relationalen Kostenanalysen. Sie zeigt: • Refinement-Typsysteme und Effekt-System können funktional und relational qualitative Eigenschaften von Programmpaaren ausdrücken, insbesondere die Differenz der Ausführungskosten. • Relationale Kostenanalyse kann angepasst werden, um dynamische Stabilität zu analysieren. Diese misst die Update-Zeit inkrementeller Programme, wenn deren Eingaben sich ändern. • Ein korrektes und vollständiges bidirektionales Typsystem für die relationale Kostenanalyse kann entwickelt und implementiert werden.