Mathematical Structures in Computer Science

Table of Contents - August 2012 - Volume 22, Issue 04  

Paper

On quasi-interpretations, blind abstractions and implicit complexity†

PATRICK BAILLOTa1, UGO DAL LAGOa2 and JEAN-YVES MOYENa3

a1 LIP, UMR 5668 CNRS, ENS-Lyon, UCBL, INRIA, Université de Lyon, France Email: patrick.baillot@ens-lyon.fr

a2 Università di Bologna, Italy Email: dallago@cs.unibo.it

a3 LIPN, UMR 7030 CNRS, Université Paris 13, France Email: jean-yves.moyen@lipn.univ-paris13.fr

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.

(Received July 23 2008)

(Revised September 23 2011)

(Online publication February 02 2012)

Footnotes

† This work was partially supported by projects CRISS (ACI), NO-CoST (ANR, JC05_43380).