Complexity of Conditional Term Rewriting

TL;DR

This paper introduces a realistic complexity measure for oriented conditional term rewrite systems, accounting for both successful and failed computations, and provides a transformation to analyze their complexity via unconditional context-sensitive rewrite systems.

Contribution

It presents a new complexity notion for conditional term rewriting that includes failed computations and offers a transformation to analyze complexity through unconditional systems.

Findings

The complexity measure accounts for partial and failed computations.

A transformation to unconditional context-sensitive systems reflects the complexity measure.

Techniques to derive runtime and derivational complexity bounds are provided.

Abstract

We propose a notion of complexity for oriented conditional term rewrite systems satisfying certain restrictions. This notion is realistic in the sense that it measures not only successful computations, but also partial computations that result in a failed rule application. A transformation to unconditional context-sensitive rewrite systems is presented which reflects this complexity notion, as well as a technique to derive runtime and derivational complexity bounds for the result of this transformation.