2006/08/06 by Patrick Baillot, Baillot, Patrick, Ugo Dal Lago +3
Computer Science · #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #cs.CC #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.cs/0608030
18 pages
arxiv created 2006/08/06 · openalex publication_date 2006/08/06 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Quasi-interpretations are a technique to guarantee complexity bounds on first-order functional programs: with termination orderings they give in particular a sufficient condition for a program to be executable in polynomial time, 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 nondeterministic program obtained by replacing lists by their lengths (natural numbers). A program is blindly polynomial if its blind abstraction terminates 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 ordering 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.