A note on complexity measures for inductive classes in constructive type theory
type: Item
instance of: scholarly article
title: A note on complexity measures for inductive classes in constructive type theory
zbMATH Open document ID: 0916.03039
author: Robert Constable
published in: Information and Computation
publication date: 1999-07-06T00:00:00Z
review text: 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\Sig…
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03D15
Mathematics Subject Classification ID: 68Q15
Mathematics Subject Classification ID: 03D20
zbMATH DE Number: 1220917
zbMATH Keywords: constructive type theory
zbMATH Keywords: polynomial time complexity
zbMATH Keywords: computational complexity
zbMATH Keywords: recursive functions
zbMATH Keywords: computable functions
describes a project that uses: ALF
describes a project that uses: TALx86
describes a project that uses: Automath
describes a project that uses: Coq
MaRDI profile type: Publication
full work available at URL: inco.1998.9999
OpenAlex ID: W1978042238
cites work: Explicit substitutions
cites work: Proofs as programs
cites work: A new recursion-theoretic characterization of the polytime functions
cites work: Q3800030
cites work: Q5586401
cites work: Q4062633
cites work: Q4793030
cites work: Q3702502
cites work: Q4035304
cites work: Q5610115
cites work: Q4012883
cites work: Q4128540
cites work: Bounded linear logic: A modular approach to polynomial-time computability
cites work: Recursive objects in all finite types
cites work: An Overview of the Theory of Computational Complexity
cites work: Q4162663
cites work: On the Computational Complexity of Algorithms
cites work: Languages that Capture Complexity Classes
cites work: ON STEPWISE EXPLICIT SUBSTITUTION
cites work: Q5812175
cites work: Optimality and inefficiency: what isn't a cost model of the lambda calculus?
cites work: A foundational delineation of poly-time
cites work: Q4501154
cites work: Q4850553
cites work: Q3688389
cites work: Classes of computable functions defined by bounds on computation
cites work: Polynomial and abstract subrecursive classes
cites work: Inductively defined types in the Calculus of Constructions
cites work: Classes of Predictably Computable Functions
cites work: Data Types as Lattices
cites work: Q4850556
cites work: The realm of primitive recursion
cites work: Partial Applicative Theories and Explicit Substitutions
cites work: A simple and powerful approach for studying constructivity, computability, and complexity
DOI: 10.1006/INCO.1998.9999
description: scientific article; zbMATH DE number 1220917