Automated Complexity Analysis Based on the Dependency Pair Method

TL;DR

This paper introduces an automated method for analyzing the runtime complexity of term rewrite systems using a variant of the dependency pair technique, significantly extending previous capabilities and implemented in a dedicated tool.

Contribution

A novel automated complexity analysis method based on the dependency pair approach, enabling analysis of systems previously not automatable, with implementation and empirical evaluation.

Findings

Successfully analyzed complex rewrite systems automatically

Extended the class of systems amenable to automated analysis

Provided empirical data demonstrating method viability

Abstract

This article is concerned with automated complexity analysis of term rewrite systems. Since these systems underlie much of declarative programming, time complexity of functions defined by rewrite systems is of particular interest. Among other results, we present a variant of the dependency pair method for analysing runtime complexities of term rewrite systems automatically. The established results significantly extent previously known techniques: we give examples of rewrite systems subject to our methods that could previously not been analysed automatically. Furthermore, the techniques have been implemented in the Tyrolean Complexity Tool. We provide ample numerical data for assessing the viability of the method.