Quasi-interpretations and small space bounds

Abstract

Quasi-interpretations are an useful tool to control resources usage of term rewriting systems, either time or space. They not only combine well with path orderings and provide characterizations of usual complexity classes but also give hints in order to optimize the program. Moreover, the existence of a quasi-interpretation is decidable. In this paper, we present some more characterizations of complexity classes using quasi-interpretations. We mainly focus on small spacebounded complexity classes. On one hand, by restricting quasi-interpretations to sums (that is allowing only affine quasi- interpretations), we obtain a characterization of LINSPACE. On the other hand, a strong tiering discipline on programs together with quasi-interpretations yield a characterization of LOGSPACE. Lastly, we give two new characterizations of PSPACE: in the first, the quasi-interpretation has to be strictly decreasing on each rule and in the second, some linearity constraints are added to the system but no assumption concerning the termination proof is made. © Springer-Verlag Berlin Heidelberg 2005.