Quasi-interpretations and Small Space Bounds

  • Guillaume Bonfante
  • Jean-Yves Marion
  • Jean-Yves Moyen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3467)


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 space-bounded 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.


Turing Machine Function Symbol Transitive Closure Polynomial Space Covering Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Benzinger, R.: Automated complexity analysis of NUPRL extracts. PhD thesis, Cornell University (1999)Google Scholar
  2. 2.
    Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, Springer, Heidelberg (1989)Google Scholar
  3. 3.
    Cichon, E., Lescanne, P.: Polynomial interpretations and the complexity of algorithms. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 139–147. Springer, Heidelberg (1992)Google Scholar
  4. 4.
    Bonfante, G., Cichon, A., Marion, J.Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. Journal of Functional Programming 11 (2000)Google Scholar
  5. 5.
    Marion, J.Y., Moyen, J.Y.: Efficient first order functional program interpreter with time bound certifications. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 25–42. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Bonfante, G., Marion, J.Y., Moyen, J.Y.: On lexicographic termination ordering with space bound certifications. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, p. 482. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Hofbauer, D.: Termination proofs with multiset path orderings imply primitive recursive derivation lengths. Theoretical Computer Science 105, 129–140 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    Weiermann, A.: Termination proofs by lexicographic path orderings yield multiply recursive derivation lengths. Theoretical Computer Science 139, 335–362 (1995)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Ritchie, R.: Classes of predictably computable functions. Transaction of the American Mathematical Society 106, 139–173 (1963)zbMATHMathSciNetCrossRefGoogle Scholar
  10. 10.
    Beckmann, A., Weiermann, A.: A term rewriting characterization of the polytime functions and related complexity classes. Archive for Mathematical Logic 36, 11–30 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Marion, J.Y.: Analysing the implicit complexity of programs. Information and Computation 183, 2–18 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the polytime functions. Computational Complexity 2, 97–110 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Leivant, D.: Predicative recurrence and computational complexity I: Word recurrence and poly-time. In: Clote, P., Remmel, J. (eds.) Feasible Mathematics II, pp. 320–343. Birkhäuser, Basel (1994)Google Scholar
  14. 14.
    Leivant, D., Marion, J.Y.: Lambda calculus characterizations of poly-time. Fundamenta Informaticae 19, 167 (1993)zbMATHMathSciNetGoogle Scholar
  15. 15.
    Jones, N.D.: LOGSPACE and PTIME characterized by programming languages. Theoretical Computer Science 228, 151–174 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    Gurevich, Y.: Algebras of feasible functions. In: Twenty Fourth Symposium on Foundations of Computer Science, pp. 210–214. IEEE Computer Society Press, Los Alamitos (1983)Google Scholar
  17. 17.
    Oitavem, I.: A term rewriting characterization of the functions computable in polynomial space. Archive for Mathematical Logic 41, 35–47 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Amadio, R., Coupet-Grimal, S., Zilio, S.D., Jakubiec, L.: A functional scenario for bytecode verification of resource bounds. In: CSL. (2004) (to appear) Google Scholar
  19. 19.
    Amadio, R.M., Dal-Zilio, S.: Resource control for synchronous cooperative threads. In: CONCUR, pp. 68–82 (2004) Google Scholar
  20. 20.
    Bonfante, G., Marion, J.Y., Moyen, J.Y., Péchoux, R.: Synthesis of quasiinterpretations. Technical report, Loria (2005) Submited to RULE 2005, Available at
  21. 21.
    Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-interpretations. Technical report, Loria (2004) Submited to Theoretical Computer Science, accessible:
  22. 22.
    Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM 27, 797–821 (1980)zbMATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Grädel, E., Gurevich, Y.: Tailoring recursion for complexity. Journal of Symbolic Logic 60, 952–969 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  24. 24.
    Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science 17, 279–301 (1982)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Krishnamoorthy, M.S., Narendran, P.: On recursive path ordering. Theoretical Computer Science 40, 323–328 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  26. 26.
    Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-interpretations and small space bounds. Technical report, Loria (2005),
  28. 28.
    Dershowitz, N.: A note on simplification ordering. Information Processing Letters 9, 212–215 (1979)zbMATHCrossRefMathSciNetGoogle Scholar
  29. 29.
    Bonfante, G.: Constructions d’ordres, analyse de la complexité. Thèse, Institut National Polytechnique de Lorraine (2000)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Guillaume Bonfante
    • 1
    • 2
  • Jean-Yves Marion
    • 1
    • 2
  • Jean-Yves Moyen
    • 1
    • 3
  1. 1.Loria, Calligramme projectVandœuvre-lès-Nancy CédexFrance
  2. 2.INPLÉcole Nationale Supérieure des Mines de NancyFrance
  3. 3.Université Henri Poincaré Nancy IFrance

Personalised recommendations