Amortised Resource Analysis and Typed Polynomial Interpretations

ABSTRACT. We introduce a novel resource analysis for typed term rewrite systems based on a potential-based type system. This type system gives rise to polynomial bounds on the runtime complexity. We relate the thus obtained amortised resource analysis to polynomial interpretations and obtain the perhaps surprising result that whenever a rewrite system R can be well-typed, then their exists a polynomial interpretation that orients R. For this we suitable adapt the standard notion of polynomial interpretations to the typed setting.