A note on complexity measures for inductive classes in constructive type theory

It is notoriously hard to express computational complexity properties of programs in programming logics based on a semantics which respects extensional function equality. That is a serious impediment to applications of programming logics requiring reasoning about complexity. This paper shows how to use existing mechanisms to define internal computational complexity measures in logics that support inductively defined types, dependent products, and functions. The method exploits a feature of inductive definitions in constructive type theory, namely that implicit proof codes are kept with the objects showing how they are presented in the inductive class. The idea is illustrated by giving a formal inductive definition of PTime based on ideas from Leivant's work and on Bellantoni and Cook's approach. Then a complexity measure is defined on elements of this class. This paper discusses the limitations of this idea and the need for faithfulness guarantees that link internal complexity classes to the implementation of the logic. The paper concludes with a definition of resource bounded logics and a discussion of interesting lines of investigation of these logics which have the potential to make practical uses of results from computational complexity theory in formal reasoning about the efficiency of programs. (C) 1998 Academic Press.