Automated complexity analysis of term rewrite systems
Martin Avanzini (Inria)
Find the material for this lecture here.
Over the last two decades, the rewriting community has introduced various techniques for the automated complexity analysis of term rewrite systems. Early research on complexity analysis mainly concentrated on assessing the strength of termination techniques. A proof of termination certifies not only that reductions are finite, but e.g. via proof-theoretical observations, a concrete bound on maximal derivation lengths can be obtained. In this spirit, the higher this bound, the better! The community then realised that by suitably restricting existing termination techniques, informative bounds can be obtained. Moreover, as the automation of termination analysis had already been extensively explored at that time, various tools emerged relatively early that could fully automatically assess the runtime of term rewrite systems, expressed as the function that relates term sizes to maximal length of reductions. This marks the birth of automated complexity analysis in rewriting.
Although rooted in termination analysis, automated complexity analysis has become nowadays a topic pursued independently. In particular, with the advent of combination frameworks for complexity analysis and dedicated complexity techniques, automated tools matured so that interesting examples can be handled fully automatically. Moreover, these tools nowadays act also as backends in the analysis of imperative, logical and functional programs, via suitable program abstractions. To date, the automated complexity analysis of real-world programs via rewriting tools is among the most competitive approaches.
This lecture will give a modern account on the state-of-the-art in complexity analysis, covering most frequently used analysis techniques, their automation and applications to real-world programs.
Outline of the lecture
This tentative outline ranges over two lecture slots, each 90 minutes. Lectures are taught in a mixture of frontal teaching and interaction with students.
In this lecture, basic concepts and main techniques for reasoning about the complexity of term rewrite systems are introduced. The lecture is divided into two parts.
- From Termination to Derivational Complexity Analysis. After introducing basic notions, we will look at some well-known termination techniques and what they tell us about the derivational complexity of the analysed system [10, 9, 14, 6], as well as draw connections to recursion theory. We will then look at restricted forms of termination techniques so that feasible bounds can be established .
- Rewriting as a Computational Model and Runtime Complexity. In this second half, we look at rewrite system as a model of functional/declarative programming and its corresponding notion of runtime complexity. We will revisit the techniques from the first half of this lecture, and see miniaturisations that can polynomial bind the runtime complexity of compatible rewrite systems [5, 12, 3, 13]. Finally, we look at variations of dependency pairs suitable for runtime analysis, e.g. dependency tuples .
Having introduced the fundamental techniques for analysis the complexity of rewrite systems in the first lecture, we turn in this lecture our attention to automation and applications. This lecture also involves hands-on experience with existing tools.
- From Theory to Automation. In this first half of the lecture we look at existing complexity analysis tools and how they operate. State-of-the-art tools such as TCT  and AProVE  combination a variety of methods, from adaptions of dependency pair techniques to various term orderings, simplification and decomposition techniques. We look at a particular instance of such a framework that enables this combination , as well as novel techniques developed under this setting which greatly improve upon the modularity of the overall analysis and which are key towards strong automated tools.
- Applications to Program Analysis. Automated tools for the runtime complexity analysis have been successfully employed to analyse imperative , logical  and functional programs . The final half of this lecture starts with an overview of these approaches. The main part of this second half consists then of a case study on a pure fragment of OCaml , illustrating advantages but also limitations in comparison to dedicated tools such as Resource Aware ML .
The students are supposed to know the basics of first-order term rewriting. Basic knowledge of termination techniques will be helpful, but is not required. Apart from basic notions such as asymptotic complexity, no special knowledge of complexity theory is assumed.
- M. Avanzini, U. Dal Lago, and G. Moser. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Proc. of 20th ICFP, pages 152–164, New York, NY, 2015. ACM.
- M. Avanzini and G. Moser. A Combination Framework for Complexity. IC, 2013. Submitted.
- M. Avanzini and G. Moser. Polynomial Path Orders. LMCS, 9(4), 2013.
- M. Avanzini, G. Moser, and M. Schaper. TcT: Tyrolean Complexity Tool. In Proc.of 2nd TACAS, LNCS, pages 407–423, Heidelberg, DE, 2016. Springer.
- G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with Polynomial Interpretation Termination Proof. JFP, 11(1):33–53, 2001.
- E. A. Cichon and A. Weiermann. Term Rewriting Theory for the Primitive Recursive Functions. APAL, 83(3):199–223, 1997.
- F. Frohn and J. Giesl. Complexity Analysis for Java with AProVE. In Proc. of 13th IFM, volume 10510 of LNCS, pages 85–101. Springer, 2017.
- J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs. Symbolic Evaluation Graphs and Term Rewriting: A General Methodology for Analyzing Logic Programs. In Proc. of 14th PPDP, pages 1–12. ACM, 2012.
- D. Hofbauer. Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths. TCS, 105(1):129–140, 1992.
- D. Hofbauer and C. Lautemann. Termination Proofs and the Length of Derivations. In Proc. of 3rd RTA, volume 355 of LNCS, pages 167–177. Springer, 1989.
- J. Hoffmann, K. Aehlig, and M. Hofmann. Resource Aware ML. In Proc. of 24th CAV, volume 7358 of LNCS, pages 781–786, Heidelberg, DE, 2012. Springer.
- J.-Y. Marion. Analysing the Implicit Complexity of Programs. IC, 183:2–18, 2003.
- A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. Zankl. Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems. In Proc. of 4th CAI, volume 6742 of LNCS, pages 1–20. Springer, 2011.
- G. Moser and A. Schnabl. Proving Quadratic Derivational Complexities using Context Dependent Interpretations. In Proc. of 19th RTA, volume 5117 of LNCS, pages 276–290. Springer, 2008.
- L. Noschinski, F. Emmes, and J. Giesl. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. JAR, 51(1):27–56, 2013.
- H. Zankl and M. Korp. Modular Complexity Analysis for Term Rewriting. LMCS, 10(1:19):1–33, 2014.