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.[1][2][3] 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.[4][5] Among its founding contributions are Girard, Scedrov, and Scott’s bounded linear logic (1992),[4] Bellantoni and Cook’s function algebra based on predicative recursion (1992),[6] and Jones’s cons-free programming language characterisation of polynomial time (1999).[7] 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.[8][9]

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.[10]

## Contents

* 1 Background and motivation
* 2 Implicit Representations of polynomial time
* 2.1 Cons-free programs
* 2.2 Function algebras with recursion on notation
* 2.3 Tiered recursion
* 2.4 Linear logic approaches
* 3 Other Classes
* 4 Applications
* 5 See also
* 6 Notes
* 7 References
* 8 External links

## Background and motivation

In classical complexity theory, a problem is assigned to a complexity class — such as P or PSPACE — by analysing the resource consumption (time, space) of a Turing machine that solves it. This analysis is extrinsic: the program and its complexity bound are separate objects, and the bound must be verified independently.

ICC seeks intrinsic characterisations: programming languages or logical systems in which every well-formed program is, by construction, feasible, and in which every feasible algorithm can be expressed. Such characterisations are of theoretical interest because they reveal the combinatorial or logical reasons why a complexity class has the extent it does, and of practical interest because they can serve as the foundation for type systems and program analysis tools that enforce resource bounds statically.

The field draws heavily on linear logic, introduced by Girard (1987),[11] in which the structural rules of weakening and contraction are controlled. Restricting these rules limits the ability of a program to duplicate or discard data, which in turn bounds the computational resources the program can consume.

## Implicit Representations of polynomial time

The important complexity classes of polynomial-time decidable sets (the class P) and polynomial-time computable functions (FP) have received much attention and possess several implicit representations.

### 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: f(x1,…,xk;xk+1,…,xk+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:

1. empty string: ε (a zero-ary function)
2. projections: πik,n(x1,…,xk;xk+1,…,xk+n)=xi, for each 1≤i≤k+n
3. normal binary successors: Si(x;)=xi, i∈{0,1}
4. bounded safe binary successors: Si(z;x)={xiif |x|<|z|xotherwise
5. binary predecessor: P(;ε)=ε,P(;xi)=x
6. numerical predecessor: p(;ε)=ε, p(;x′)=x
7. conditional: Q(;ε,y,z0,z1)=y,Q(;xi,y,z0,z1)=zi
8. tally product: ×(x,y;)=1|x|×|y|.

We can combine functions to form new ones using a composition scheme and a recursion scheme. Given g,r→,s→, their predicative composition, f=g∘(r→;s→) is defined by f(x→;y→)=g(r→(x→;);s→(x→;y→)). Given g,h0,h1, the predicative recursion on notation scheme defines a function f by f(ε,x→;y→)=g(x→;y→),f(zi,x→;y→)=hi(z,x→;y→,f(z,x→;y→)). 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 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., π11(x) to get x in function g(x). g(x)=f(x,x),wheref(ε,x;)=ε,f(zi,x;)=S0(x;f(z,x;)). 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.

## Other Classes

Implicit representations have been found for many complexity classes, including the hierarchy of time classes P, EXPTIME, 2-EXPTIME,… and the space classes L, PSPACE, EXPSPACE,…;[12] as well as the classes of the hierarchy DTIME(O(n)), DSPACE(O(n)), DTIME(O(2n)), DSPACE(O(2n)),…[16] For most classes, several alternative representations are known, which suggests that the classes have robust intrinsic descriptions rather than being artefacts of a single formalism.

The Grzegorczyk hierarchy of elementary and primitive recursive functions has also been studied from an ICC perspective: the hierarchy levels correspond to restrictions on the nesting depth of bounded recursion schemes.[17][18]

## Applications

ICC results have been applied in several practical directions:

* Type-based resource analysis. Type systems inspired by light and soft linear logic have been implemented in functional languages to certify that well-typed programs run in polynomial time or in polynomial space.[9]
* Implicit complexity of real-number computation. ICC methods have been extended to characterise feasible computation over the real numbers, going beyond the discrete setting.[5]
* Security and information flow. The resource-bounding properties of ICC type systems have been adapted to control information flow in programs, with applications to language-based security.[19]

## See also

* Formal verification
* Linear logic
* Primitive recursive function
* Semantics (computer science)
* Static program analysis
* Type theory

## Notes

1. ↑ Dal Lago 2012.
2. ↑ University of Edinburgh 2001.
3. ↑ École normale supérieure de Lyon 2017.
4. ↑ 4.0 4.1 4.2 Girard, Scedrov & Scott 1992.
5. ↑ 5.0 5.1 National Institute of Informatics 2013.
6. ↑ 6.0 6.1 Bellantoni & Cook 1992.
7. ↑ 7.0 7.1 Jones 1999.
8. ↑ DICE 2014.
9. ↑ 9.0 9.1 Aubert et al. 2022.
10. ↑ 10.0 10.1 Leivant 2020.
11. ↑ Girard 1987.
12. ↑ 12.0 12.1 12.2 Jones 2001.
13. ↑ Girard 1998.
14. ↑ Baillot & Terui 2004.
15. ↑ Lafont 2004.
16. ↑ Kristiansen & Voda 2005.
17. ↑ Rose 1984.
18. ↑ Clote 1999.
19. ↑ Marion 2011.

## References

* Aubert, Clément; Rubiano, Thomas; Rusch, Neea; Seiller, Thomas (2022). "Realizing Implicit Computational Complexity". 7th International Conference on Formal Structures for Computation and Deduction, (FSCD) 2022. LIPIcs 228: 26:1–26:33. https://drops.dagstuhl.de/storage/00lipics/lipics-vol228-fscd2022/LIPIcs.FSCD.2022.26/LIPIcs.FSCD.2022.26.pdf.

* Baillot, Patrick; Terui, Kazushige (2004). "Light types for polynomial time computation in lambda-calculus". Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004). IEEE Computer Society Press. pp. 266–275. doi:10.1109/LICS.2004.1319621.

* Bellantoni, Stephen; Cook, Stephen (1992). "A new recursion-theoretic characterization of the polytime functions". Computational Complexity 2 (2): 97–110. doi:10.1007/BF01201998.

* Clote, Peter (1999). "Computation models and function algebras". in Griffor, Edward R.. Handbook of Computability Theory. Studies in Logic and the Foundations of Mathematics. 140. Amsterdam: North-Holland. pp. 589–681. ISBN 978-0-444-89882-1.

* Dal Lago, Ugo (2012). "A Short Introduction to Implicit Computational Complexity". in Bezhanishvili, N.; Goranko, V.. Lecture Notes in Computer Science (LNCS). 7388. Berlin, Heidelberg: Springer. pp. 89–109. doi:10.1007/978-3-642-31485-8_3. ISBN 978-3-642-31485-8. http://cs.unibo.it/~dallago/FICQRA/esslli.pdf. Retrieved 2026-04-22.

* DICE (2014). "DICE 2014 – Developments in Implicit Computational Complexity". https://dice14.tcs.ifi.lmu.de/.

* École normale supérieure de Lyon (2017). "Implicit Computational Complexity". https://perso.ens-lyon.fr/olivier.laurent/cours/cr-icc.html.

* Girard, Jean-Yves (1987). "Linear logic". Theoretical Computer Science 50 (1): 1–102. doi:10.1016/0304-3975(87)90045-4. https://girard.perso.math.cnrs.fr/linear.pdf.

* Girard, Jean-Yves; Scedrov, Andre; Scott, Philip (1992). "Bounded linear logic: a modular approach to polynomial-time computability". Theoretical Computer Science 97 (1): 1-66. doi:10.1016/0304-3975(92)90386-T.

* Girard, Jean-Yves (1998). "Light linear logic". Information and Computation 143 (2): 175–204. doi:10.1006/inco.1998.2700.

* Jones, Neil D. (1999). "LOGSPACE and PTIME Characterized by Programming Languages". Theoretical Computer Science 228 (1–2): 151–174. doi:10.1016/S0304-3975(98)00357-0.

* Jones, Neil D. (2001). "The expressive power of higher-order types or, life without CONS". Journal of Functional Programming 11 (1): 55–94. doi:10.1017/S0956796800003889.

* Kristiansen, Lars; Voda, Paul J. (2005). "Programming Languages Capturing Complexity Classes". Nordic Journal of Computing 12: 89–115.

* Lafont, Yves (2004). "Soft linear logic and polynomial time". Theoretical Computer Science 318 (1–2): 163–180. doi:10.1016/j.tcs.2003.10.018.

* Leivant, Daniel (2020). "A Generic Imperative Language for Polynomial Time". arXiv:1911.04026 [cs.CC].

* Marion, Jean-Yves (2011). "A type system for complexity flow analysis". Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011). IEEE Computer Society Press. pp. 123–132. doi:10.1109/LICS.2011.41.

* National Institute of Informatics (2013). "No.033 Implicit Computational Complexity and Applications: Resource Control, Security, Real-Number Computation | SeminarsNII Shonan Meeting". https://shonan.nii.ac.jp/seminars/033/.

* Rose, H. E. (1984). Subrecursion: Functions and Hierarchies. Oxford Logic Guides. 9. Oxford: Clarendon Press. ISBN 0198531893.

* University of Edinburgh (2001). "ICC’01 - Implicit Computational Complexity". https://www.dcs.ed.ac.uk/home/mxh/ICC01.html.

## External links

* Rusch, Neea (2024-08-20). "Implicit Computational Complexity: From Theory to Practice". Augusta, Georgia (United States): Augusta University. https://nkrusch.github.io/posts/2024-aalto.

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Implicit computational complexity. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Implicit_computational_complexity&oldid=4414684"