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

This paper proposes the use of constructive type theory in the sense of Martin-Löf as a framework for a formal study of computational complexity. To this end a type theory \(\Pi\mu\Sigma^+\) is defined -- essentially a subset of Martin-Löf's extensional type theory with \(\Pi\)-, \(\Sigma\)- and inductive types. Starting from a syntactic characterisation of a certain subset of the recursive functions, e.g., primitive recursive functions or polynomial time functions (via Cobham's or Bellantoni-Cook's function algebra), the author formalises that class as a subset type of the full function space in the type theory. For instance, primitive recursive functions are defined as the type \[ {\mathcal PR} = \Sigma f{:}{\mathbb N}\rightarrow{\mathbb N} . \text{PrimRec}(f), \] where \(\text{PrimRec}(f)\) is an inductively defined predicate singling out the primitive recursive functions as those built up from basic functions by composition and primitive recursion. In other words a member \(\langle f,p\rangle\) of \({\mathcal PR}\) consists of a function \(f\) and a proof \(p\) that \(f\) admits a primitive recursive representation. Similarly, the set of polynomial time computable functions would be given as the type \[ {\mathcal P} = \Sigma f{:}{\mathbb N}\rightarrow{\mathbb N} . \text{Poly}(f), \] where the inductively defined predicate \(\text{Poly}(f)\) asserts that \(f\) is definable in Bellantoni-Cook's function algebra for polynomial time. The main technical result of the paper (Theorem 3) says that if \(f\) is a polynomial time function then we can find a member \(\langle f',p\rangle\) of \({\mathcal P}\) such that if \(n\in {\mathbb N}\) and \(n':{\mathbb N}\) is the numeral in \(\Pi\mu\Sigma^+\) representing \(n\), then \(f'(n')\) can be evaluated to the numeral representing \(f(n)\) using the computation rules of \(\Pi\mu\Sigma^+\) in a polynomial (in the size of \(n\)) number of steps. Essentially, this says that counting the number of reduction steps in \(\Pi\mu\Sigma^+\) can serve as an adequate cost model at least as far as polynomial time is concerned. The conclusions section speculates on extensions of this idea to logic via functional interpretation.