Seminar 19 Apr, 2012

Automated Complexity Analysis for Integer Term Rewrite Systems


An integer term rewrite system (ITRS) is defined as an ordinary term rewrite system but with predefined constants, i.e., integers and booleans. Moreover, every ITRS contains implicitly of an infinite set of rules defining predefined operations on these constants like addition and subtraction. A modular framework which analyzes the runtime complexity of an ITRS w.r.t. constructor rewriting will be presented. Especially, it will be shown how we can adopt polynomial interpretations on integers with the "maximum" function, known from termination analysis for ITRSs, to this framework to determine polynomial bounds for ITRSs.