Qqqqqqqqqqqqqqqqq

Computational Complexity and Induction for Partial Computable Functions in Type Theory
Robert L. Constable Cornell University Karl Crary Carnegie Mellon University

March 2, 1999

Abstract
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 typetheory 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 rst introduce an extensional theory of partial computable functions in type theory. We then add support for intensional reasoningabout programs by explicitly reecting the essential properties of the underlying computation system. We use the resulting intensional reasoning tools to justify computational induction and to de ne computational complexity classes. Complexity classes take the form of complexity-constrained function types. These function types are also used in conjunction with the propositions-as-types principle tode ne a resource-bounded logic in which proofs of existence can guarantee feasibility of construction.
computational complexity measures and should justify the principle of computational induction

An adequate theory of partial computable functions should provide a basis for de ning

1 Introduction
Over the past two decades, type theory has become the formalism of choice to supportprogramming, veri cation 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 signi cant e orts in compilation 24, 43, 31, 34, 36, 7, 40] and semantics 8, 20, 16]. Theorem proving systems based on type theory have been used for the veri cation of both hardware and software, and have also been verywidely used for the formalization of mathematics. One of the major reasons type theory has enjoyed such wide successes is that it is a natural highlevel language for computational mathematics and programming. 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 signicant. That is, if the result of f (a) is b then f (a) = b, and functions f and g are equal (in A ! B ) exactly when f (a) = g (a) for every a in A. In contrast, in the analysis of programs, it is often critical to consider programs intensionally, reasoning about their structure as well as their result value. For example, showing 1

partial correctness of recursive procedures requires reasoninginductively about the computation of recursive calls. Also, computational complexity certainly depends on a program's algorithm, and not only on its result. So a programming logic must reconcile two needs: one, the need to treat functions extensionally in order to interface with mathematics and to express the most general laws of substitution; and, two, the need to treat functions intensionally (asalgorithms) in order to state the most useful rules of program reasoning and to express complexity. There have been several attempts at this reconciliation, some of which are theoretically quite interesting 11, 42, 3, 29, 30]. Nevertheless, none of these are very practical, nor have any been implemented. We set as our goal producing a practical and adequate account of partial functions,computational induction and computational complexity in the class of constructive type theories such as those of Martin-Lof or Girard. This means that the type theory is built on an underlying computation system (or programming language), and reasoning about this computation system will be central to our account. The particular type theory we have chosen in which to formalize our account is summarized in...