A Path Order for Rewrite Systems that Compute Exponential Time Functions
Proceedings of the 22nd International Conference on Rewriting Techniques
and Applications, RTA 2011, May 30 - June 1, 2011, Novi
Sad, Serbia, volume 10 of LIPIcs, pages 123–138, (2011).
Abstract
In this paper we present a new path order for rewrite systems, the exponential path order EPO*. Suppose a term rewrite system is compatible with EPO*, 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 EPO* equals the class of functions computable in exponential time on a Turing machine.
Categories
Term Rewriting, Complexity Analysis, Path Orders, ICC, Predicative Recursion