Some applications of logic to feasibility in higher types

ABSTRACT

While it is commonly accepted that computability on a Turing machine in polynomial time represents a correct formalization of the notion of a feasibly computable function, there is no similar agreement on how to extend this notion on functionals, that is, what functionals should be considered feasible. One possible paradigm was introduced by Mehlhorn, who extended Cobham's definition of feasible functions to type 2 functionals. Subsequently, this class of functionals (with inessential changes of the definition) was studied by Townsend who calls this class POLY, and by Kapron and Cook who call the same class basic feasible functionals. Kapron and Cook gave an oracle Turing machine model characterisation of this class. In this article, we demonstrate that the class of basic feasible functionals has recursion theoretic properties which naturally generalise the corresponding properties of the class of feasible functions, thus giving further evidence that the notion of feasibility of functionals mentioned above is correctly chosen. We also improve the Kapron and Cook result on machine representation.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^N which suitably characterises 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 that use nonfeasible functions.

REFERENCES

• 1: Allen, B. 1991. Arithmetising Uniform NC. Ann. Pure Appl. Logic 53, 1, 1--50.
• 2: Buss, S. R. 1986. Bounded Arithmetic. Bibliopolis.
• 3: Clote, P., Ignjatovic, A., and Kapron, B. 1993. Parallel computable higher type functionals. In Proceedings of the 34th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 72--81.
• 4: Clote, P. and Takeuti, G. 1992. Bounded Arithmetic for NC, ALogTIME, L and NL. Ann. Pure Appl. Logic 56, (1--3), 73--117.
• 5: Cobham, A. 1965. The intrinsic computational difficulty of functions. In Logic, Methodology and Philosophy of Science II. Y. Bar-Hillel, Ed. North-Holland, Amsterdam, The Netherlands, 24--30.
• 6: B. M. Kapron , S. A. Cook, A New Characterization of Type-2 Feasibility, SIAM Journal on Computing, v.25 n.1, p.117-132, Feb. 1996 [doi>10.1137/S0097539794263452]
• 7: Mehlhorn, K. 1976. Polynomial and abstract subrecursive classes. J. Comput. Syst. Sci. 12, 147--178.
• 8: Sieg, W. 1985. Fragments of arithmetic. Ann. Pure Appl. Logic 28, 33--71.
• 9: Sieg, W. 1991. Herbrand analyses. Arch. Math. Logic 30, 409 -- 441.
• 10: Townsend, M. 1990. Complexity for type-2 relations. Notre Dame J. Form. Logic 31, 241 -- 262.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Relations between models

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Relations among complexity classes
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Proof theory; Computability theory

General Terms:
Algorithms, Theory

Keywords:
bounded arithmetic, functionals, higher-order complexity, second-order theories