Polynomial Time Type-2 Computation

Bruce M. Kapron
University of Victoria

The theory of type-2 computability extends ordinary computability theory by allowing functions as well as numbers as input arguments. This theory provides a foundation for areas such as effective descriptive set theory and computable real analysis, and has a long and well-established history. It is also a starting point for the theory of computation in higher types, which in turn provides part of the foundation of modern programming language theory. In contrast to the situation with general type-2 computability, to date there have been only a few attempts to consider resource-bounded type-2 computability. Constable [2] and Mehlhorn [4] proposed machine-independent definitions of type-2 polynomial-time, but did not relate these definitions to any purely machine-theoretic characterization. Recently, Kapron and Cook [3] and Royer [5] have proposed machine-theoretic characterizations based on different notions of type-2 computability, and studied their relationship to Mehlhorn's original definition.

Mehlhorn obtained his definition of type-2 polynomial-time by relativizing Cobham's [1] original definition of polynomial-time. Mehlhorn's class is characterized as the smallest class containing certain type-1 polynomial-time functions and the type-2 application functional, which is closed under composition and bounded recursion on notation. The latter is a variant of primitive recursion in which the recursion is based on the binary notation of a numerical input, and for which the final result can be bounded by a function in the class.

Type-2 computability comes in three basic flavors. The following is a brief description of each.

Kapron and Cook gave a polynomial-time version of the partial recursive functionals in the case where function inputs are total. Later Seth [6] showed how this could be extended to partial function inputs. Royer [5] presented a polynomial-time version of the effective operations.

In order to define resource-bounded versions of these models, we must answer a basic question: how do we measure resource usage as a uniform function of input size? More specifically, what is the ``size'' of a function input? In [3] the following answer is provided: if f is a function from N to N, then |f|, the size of f, is the function \n.max{|f(x)| : |x| <= n}. The idea behind this is that if the cost associated with querying an input oracle f at some y is |f(y)|, then |f| gives a uniform measure of the cost of accessing f over all inputs up to a given size. Given this definition of the size of a function input, there is a natural definition of being polynomial in the size of a function input.

Kapron and Cook show that the class total recursive functionals which are computed by oracle Turing machines with running time polynomial in the size of their function inputs correspond exactly to Mehlhorn's class. This result is not merely a relativization of Cobham's original characterization result. A major difficulty lies in the the fact that the functional \f \n. |f|(n) is not in Mehlhorn's class. The essential observation made in [3] is that the full power of |f| is not required, since the running time can only depend on those values of f which are actually queried during the computation. This is also the basis for Seth's notion of clocking for type-2 polynomial-time functionals. In Seth's model, machines have clocks which are updated using the size of oracle answers, The clocking notion also is essential in Royer's definition of a polynomial-time version of the effective operations. In Royer's model, such operations are computed by clocked Turing machines which may perform any operation on the code corresponding to its function input. However, the clock is updated only in the case where the code is accessed by a special subroutine which simulates the computation of the corresponding recursive function on a given numerical input. In this case, the number of steps in the simulation is used to do the update, rather than the size of the result.

An important result of type-2 recursion theory, the Kreisel-Lacombe-Shoenfield theorem, states that when restricted to total recursive inputs, the total effective operations correspond to the effective continuous functionals. This correspondence can also be extended to include the partial recursive functionals. Royer considered a polynomial-time version of this result, and was able to show that if, when restricted to total recursive inputs, the clocked polynomial-time effective operations correspond to Mehlhorn's class, then P is not equal to NP. Hence proving such a result will be extremely difficult. However, if the notion of effective operation is weakened to allow functionals only to access computations of their function inputs, rather than their program code, then a correspondence can be established.

Recently, Kapron proposed a definition for poly-time effective continuous functionals, and conjectured that when restricted to total inputs, these coincide with Mehlhorn's class. Royer has shown that if this conjecture holds, then there is a poly-time factorization algorithm.


  1. A. Cobham. The intrinsic computational difficulty of functions. In Y. Bar-Hillel, ed., Logic, Methodology and Philosophy of Science II, pp. 24--30. North-Holland, 1973.
  2. R. Constable. Type 2 computational complexity. In Proceedings of the 5th Annual ACM Symposium on the Theory of Computing, 1973. pp. 108--121.
  3. B.M. Kapron and S.A. Cook. A new characterization of type-2 feasiblity. SIAM J. on Computing 25:117-132:
  4. K. Mehlhorn. Polynomial and abstract subrecursive classes. JCSS, 12:147--178, 1976
  5. J.S. Royer. Semantics vs. syntax vs. computations. In Proceedings of the 10th Annual IEEE Structure in Complexity Conference, 1995, pp. 37--48
  6. A. Seth. There is no recursive axiomatization for feasible functionals of type 2. In Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, 1992, pp. 286--295.

Bruce M. Kapron

Department of Computer Science

Victoria, BC
Email: bmkapron@csr.uvic.ca
Home page: http://www.csc.uvic.ca/home/bmkapron/bmkapron.html

Back to the list of talks