Some applications of logic to feasibility in higher types

TL;DR

This paper explores the logical foundations of basic feasible functionals, extending their recursion properties, improving their representation, and demonstrating how logic can extract feasible programs from complex proofs.

Contribution

It introduces a logical framework characterizing basic feasible functionals and shows how to derive feasible programs from non-feasible mathematical proofs.

Findings

Basic feasible functionals have recursion-theoretic properties similar to feasible functions.

A weak fragment of second order arithmetic characterizes basic feasible functionals.

Feasible programs can be extracted from proofs involving non-feasible functionals.

Abstract

In this paper we demonstrate that the class of basic feasible functionals has recursion theoretic properties which naturally generalize the corresponding properties of the class of feasible functions. We also improve the Kapron - Cook result on mashine representation of basic feasible functionals. Our proofs are based on essential applications of logic. We introduce a weak fragment of second order arithmetic with second order variables ranging over functions from N into N which suitably characterizes basic feasible functionals, and show that it is a useful tool for investigating the properties of basic feasible functionals. In particular, we provide an example how one can extract feasible "programs" from mathematical proofs which use non-feasible functionals (like second order polynomials).