Characterizations of polynomial complexity classes with a better intensionality

ABSTRACT

In this paper, we study characterizations of polynomial complexity classes using first order functional programs and we try to improve their intensionality, that is the number of natural algorithms captured. We use polynomial assignments over the reals. The polynomial assignments used are inspired by the notions of quasiinterpretation and sup-interpretation, and are decidable when considering polynomials of bounded degree ranging over real numbers. Contrarily to quasi-interpretations, the considered assignments are not required to have the subterm property. Consequently, they capture a strictly larger number of natural algorithms (including quotient, gcd, duplicate elimination from a list) than previous characterizations using quasi-interpretations

REFERENCES

• 1: E. Albert, P. Arenas, S. Genaim, and G. Puebla. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. Proc. of Static Analysis Symposium (SAS), a. To appear.
• 2: E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost analysis of java bytecode. 16th European Symposium on Programming, ESOP, 7:157--172, b.
• 3: Thomas Arts , Jürgen Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, v.236 n.1-2, p.133-178, April 6, 2000 [doi>10.1016/S0304-3975(99)00207-8]
• 4: P. Baillot and V. Mogbil. Soft lambda-calculus: a language for polynomial time computation. In FOSSACS 2004, volume 2987 of LNCS, pages 27--41. Springer, 2004.
• 5: G. Bonfante , A. Cichon , J.-Y. Marion , H. Touzet, Algorithms with polynomial interpretation termination proof, Journal of Functional Programming, v.11 n.1, p.33-53, January 2001 [doi>10.1017/S0956796800003877]
• 6: G. Bonfante, J.-Y. Marion, J.-Y. Moyen, and R. Péchoux. Synthesis of quasi-interpretations. LCC2005, LICS affiliated Workshop, 2005. http://hal.inria.fr/.
• 7: G. Bonfante, J.Y. Marion, and J.Y. Moyen. Quasi-interpretations, a way to control resources. Accepted to Theoretical Computer Science, 2007. http://www.loria.fr/~marionjy/Research/Publications/Articles/TCS.pdf.
• 8: N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17(3):279--301, 1982.
• 9: M. Gaboardi and S. Ronchi Della Rocca. A soft type assignment system for λ-calculus. CSL 2007, 4646:253--267, 2007.
• 10: Marco Gaboardi , Jean-Yves Marion , Simona Ronchi Della Rocca, A logical account of pspace, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 11: Jean-Yves Girard, Light linear logic, Information and Computation, v.143 n.2, p.175-204, June 15, 1998 [doi>10.1006/inco.1998.2700]
• 12: Martin Hofmann, The strength of non-size increasing computation, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.260-269, January 16-18, 2002, Portland, Oregon
• 13: Gérard Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM (JACM), v.27 n.4, p.797-821, Oct. 1980 [doi>10.1145/322217.322230]
• 14: S. Kamin and J-J Lévy. Attempts for generalising the recursive path orderings. Technical report, University of Illinois, Urbana, 1980.
• 15: L. Kristiansen and N.D. Jones. The flow of data and the complexity of algorithms. In CIE, volume 3526, pages 263--274. Springer, 2005.
• 16: Keiichirou Kusakari , Masaki Nakamura , Yoshihito Toyama, Argument Filtering Transformation, Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming, p.47-61, September 29-October 01, 1999
• 17: Yves Lafont, Soft linear logic and polynomial time, Theoretical Computer Science, v.318 n.1-2, p.163-180, June 2004 [doi>10.1016/j.tcs.2003.10.018]
• 18: D.S. Lankford. On proving term rewriting systems are noetherien. Technical report, 1979.
• 19: S. Lucas. Polynomials over the reals in proofs of termination: from theory to practice. RAIRO Theoretical Informatics and Applications, 39(3):547--586, 2005.
• 20: Z. Manna and S. Ness. On the termination of Markov algorithms. In Third hawaii international conference on system science, pages 789--792, 1970.
• 21: J.-Y. Marion and R. Péchoux. Resource analysis by sup-interpretation. In FLOPS, volume 3945 of LNCS, pages 163--176, 2006.
• 22: Karl-Heinz Niggl , Henning Wunderlich, Certifying Polynomial Time and Linear/Polynomial Space for Imperative Programs, SIAM Journal on Computing, v.35 n.5, p.1122-1147, 2006 [doi>10.1137/S0097539704445597]
• 23: A. Tarski. A Decision Method for Elementary Algebra and Geometry, 2nd ed. University of California Press, 1951.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.0 General

General Terms:
Theory, Verification

Keywords:
quasi-interpretation, resource upper bounds, static analysis, sup-interpretation