Computability in polynomial time is generally regarded as capturing feasibility for functions. What is the proper notion of feasibility for functionals? A definition due to Steve Cook, Basic Feasible Functionals, is only one of several options that have been proposed and studied.
I will survey some work of Cook, Kapron, Seth and others on this issue, and present new applicative and proof theoretic characterizations of Cook's basic feasible functionals, which lend strong credence to the thesis that they constitute the correct notion of feasibility in type 2. These characterizations lift to higher type, providing a natural approach to feasibility in the entire type hierarchy.
Back to the list of talks