a1 LIP, UMR 5668 CNRS, ENS-Lyon, UCBL, INRIA, Université de Lyon, France Email: email@example.com
a2 Università di Bologna, Italy Email: firstname.lastname@example.org
a3 LIPN, UMR 7030 CNRS, Université Paris 13, France Email: email@example.com
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.
(Received July 23 2008)
(Revised September 23 2011)
(Online publication February 02 2012)
† This work was partially supported by projects CRISS (ACI), NO-CoST (ANR, JC05_43380).