Quasi-interpretations. A way to control resources (Q541228)

Interpretations have been used in program and software optimization by researchers such as Dershowitz and Cobham [\textit{N. Dershowitz}, Theor. Comput. Sci. 17, 279--301 (1982; Zbl 0525.68054); \textit{A. Cobham}, in: Logic Methodology Philos. Sci., Proc. 1964 internat. Congr. 24--30 (1965; Zbl 0192.08702)]. The authors introduce the notion of quasi-interpretation that allows them to provide a characterization of the functions computable in polynomial space and in polynomial time. In a formal programming scheme, an assignment is a map associating to each function symbol and each constructor a real function. An assignment is extended recursively and monotonically, according to composition orderings, to the whole programming structures within the scheme in order to obtain the so-called quasi-interpretations. Thus a quasi-interpretation is a numerical map compatible with the operational semantics. The verification problem (given a program and an assignment decide whether the assignment is a quasi-interpretation of the program) and the synthesis problem (given a program decide whether it possesses a quasi-interpretation) are posed and they are shown to be decidable. Tarski's theorem related to the decidability of real closed fields is used here in a very instructive way. Also, program termination conditions are discussed within the frame of quasi-interpretations. A program is additive, affine or multiplicative according to the form of the corresponding quasi-interpretations. When the quasi-interpretations are restricted to the class MaxPoly spanned by the non-negative rational constants and the operators of projection, maximum, addition, multiplication and composition, then polynomial time and space complexities are estimated for additive programs, exponential for affine programs and doubly-exponential for multiplicative programs. These results together with the termination conditions allow a characterization of the functions calculable by programs in PSPACE and PTIME.