Derivational Complexity Analysis

In the area of term rewriting powerful methods have been introduced to establish termination of a given term rewrite system. Modern termination provers can often establish termination or nontermination of the input rewrite system in a couple of seconds. However, termination of a rewrite system is only one property of interest. Another interesting property is the complexity of the rewrite system. Here complexity is measured as the maximal length of derivations. This notion of complexity is usually called derivational complexity in the literature. The goal of this project is to make derivational complexity analysis

  • modern by studying the derivational complexities induced by modern termination techniques,
  • useful by establishing refinements of existing termination techniques guaranteeing that the induced derivational complexity is bounded by a function of low computational complexity, for example a polytime computable function,
  • broad by analysing the derivational complexities of higher-order rewrite systems and for rewrite systems based on particular rewrite strategies.

Further we want to ensure that the results that we develop in these three parts provide computable and precise bounds. Thus guaranteeing that we can establish instructive upper bounds automatically. We have incorporated obtained results into a complexity analyser: the Tyrolean Complexity Tool (TCT for short). TCT is open source and and licensed under the GNU Lesser General Public License.

  • Martin Avanzini
  • Georg Moser
  • Andreas Schnabl
FWF project number



Nach oben scrollen