A note on complexity measures for inductive classes in constructive type theory
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.
scientific article; zbMATH DE number 1220917
scientific article