Synthesis of max-plus quasi-interpretations

Issue title: Typed Lambda Calculi and Applications 2003, Selected Papers

Article type: Research Article

Authors: Amadio, Roberto M.

Affiliations: Université de Provence, Centre de Math'matiques et d'Informatique (CMI), France. amadio@cmi.univ-mrs.fr

Note: [] Address for correspondence: CMI, 39 rue Joliot-Curie, 13453 Marseille, France

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. We prove that the synthesis problem is NP-hard under various conditions and in NP for the particular case of multi-linear quasi-interpretations when programs are specified by rules of bounded size. We provide a polynomial time algorithm to synthesize homogeneous quasi-interpretations of bounded degree and show how to extend the algorithm to synthesize (general) quasi-interpretations. The resulting algorithm generalizes certain syntactic and type theoretic conditions proposed in the literature to control time and space complexity.

Keywords: Functional languages and term rewriting, Function algebras and implicit computational complexity, Static analysis, Polynomial interpretations and max-plus algebras

Journal: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 29-60, 2005