Predicative Analysis of Feasibility and Diagonalization

International audiencePredicative analysis of recursion schema is a method to characterize complexity classes like the class of polynomial time functions. This analysis comes from the works of Bellantoni and Cook, and Leivant. Here, we refine predicative analysis by using a ramified Ackermann's construction of a non-primitive recursive function. We obtain an hierarchy of functions which characterizes exactly functions, which are computed in $O(n^k)$ over register machine model of computation. Then, we are able to diagonalize using dependent types in order to obtain an exponential function