Implicit computational complexity

Implicit computational complexity (ICC) is a subfield of computational complexity theory that characterizes programs by constraints on the way in which they are constructed, without reference to a specific underlying machine model or to explicit bounds on computational resources unlike conventional complexity theory. The central goal of ICC is to identify programming formalisms — such as restricted formal languages, type systems, or recursion schemes — whose expressive power coincides exactly with a given complexity class, so that membership in the class becomes a consequence of syntactic well-formedness rather than a separate computational argument. ICC was developed in the 1990s and employs the techniques of proof theory, substructural logic, linear logic, model theory and recursion theory to prove bounds on the expressive power of high-level formal languages. Among its founding contributions are Girard, Scedrov, and Scott’s bounded linear logic (1992), Bellantoni and Cook’s function algebra based on predicative recursion (1992), and Jones’s cons-free programming language characterisation of polynomial time (1999). ICC is also concerned with the practical realization of functional programming languages, language tools and type theory that can control the resource usage of programs in a formally verifiable sense.…

Implicit computational complexity (ICC) is a subfield of computational complexity theory that characterizes programs by constraints on the way in which they are constructed, without reference to a specific underlying machine model or to explicit bounds on computational resources unlike conventional complexity theory. The central goal of ICC is to identify programming formalisms — such as restricted formal languages, type systems, or recursion schemes — whose expressive power coincides exactly with a given complexity class, so that membership in the class becomes a consequence of syntactic well-formedness rather than a separate computational argument. ICC was developed in the 1990s and employs the techniques of proof theory, substructural logic, linear logic, model theory and recursion theory to prove bounds on the expressive power of high-level formal languages. Among its founding contributions are Girard, Scedrov, and Scott’s bounded linear logic (1992), Bellantoni and Cook’s function algebra based on predicative recursion (1992), and Jones’s cons-free programming language characterisation of polynomial time (1999). ICC is also concerned with the practical realization of functional programming languages, language tools and type theory that can control the resource usage of programs in a formally verifiable sense. Two leading approaches to resource certification have been Static Analysis (SA) and Implicit Computational Complexity (ICC). SA is algorithmic in nature: it focuses on a broad programming language of choice, and seeks to determine by syntactic means whether given programs in that language are feasible. In contrast, ICC attempts to create from the outset specialized programming languages or methods that delineate a complexity class. Thus, SA's focus is on compile time, making no demand on the programmer; whereas ICC is a language-design discipline. {{ordered list|start=1 |1= empty string: \varepsilon (a zero-ary function) |2= projections: \pi_i^{k,n}(x_1, \ldots, x_k; x_{k+1}, \ldots, x_{k+n}) = x_i, for each 1 \le i \le k+n |3= normal binary successors: S_i(x;) = x i , \ i \in \{ 0, 1 \} |4= bounded safe binary successors: S_i(z; x) = \left\{\begin{array}{ll} xi & \text{if }|x| |5= binary predecessor: P(;\varepsilon) = \varepsilon, P(;x i) = x |6= numerical predecessor: p(;\varepsilon) = \varepsilon,\ p(;x') = x |7= conditional: Q(;\varepsilon, y, z_0, z_1) = y, Q(;x i, y, z_0, z_1) = z_i |8= tally product: \times(x, y;) = 1^ . }} We can combine functions to form new ones using a composition scheme and a recursion scheme. Given g, \vec r, \vec s , their predicative composition, f = g\circ(\vec r; \vec s) is defined by f(\vec x; \vec y) = g(\vec r(\vec x;); \vec s(\vec x; \vec y)). Given g, h_0, h_1 , the predicative recursion on notation scheme defines a function f by \begin{align} f(\varepsilon, \vec x; \vec y) &= g(\vec x; \vec y),\\ f(z i, \vec x; \vec y) &= h_i(z, \vec x; \vec y, f(z, \vec x; \vec y)). \end{align} It is called "recursion on notation", because in each recursive call we strip a bit of the recursion argument, in contrast with recursion "on value" which goes from to -1. Example. We define a function r(x) that receives a binary string and returns a string of 0s of the same length as . For readability we omit invocations of the projection functions which are technically necessary to retrieve function argument, e.g., \pi^1_1(x) to get in function g(x) . \begin{align} g(x) &= f(x,x), \text{where}\\ f(\varepsilon, x; ) &= \varepsilon,\\ f(z i, x; ) &= S_0(x; f(z, x;)). \end{align} Note how we need to initially keep a copy of in order to be able to apply the bounded binary successor operator in the recursion. ==Notes== ==References== ==External links==

Text derived from https://en.wikipedia.org/w/index.php?oldid=1374587013 under CC BY-SA 4.0; modifications have been made.