A Path Order for Rewrite Systems that Compute Exponential Time Functions

Martin Avanzini, Naohi Eguchi & Georg Moser
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.