Implicit computational complexity

Cons-free programs

Jones^[7][12] defined a programming language that can solve decision problems where the input is a binary string, and showed that a problem can be decided in this language if and only if it is in P. The language can be briefly described as follows. It receives the input as a list of bits. It has variables that can point to the list and change by application of the "tail" operation so they can move forward on the list. It can define recursive functions, but has no Higher-order functions. Crucially, it has no data-type constructors (hence the name cons-free): the input list is the one and only data structure throughout the program. The absence of constructors limits expressive power, preventing the construction of auxiliary data structures whose size could grow during computation. Remarkably, this restriction does not reduce the class of decidable problems to a proper subset of P: every problem in P can be decided within the language. Moreover, programs in the language may run in exponential time yet decide only polynomial-time problems, so the implicit characterisation is independent of the actual execution time of individual programs. Jones has also shown that if non-determinism is added to the language (as in a Nondeterministic Turing machine), the class of problems that can be accepted is still P.^[12]

Function algebras with recursion on notation

Bellantoni and Cook^[6] showed that a certain class of functions coincides with FP. These are functions which are defined, like the primitive recursive functions, by a set of base functions and operators for constructing new functions from existing ones. A special recursion scheme is used instead of the primitive recursion scheme, as will be seen below, and in addition, the functions have their arguments partitioned in two "sorts". This is denoted by separating arguments by a semicolon: ${\displaystyle f(x_{1},\dots ,x_{k};x_{k+1},\dots ,x_{k+n})}$. The arguments following the semicolon are called safe (a more intuitive name might be "protected"). When a value is passed in a safe position, it is not allowed to grow too much — note the difference between clauses (3) and (4) below. Another important difference to the definition of primitive recursive functions is that here the arguments are considered as binary strings and we can increase a value by adding a bit (x0 or x1) in contrast to the numeric successor function (x’).

Here is the list of basic functions:

We can combine functions to form new ones using a composition scheme and a recursion scheme. Given ${\displaystyle g,{\vec {r}},{\vec {s}}}$, their predicative composition, ${\displaystyle f=g\circ ({\vec {r}};{\vec {s}})}$ is defined by $${\displaystyle f({\vec {x}};{\vec {y}})=g({\vec {r}}({\vec {x}};);{\vec {s}}({\vec {x}};{\vec {y}})).}$$ Given ${\displaystyle g,h_{0},h_{1}}$, the predicative recursion on notation scheme defines a function ${\displaystyle f}$ by $${\displaystyle {\begin{aligned}f(\varepsilon ,{\vec {x}};{\vec {y}})&=g({\vec {x}};{\vec {y}}),\\f(zi,{\vec {x}};{\vec {y}})&=h_{i}(z,{\vec {x}};{\vec {y}},f(z,{\vec {x}};{\vec {y}})).\end{aligned}}}$$ 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 z to z-1.

Example. We define a function ${\displaystyle r(x)}$ that receives a binary string x and returns a string of 0s of the same length as x. For readability we omit invocations of the projection functions which are technically necessary to retrieve function argument, e.g., ${\displaystyle \pi _{1}^{1}(x)}$ to get x in function ${\displaystyle g(x)}$. $${\displaystyle {\begin{aligned}g(x)&=f(x,x),{\text{where}}\\f(\varepsilon ,x;)&=\varepsilon ,\\f(zi,x;)&=S_{0}(x;f(z,x;)).\end{aligned}}}$$ Note how we need to initially keep a copy of x in order to be able to apply the bounded binary successor operator in the recursion.

Tiered recursion

Leivant^[10] developed an alternative approach based on ‘‘data tiering’’: natural numbers (or other data) are stratified into tiers, and recursion is permitted only in ways that respect the tier order. Functions definable with tier-bounded recursion coincide with polynomial-time computable functions. Leivant’s framework is more syntactically flexible than the Bellantoni–Cook algebra and extends naturally to imperative languages.

Linear logic approaches

Girard, Scedrov, and Scott^[4] introduced bounded linear logic, a variant of linear logic in which the use of the contraction rule is bounded by polynomial terms. Proofs in this system correspond, via the Curry–Howard correspondence, to polynomial-time computable functions. Subsequent work on light linear logic by Girard^[13] and its type-theoretic development by Baillot and Terui,^[14] and Lafont’s soft linear logic,^[15] gave related systems with cleaner proof theory, all characterising polynomial-time computation via structural constraints on the exponential modality.​​​​​​​​​​​​​​​