Participation in at least one master's seminar in the TCS group is mandatory for all master's theses.
Probabilistic Term Rewriting
In recent years interest and techniques in resource analysis of probabilistic programs have significantly increased. In the project, we study a recent approach for the automated complexity analysis of probablisitic term rewrite systems (PTRS) due to Avanzini et al., with the goal of implementing the methods in TcT. A further goal is the (potential) improvement of the theory and methods.
- On Probabilistic Term Rewriting
Martin Avanzini, Ugo Dal Lago, Akihisa Yamada
Proc. 14th International Symposium on Functional and Logic Programming, LNCS 10818, pp. 132–148, 2018 - TcT: Tyrolean Complexity Tool
Martin Avanzini, Georg Moser, Michael Schaper
Proc. 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 9636, pp. 407–423, 2016
Complexity Analysis of Lazy Programs
In contrast to the wealth of literature on the (automated) resource analysis of strict language, like OCaml, the resource analysis of non-strict languages, like Haskell, has received scarce attention. One notable exception is Okasaki, who adapted the banker's method of amortised cost analysis to the debit method, in order to correctly analyse the amortised costs of lazy data structures. In this master thesis project, we aim to study and formalse his approach. In particular we aim to adapt recent work on the fully automated amortised analysis of self-adjusting data structures such as splay trees, splay heaps, pairing heaps to lazy evaluation. The first goal is a rigorous formalisation of the Okasaki's debit method for the amortised analysis of non-strict functional programs, second the implementation of this formal methodology is envisioned as well as the application of this prototype implementation to popular lazy data structures, like lazy skew heaps. A possible further target could be lazy pairing heaps.
- Purely functional data structures Chris Okasaki, Cambridge University Press 1999, ISBN 978-0-521-66350-2, pp. I-X, 1-220
Multivariate Amortised Resource Analysis
In recent work in resource analysis the amortised analysis has received substantial interest. In this master project, we'll investigate the various approaches and in particular implement recent results on multivariate amortised analysis of term rewrite systems. Among others this will involve the automatic synthesis of tree automata, which are employed to define the potential of values over arbitrary user-defined datatypes.
- Amortised Resource Analysis and Typed Polynomial Interpretations Martin Hofmann, Georg Moser, RTA-TLCA 2015
Porting ATLAS to Haskell
ATLAS (Automated Amortised Complexity Analysis of Self-Adjusting Data Structures) provides a fully automated expected amortised cost analysis of self-adjusting data structures, that is, of randomised splay trees, randomised splay heaps, randomised meldable heaps and other sophisticated data structures (not necessarily randomised), which so far have only (semi-)manually been analysed in the literature. The current prototype is implemetned in Java and should be ported to Haskell. If possible, this re-implementation should also extend the class of resource functions considered.
- ATLAS: Automated Amortised Complexity Analysis of Self-adjusting Data Structures Lorenz Leutgeb, Georg Moser, Florian Zuleger, CAV 2021
- Automated Expected Amortised Cost Analysis of Probabilistic Data Structures Lorenz Leutgeb, Georg Moser, Florian Zuleger, CAV 2022
No entries.
Real Root Counting and Derivational Complexity of Term Rewrite Systems
We can induce polynomial upper bounds on the derivational complexity of a term rewrite system if we find a compatible matrix interpretation whose maximum matrix has spectral radius at most one. Starting from root counting algorithms of the mathematical literature, we investigate the performance of several constraints which ensure this condition is met.
Student
Philipp Wirtenberger
Supervisor
Georg Moser