title: A new order-theoretic characterisation of the polytime computable functions.
abstract: We propose a new order-theoretic characterisation of the class of polytime computable functions. To this avail we define thesmall polynomial path order([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 depthd, the (innermost) runtime complexity is polynomially bounded of degreed. 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.
authors.affiliation: Institute of Computer Science, University of Innsbruck, Austria.
authors.forename: Martin
authors.initials: M
authors.lastname: Avanzini
authors.affiliation: Institute of Computer Science, University of Innsbruck, Austria.
authors.forename: Naohi
authors.initials: N
authors.lastname: Eguchi
authors.affiliation: Institute of Computer Science, University of Innsbruck, Austria.
authors.forename: Georg
authors.initials: G
authors.lastname: Moser
keywords: Automation; Complexity analysis; Implicit computational complexity; Term rewriting