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 Urquahart'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).
展开▼
