Feasibility in Higher Types

Daniel Leivant
Indiana University

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.

Daniel Leivant

Computer Science Department
Indiana University
Lindley Hall 215
Bloomington, IN 47405 USA
Email: leivant@cs.indiana.edu
Home page: http://www.cs.indiana.edu/people/l/leivant.html

Back to the list of talks