Synthesis of Quasi-interpretations
Guillaume Bonfante, Jean-Yves Marion, Jean-Yves Moyen, Romain Péchoux · 2005
This paper presents complexity results by showing that the synthesis of Max-Poly quasi-interpretations over R+ is decidable in exponential time with xed polyno-mial degrees and xed max-degree and that the synthesis of Max-Plus quasi-interpretations over R+ is NPtime-complete with xed multiplicative degrees and xed max-degree. Quasi-interpretations are a tool that allows to control resources like the runtime, the runspace or the size of a result in a program execution. Quasi-interpretations assign to each program symbol a numerical function which is com-patible with the computational semantics and roughly speaking provide an upper bound on sizes of intermediate values computed. The synthesis problem is to nd a quasi-interpretation for a given program. We show that this problem is decidable in exponential time for the class of Max-Poly assignments over real numbers with xed polynomial degree and max-degree. The class Max-Poly contains the projections, max, addition, multiplication operations and is closed by composition. This class is broad enough to cover a lot of practical algorithms. Then we consider the class of Max-Plus of assignments which consists of pro-jections, addition, the max operation and is closed by composition. We extend the work of Amadio on the synthesis of Max-Plus quasi-interpretation over real num-bers by establishing that it is NPtime-complete with xed multiplicative degree and max-degree.