Tiered complexity at higher order

In [1], Kapron and Steinberg introduce restrictions on Oracle Turing Machines to characterize the class of basic feasible functionals (BFF). The Oracle Turing Machines they consider M φ are Turing Machines with one query tape for oracle calls. If a query is written on such a tape and the machine enters a query-state, then the machine outputs the oracle's answer on the query tape in one step. Definition 1. Given an OTM M φ and an input a, let m M φ a be the maximum of the size of the input a and of the biggest oracle's answer in the run of machine on input a with oracle φ. A machine M φ has:-a polynomial step count if there is a polynomial P such that for any input a and oracle φ, M runs in time bounded by P (m M φ a).-a finite length revision if there exists a natural number n such that for any oracle and any input, in the run of the machine, the number of times it happens that an oracle answer is bigger than the input and all of the previous oracle answers is at most n.-a finite lookahead revision if there exists a natural number n such that for any oracle and any input, in the run of the machine, it happens at most n times that a query is posed whose size exceeds the size of all previous queries. Definition 2 (Strong and Moderate Poly-Time).-SPT is the class of second order functions computable by an OTM with a polynomial step count and finite length revision.-MPT is the class of second order functions computable by an OTM with a polynomial step count and finite lookahead revision. For a given class of functionals X, let λ(X) be the set of simply typed lambda-terms where a constant symbol is available for each element of X. Let λ(X) 2 be the set of type two functionals represented by type two terms of λ(X). They obtain the following characterization of BFF: Theorem 1. λ(MPT) 2 = λ(SPT) 2 = BF F The main interest of this characterization is that it does not require the use of polynomial at order 2 and the semantics restrictions on the OTM are very natural. We are now interested in finding a static analysis criterion allowing to ensure that a program computes a function of BF F. Our target is an implicit computational complexity characterization of BFF based on Kapron and Steinberg's restrictions.