Derivational Complexity Analysis

Term rewriting is a conceptual simple, but powerful abstract model of computation that underlies much of declarative programming. In this project proposal we are interested in the -- general undecidable -- termination problem in term rewriting and the complexity of rewrite systems measured by the maximal length of derivations, i.e., rewrite steps. In the area of term rewriting powerful methods have been introduced to establish termination of a given term rewrite system. Earlier research mainly concentrated on inventing suitable reduction orders capable of proving termination directly. In recent years the emphasis shifted towards transformation techniques like the dependency pair method or semantic labelling. These techniques can be used to prove termination of a given rewrite system automatically. 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 a rewrite system of interest. Another interesting property is the complexity of the term rewriting 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 will develop in these three parts provide computable and precise bounds. Thus guaranteeing that we can establish instructive upper bounds automatically. We will incorporate them into the Tyrolean Termination Tool, a termination prover which is developed in our research group. This will make the Tyrolean Termination Tool more expressive by rendering the user not only information about the termination behaviour of the analysed term rewrite system, but also about its derivational complexity.

Term rewriting is a conceptual simple, but powerful abstract model of computation that underlies much of declarative programming. In this project proposal we are interested in the - general undecidable - termination problem in term rewriting and the complexity of rewrite systems measured by the maximal length of derivations, i.e., rewrite steps. In the area of term rewriting powerful methods have been introduced to establish termination of a given term rewrite system. Earlier research mainly concentrated on inventing suitable reduction orders capable of proving termination directly. In recent years the emphasis shifted towards transformation techniques like the dependency pair method or semantic labelling. These techniques can be used to prove termination of a given rewrite system automatically. 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 a rewrite system of interest. Another interesting property is the complexity of the term rewriting 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 will develop in these three parts provide computable and precise bounds. Thus guaranteeing that we can establish instructive upper bounds automatically. We will incorporate them into the Tyrolean Termination Tool, a termination prover which is developed in our research group. This will make the Tyrolean Termination Tool more expressive by rendering the user not only information about the termination behaviour of the analysed term rewrite system, but also about its derivational complexity.