Amortized resource analysis for term rewrite systems

Based on earlier work on amortised resource analysis, we establish two novel automated amortised resource analyses for term rewrite systems. On one hand the worst-case analysis gives rise to polynomial bounds on the innermost runtime complexity of the analysed term rewrite system while on the other hand we present a best-case analysis for term rewrite systems. Both methods are presented in an inference system akin to a type system and build upon similar concepts. The worst-case analysis does not restrict the input rewrite system in any way, which facilitates integration in a general framework for resource analysis of programs. In contrast to that the best-case analysis is designed for first-order eagerly evaluated term rewrite systems and thus provides novel methods to fully automatically infer lower bounds. More precisely, we establish univariate amortised resource analyses based on the potential method which gives rise to polynomial bounds of the term rewrite system investigated. Due to the invocation of small-step semantics, the methods do not presuppose termination. This complements earlier work on automated amortised resource analysis. We have implemented the methods and provide ample evidence of their viability.by Manuel Schneckenreither, MScUniversität Innsbruck, Masterarbeit, 2018(VLID)271194