A note on complexity measures for inductive classes in constructive type theory (Q1271558): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1006/inco.1998.9999 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1978042238 / rank | |||
Normal rank |
Revision as of 18:28, 19 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A note on complexity measures for inductive classes in constructive type theory |
scientific article |
Statements
A note on complexity measures for inductive classes in constructive type theory (English)
0 references
6 July 1999
0 references
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.
0 references
constructive type theory
0 references
polynomial time complexity
0 references
computational complexity
0 references
recursive functions
0 references
computable functions
0 references