Abstract An adequate theory of partial computable functions should provide a basis for defining computational complexity measures and should justify the principle of computational induction for reasoning about programs on the basis of their recursive calls. There is no practical account of these notions in type theory, and consequently such concepts are not available in applications of type theory where they are greatly needed. It is also not clear how to provide a practical and adequate account in programming logics based on set theory.
This paper provides a practical theory supporting all these concepts in the setting of constructive type theories. We first introduce an extensional theory of partial computable functions in type theory. We then add support for intensional reasoning about programs by explicitly reflecting the essential properties of the underlying computation system. We use the resulting intensional reasoning tools to justify computational induction and to define computational complexity classes. Complexity classes take the formof complexity-constrained function types. These function types are also used in conjunction with the propositions-as-types principle to define a resource-bounded logic in which proofs of existence can guarantee feasibility of construction.
Introduction Over the past two decades, type theory has become the formalism of choice to support programming, verification and the logical foundations of computer science. The language of types underlies modern programming languages like Java and ML, and the theory of types drives significant efforts in compilation [29, 50, 36, 39, 42, 6, 47] and semantics [7, 23, 16]. Theorem proving systems based on type theory have been used for the verification of both hardware and software, and have also been very widely used for the formalization of mathematics [8, 10, 26, 24, 41, 46].
One of the major reasons type theory has enjoyed such wide successes is that it is a natural high-level language for computational mathematics and programming, a point that Sol Feferman has effectively made over the years [20, 22]. However, this advantage can sometimes pose a problem because the needs of mathematics and programming can diverge. In mathematics, equality is extensional, where only an object's value is significant. That is, if the result of f(a) is b then f(a) = b, and functions f and g are equal (in A → B, the space of functions from A to B) exactly when f(a) = g(a) for every a in A.