Amortised Resource Analysis and Typed Polynomial Interpretations (extended version)

TL;DR

This paper presents a new type-based resource analysis method for typed term rewrite systems that provides polynomial bounds on runtime complexity and connects to polynomial interpretations.

Contribution

It introduces a potential-based type system for resource analysis and links well-typed systems to polynomial interpretations, extending existing theories.

Findings

Typed systems yield polynomial bounds on runtime complexity.

Well-typed rewrite systems can be oriented by polynomial interpretations.

The approach bridges resource analysis and polynomial interpretations in typed settings.

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 innermost 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 there exists a polynomial interpretation that orients R. For this we adequately adapt the standard notion of polynomial interpretations to the typed setting.