Hostname: page-component-586b7cd67f-dsjbd Total loading time: 0 Render date: 2024-11-28T17:27:06.771Z Has data issue: false hasContentIssue false
  • English
  • Français

On quasi-interpretations, blind abstractions and implicit complexity†

Published online by Cambridge University Press:  02 February 2012

PATRICK BAILLOT ,
UGO DAL LAGO  and
JEAN-YVES MOYEN
PATRICK BAILLOT
Affiliation:
LIP, UMR 5668 CNRS, ENS-Lyon, UCBL, INRIA, Université de Lyon, France Email: [email protected]
UGO DAL LAGO
Affiliation:
Università di Bologna, Italy Email: [email protected]
JEAN-YVES MOYEN
Affiliation:
LIPN, UMR 7030 CNRS, Université Paris 13, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

Quasi-interpretations are a technique for guaranteeing complexity bounds on first-order functional programs: in particular, with termination orderings, they give a sufficient condition for a program to be executable in polynomial time (Marion and Moyen 2000), which we call the P-criterion here. We study properties of the programs satisfying the P-criterion in order to improve the understanding of its intensional expressive power. Given a program, its blind abstraction is the non-deterministic program obtained by replacing all constructors with the same arity by a single one. A program is blindly polytime if its blind abstraction terminates in polynomial time. We show that all programs satisfying a variant of the P-criterion are in fact blindly polytime. Then we give two extensions of the P-criterion: one relaxing the termination ordering condition and the other (the bounded-value property) giving a necessary and sufficient condition for a program to be polynomial time executable, with memoisation.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 22 , Issue 4 , August 2012 , pp. 549 - 580
Copyright
Copyright © Cambridge University Press 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Amadio, R. (2005) Synthesis of max-plus quasi-interpretations. Fundamenta Informaticae 65 29–60.Google Scholar
Avanzini, M. and Moser, G. (2008) Complexity analysis by rewriting. In: Proceedings of 9th International Symposium on Functional and Logic Programming. Springer-Verlag Lecture Notes in Computer Science 4989 130–146.Google Scholar
Bellantoni, S. J. and Cook, S. A. (1992) A new recursion-theoretic characterization of the poly-time functions. Computational Complexity 2 97–110.Google Scholar
Bonfante, G., Cichon, A., Marion, J.-Y. and Touzet, H. (2001) Algorithms with polynomial interpretation termination proof. Journal of Functional Programming 11 (1)33–53.CrossRefGoogle Scholar
Bonfante, G., Marion, J.-Y. and Moyen, J.-Y. (2001) On lexicographic termination ordering with space bound certifications. In: Ershov Memorial Conference. Springer-Verlag Lecture Notes in Computer Science 2244 482–493.CrossRefGoogle Scholar
Bonfante, G., Marion, J.-Y. and Moyen, J.-Y. (2005) Quasi-Interpretations and Small Space Bounds. In: Proceedings of The International Conference on Rewriting Techniques and Applications (RTA 2005). Springer-Verlag Lecture Notes in Computer Science 3467.Google Scholar
Bonfante, G., Marion, J.-Y. and Moyen, J.-Y. (2011) Quasi-interpretations – a way to control resources. Theoretical Computer Science 412 (25)2776–2796.Google Scholar
Bonfante, G., Marion, J.-Y. and Péchoux, R. (2007) Quasi-interpretation synthesis by decomposition. In: Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC 2007). Springer-Verlag Lecture Notes in Computer Science 4711 410–424.Google Scholar
Dal Lago, U. (2007) Note on the intentional expressive power of bounded calculi. Manuscript available at http://www.cs.unibo.it/~dallago/iepbc.pdf.Google Scholar
Dershowitz, N. (1982) Orderings for term-rewriting systems. Theoretical Computer Science 17 (3)279–301.CrossRefGoogle Scholar
Girard, J.-Y. (1998) Light linear logic. Information and Computation 143 175–204.Google Scholar
Hofmann, M. (1999) Linear types and Non-Size Increasing polynomial time computation. In: Proceedings of the Fourteenth IEEE Symposium on Logic in Computer Science (LICS '99) 464–473.CrossRefGoogle Scholar
Hofmann, M. (2003) Linear types and non-size-increasing polynomial time computation. Information and Computation 183 (1)57–85.Google Scholar
Huet, G. (1980) Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM 27 (4)797–821.CrossRefGoogle Scholar
Jones, N. D. (1999) LOGSPACE and PTIME characterized by programming languages. Theoretical Computer Science 228 151–174.CrossRefGoogle Scholar
Kamin, S. and Lévy, J.-J. (1980) Attempts for generalising the recursive path orderings. Technical report, University of Illinois, Urbana Champaign. Available at http://perso.ens-lyon.fr/pierre.lescanne/not_accessible.html#termination.Google Scholar
Klop, J. W. and de Vrijer, R. (2003) Term Rewriting Systems, Cambridge University Press.Google Scholar
Leivant, D. (1994) Predicative recurrence and computational complexity I: word recurrence and poly-time. In: Feasible Mathematics II, Birkhauser 320–343.Google Scholar
Leivant, D. and Marion, J.-Y. (1993) Lambda calculus characterizations of poly-time. In: Proceedings of Typed Lambda Calculi and Applications (TLCA '05). Springer-Verlag Lecture Notes in Computer Science 664 274–288.Google Scholar
Marion, J.-Y. (2003) Analysing the implicit complexity of programs. Information and Computation 183 (1)2–18.CrossRefGoogle Scholar
Marion, J.-Y. and Moyen, J.-Y. (2000) Efficient First Order Functional Program Interpreter with Time Bound Certifications. In: Proceedings of Logic for Programming Artificial Intelligence and Reasoning (LPAR '00). Springer-Verlag Lecture Notes in Artificial Intelligence 1955 25–42.Google Scholar
Marion, J.-Y. and Péchoux, R. (2006) Resource analysis by sup-interpretation. In: Proceedings of Symposium on Functional and Logic Programming (FLOPS '06) Springer-Verlag Lecture Notes in Computer Science 3945 163–176.CrossRefGoogle Scholar
Marion, J.-Y. and Péchoux, R. (2009) Sup-interpretations, a semantic method for static analysis of program resources. ACM Transactions on Computational Logic (TOCL) 10 (4).Google Scholar
Moyen, J.-Y. (2003) Analyse de la complexité et transformation de programmes, Thèse d'Université (Ph.D. Thesis), University Nancy 2.Google Scholar
Péchoux, R. (2007) Analyse de la complexité des programmes par interprétation sémantique, Ph.D. Thesis, Institut National Polytechnique de Lorraine.Google Scholar