Complexity Analysis of Higher-Order Rewrite Systems

We are increasingly relying on computer systems, whereas the level of sophistication of such systems steadily increased over the last decades. To produce robust systems, we require tools which support verification in an automated setting. Limited computational resources, such as space (i.e., memory) and time, render resource analysis a central topic in software verification. We aim to advance the field of static resource analysis, by devising new methods for the automated runtime complexity analysis of functional programs. Given a program, such methods should be able to deduce useful bounds on the runtime (i.e., number of computation steps) of the provided programs, as a function of the size of the inputs. To ensure that results are broadly applicable, one usually considers an abstract model of computation instead of a specific programming language. Term rewrite systems are particularly well suited as such an abstract language, and runtime complexity analysis is a very active research area in rewriting. However, the lack of facilities to faithfully model higher-order functions has prevented the use of rewrite systems for the analysis of functional programs written in languages like Haskell or OCaml, where the use of higher-order functions is paramount. To overcome this regrettable situation, we base our studies on higher-order rewrite systems (HORSs for short), one of the most general formal models of functional programs. HORSs extend term rewrite systems to terms with abstraction and application. To date, almost no results are known on the resource analysis of HORSs. Nevertheless, we can draw inspiration from related areas of research, such as program analysis and the area of implicit computational complexity (ICC for short). Notably, the ICC community has a long history of producing characterisations of the class of polytime computable functions and related classes, based on specific instances of higher-order rewrite systems like the lambda calculus. We will seek to synthesise complexity analysis techniques for HORSs from such implicit characterisations. Although this synthesis is clearly feasible, the so obtained methods are rarely precise, and often only effective on a small class of systems. To obtain methods of practical relevance, we will have to calibrate the techniques for precision and effectiveness. To shed light on expressiveness and to demonstrate the feasibility of the established techniques, we will develop prototypical implementations along the theoretical development. Building upon the lessons learned from those prototypes, we integrate the established techniques into the Tyrolean Complexity Tool (TCT for short). TCT is a highly modular tool for the automated complexity analysis of rewrite systems. To date, it implements a majority of the state-of-the-art techniques for the analysis of first-order rewrite systems. Our additions will allow TCT to fully automatically analyse the runtime complexity of functional programs, via abstractions to HORSs.

We are living in a world where we have become more and more dependent on computer systems. In particular, the complexity of our software-systems drastically increased over the last decades. It is thus of paramount importance to provide software developers with a set of tools that allow them to verify that written code matches certain standards, even before the developed software is used in production. One aspect that one wishes to analyse here is the efficiency and resource consumption of programs, noteworthy the running time (i.e., number of executed instructions) measured in relation to the size of the programs input. Within this project, we are interested in the development of such program analysis techniques. The analysis should be static, i.e., it should be applicable already during the development cycle. This is in contrast to traditional profiling and monitoring techniques. Furthermore, we are striving at push-button technologies, in the sense that no interaction from the developer is required. Main results. During the course of the project we developed methods for the automated runtime analysis of functional programs. We could also broaden our understanding on the effect of (non)-standard evaluation semantics, such as sharing and memoization, on the efficiency of such programs. Functional programming is a rising programming paradigm that treats computation as the evaluation of mathematical functions. As such, functional programs are in principle well-suited to the kind of static verification techniques that we are aiming at. However, the very nature of functional programs, where functions are created on the fly and passed around, renders our goal a particularly challenging one. In the context of automated runtime analysis, we have followed two approaches. In the first approach we transform the analysed program to an equivalent, but much simpler to analyse program, so that more traditional analysis techniques apply. In the second approach, we have devised a fine-grained typing system that is capable of expressing size relations between inputs and outputs of functions. By threading through the computations an instruction counter, this type system is then also able to reason about the runtime of programs. A remarkable feature of this type system is its inference procedure, suitable types can be fully automatically determined by a computer. The methods developed in the course of this project have also been integrated in the Tyrolean Complexity Tool, which is nowadays among the most powerful tools for the analysis of functional programs. Factual informations. This Schrödinger fellowship started on the 27th of April, 2014. It was conducted for a period of 24 months at the University of Bologna, Italy, and included an additional return phase of 12 months at the University of Innsbruck, Austria.