Implicit Computational Complexity for Higher Type Functionals

Abstract In previous works we argued that second order logic with comprehension restricted to positive formulas can be viewed as the core of Feasible Mathematics. Indeed, the equational programs over strings that are provable in this logic compute precisely the poly-time computable functions. Here we investigate the provable functionals of this logic, and show that they are precisely Cook and Urquhart’s basic feasible functionals, BFF. This further confirms the stability of BFF as a notion of computational feasibility in higher type. Using a formula-as-type morphism, we also show that BFF consists precisely of the functionals that are lambda representable in F 2 restricted to positive type arguments (and trivially augmented with basic constructors and destructors).

Authors

• Daniel Leivant

Keywords

No keywords are indexed for this paper.