Avanzini Martin, Eguchi Naohi, Moser Georg
Institute of Computer Science, University of Innsbruck, Austria.
Theor Comput Sci. 2015 Jun 20;585:3-24. doi: 10.1016/j.tcs.2015.03.003.
We propose a new order-theoretic characterisation of the class of polytime computable functions. To this avail we define the ([Formula: see text] for short). This termination order entails a new syntactic method to analyse the innermost runtime complexity of term rewrite systems fully automatically: for any rewrite system compatible with [Formula: see text] that employs recursion up to depth , the (innermost) runtime complexity is polynomially bounded of degree . This bound is tight. Thus we obtain a direct correspondence between a syntactic (and easily verifiable) condition of a program and the asymptotic worst-case complexity of the program.
我们提出了一种关于多项式时间可计算函数类的新的序理论特征描述。为此,我们定义了(简称为[公式:见正文])。这种终止序带来了一种全新的句法方法,可完全自动地分析项重写系统的最内层运行时复杂度:对于任何与[公式:见正文]兼容且使用深度达的递归的重写系统,(最内层)运行时复杂度在多项式上有界,次数为。这个界是紧密的。因此,我们在程序的一个句法(且易于验证)条件与程序的渐近最坏情况复杂度之间建立了直接对应关系。