On Quasi-Interpretations, Blind Abstractions and Implicit Complexity

TL;DR

This paper explores quasi-interpretations and the P-criterion to characterize polynomial-time programs, introducing the concept of blind abstraction and extending the criterion to better understand implicit complexity.

Contribution

It demonstrates that programs satisfying a variant of the P-criterion are blindly polynomial and proposes extensions to the criterion for more precise complexity analysis.

Findings

All programs satisfying a variant of the P-criterion are blindly polynomial.

Extensions of the P-criterion include relaxed termination conditions and the bounded value property.

The bounded value property provides a necessary and sufficient condition for polynomial-time execution with memoisation.

Abstract

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.