Quasi-interpretation Synthesis by Decomposition: An Application to Higher-Order Programs

摘要

Quasi-interpretation analysis belongs to the field of implicit computational complexity (ICC) and has shown its interest to deal with resource analysis of first-order functional programs, which are terminating or not. In this paper, we tackle the issue of program decomposition wrt quasi-interpretations analysis. For that purpose, we use the notion of modularity. Firstly, modularity decreases the complexity of the quasi-interpretation search algorithms. Secondly, modularity increases the in-tentionality of the quasi-interpretation method, that is the number of captured programs. Finally, we take advantage of modularity conditions to extend smoothly quasi-interpretations to higher-order programs. We study the modularity of quasi-interpretations through the notions of constructor-sharing and hierarchical unions of programs. We show that, in both cases, the existence of quasi-interpretations is no longer a modular property. However, we can still certify the complexity of programs by showing, under some restrictions, that the size of the values computed by a program remains polynomially bounded by the inputs.