This article is an orphan, as no other articles link to it. Please introduce links to this page from related articles; try the Find link tool for suggestions. (February 2023) |
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. ICC was developed in the 1990s and employs the techniques of proof theory, substructural logic, model theory and recursion theory to prove bounds on the expressive power of high-level formal languages. 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 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. Two examples follow.
Cons-free programs
Jones 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 lack of constructors limits the computational power of the language, so it is no wonder that it cannot decide all the decidable problems, but the interest in it for Implicit Computational Complexity lies in that it can decide exactly P, and this is independent of the execution time of the programs, that can be exponential. Interestingly, 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.
Function algebras with recursion on notation
Bellantoni and Cook 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: . 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:
- empty string: (a zero-ary function)
- projections: for each
- normal binary successors:
- bounded safe binary successors:
- binary predecessor:
- numerical predecessor:
- conditional:
- tally product: .
We can combine functions to form new ones using a composition scheme and a recursion scheme. Given , their predicative composition, is defined by Given , the predicative recursion on notation scheme defines a function by 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 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., to get x in function . 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.
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,...; as well as the classes of the hierarchy DTIME(O(n)), DSPACE(O(n)), DTIME(), DSPACE(),... For most classes, several alternative representations are known.
References
- "ICC'01 - Implicit Computational Complexity". www.dcs.ed.ac.uk. Retrieved 2023-08-06.
- "Implicit Computational Complexity". perso.ens-lyon.fr. Retrieved 2023-08-06.
- Girard, Jean-Yves; Scott, Philip; Andre, Scedrov (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.
- "No.033 Implicit Computational Complexity and Applications: Resource Control, Security, Real-Number Computation | SeminarsNII Shonan Meeting". NII Shonan Meeting. Retrieved 2023-08-06.
- "DICE 2014 – Developments in Implicit Computational Complexity". dice14.tcs.ifi.lmu.de. Retrieved 2023-08-06.
- 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.
- 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.
- Bellantoni, Stephen; Cook, Stephen (1992). "A new recursion-theoretic characterization of the polytime functions (Extended abstract)". Proceedings of the twenty-fourth annual ACM symposium on Theory of computing - STOC '92. pp. 283–293. doi:10.1145/129712.129740. ISBN 0897915119. S2CID 2215181.
- Kristiansen, Lars; Voda, Paul J. "Programming Languages Capturing Complexity Classes". Nordic Journal of Computing. 12 (2005): 89–115.