On quasi-interpretations, blind abstractions and implicit complexity

Abstract. Quasi-interpretations are a technique to guarantee complex-ity bounds on first-order functional programs: with termination order-ings they give in particular a sufficient condition for a program to be executable in polynomial time ([MM00]), called here the P-criterion. We study properties of the programs satisfying the P-criterion, in order to better understand its intensional expressive power. Given a program on binary lists, its blind abstraction is the non-deter-ministic program obtained by replacing lists by their lengths (natural numbers). A program is blindly polynomial if its blind abstraction ter-minates in polynomial time. We show that all programs satisfying a variant of the P-criterion are in fact blindly polynomial. Then we give two extensions of the P-criterion: one by relaxing the termination order-ing condition, and the other one (the bounded value property) giving a necessary and sufficient condition for a program to be polynomial time executable, with memoisation.