A Path Order for Rewrite Systems that Compute Exponential Time Functions (Technical Report)

TL;DR

This paper introduces the exponential path order EPOSTAR, a new method to analyze rewrite systems, establishing a correspondence with exponential time computable functions and providing a tool for complexity analysis.

Contribution

The paper presents EPOSTAR, a novel path order that characterizes exponential time computable functions via rewrite systems, bridging rewriting and complexity theory.

Findings

Rewrite systems compatible with EPOSTAR have exponential runtime bounds.

EPOSTAR characterizes exactly the class of exponential time computable functions.

The method provides a new tool for analyzing the complexity of rewrite systems.

Abstract

In this paper we present a new path order for rewrite systems, the exponential path order EPOSTAR. Suppose a term rewrite system is compatible with EPOSTAR, then the runtime complexity of this rewrite system is bounded from above by an exponential function. Furthermore, the class of function computed by a rewrite system compatible with EPOSTAR equals the class of functions computable in exponential time on a Turing maschine.