The usual way of describing a bound on the time or space complexity of an algorithm is to give some expression, e.g., a polynomial, over the sizes of arguments of the algorithm. When the algorithm involves higher-type arguments, however, there is no commonly accepted notion of the "size" of a higher-type object nor, for that matter, of a "higher-type polynomial."

For type-level two, Kapron and Cook have proposed a notion of the length of a type-one object and of a notion of second-order polynomial. Moreover, they showed that, with respect to a reasonable machine model, the type-two "polynomial-time" computable functionals are exactly the type-2 basic feasible functionals (BFF₂), where BFF₂ is a class of functionals first described (via a programming formalism) in 1974 by Mehlhorn and later, independently, by Cook and Urquhart in 1989 (via a different programming formalism).

While this a deep and difficult characterization, it does not leave matters in a complete satisfactory state. First, on the programming formalism side, all the the prior programming formalism for BFF₂ are difficult to actually write programs in. Second, on the machine/poly-bounds side, programming is much easier in this context, but there is an air of ad hoc-ery the machine model and the poly-bounds.

In this talk we will present a characterization of BFF₂ based on type-theoretic constraints inspired by type-theoretic characterizations of type-1 polynomial-time by Bellantoni and Cook and by Leivant. While the Bellantoni-Cook and Leivant systems are strictly predicative, it seems necessary to partially break predicativity under our general approach. Also, in contrast to the prior programming formalisms characterizing BFF₂, our formalism is very close in spirit to Kapron and Cook's machine-based characterization of BFF₂.

If there is time, we will also discuss

• how to extend this characterization to higher types;
• higher-type notions of "polynomial" and "size," and
• some of the difficulties arising at type-three.

This is joint work with Robert Irwin and Bruce Kapron.