Expressing Computational Complexity in Constructive Type Theory
by Robert L. Constable
Proceedings of International Workshop on Logic and Computational Complexity (LCC'94), D. Leivant (ed.), LNCS 960, pp. 131-144, Springer-Verlag
It is notoriously hard to express computational complexity properties of programs in programming logics based on a semantics which respects extensional function equality. This is a serious impediment to certain key applications of programming logics, even those which apply very well otherwise.
This paper shows how to define computational complexity measures in such logics as long as they support inductively defined types, dependent products, and functions. The method exploits a natural feature of inductive definitions in type theory, namely that implicit codes are kept with the objects showing how they are presented in the inductive class.
The adequacy of the proposed definition depends on a faithfulness theorem showing that the external (or meta-level) definition of complexity is respected by the internal definition. The results are applied to defining resource bounded quantifiers that can be used to state complexity constraints on constructive proofs and their extracted programs. In such resource bounded logic it is possible to prove theorems like a PTime axiom of choice. The results of the paper bridge the fields of semantics and complexity to a small extent.
bibTex ref: Con95