Max-plus quasi-interpretations

Abstract

Quasi-interpretations are a tool to bound the size of the values computed by a first-order functional program (or a term rewriting system) and thus a mean to extract bounds on its computational complexity. We study the synthesis of quasi-interpretations selected in the space of polynomials over the max-plus algebra determined by the non-negative rationals extended with -∞ and equipped with binary operations for the maximum and the addition. We prove that in this case the synthesis problem is NP-hard, and in NP for the particular case of multi-linear quasi-interpretations when programs are specified by rules of bounded size. The relevance of multi-linear quasi-interpretations is discussed by comparison to certain syntactic and type theoretic conditions proposed in the literature to control time and space complexity. © Springer-Verlag Berlin Heidelberg 2003.