<p>The third approach mentioned in the linked paper refers to the framework of bounded applicative theories, which are subsystems of Feferman's theory of Explicit Mathematics just as Bounded Arithmetic theories are subsystems of Peano Arithmetic (or higher order extensions of it). These theories contain full lambda calculus (or combinatory logic rather) and therefore have terms denoting all computable functions. They also have a predicate $W$ denoting the set of binary words. The strength of a theory is mainly determined by what axioms about $W$ it contains. The way to characterize a complexity class $C$ by theory $T$ is the following:</p>

<ul>
<li>For a function $f$ there is a term $t_f$  such that $T$ proves $\forall x. W(x) \to W(t_f(x)) $ if and only if $f$  is in $C$. </li>
</ul>

<p>They originate from the work of Thomas Strahm, in particular the following papers:</p>

<p>Thomas Strahm. Theories with self-application and computational complexity, Information and Computation 185, 2003, pp. 263-297. <a href="http://dx.doi.org/10.1016/S0890-5401(03)00086-5">http://dx.doi.org/10.1016/S0890-5401(03)00086-5</a></p>

<p>Thomas Strahm. A proof-theoretic characterization of the basic feasible functionals, Theoretical Computer Science 329, 2004, pp. 159-176. <a href="http://dx.doi.org/10.1016/j.tcs.2004.08.009">http://dx.doi.org/10.1016/j.tcs.2004.08.009</a></p>

CC BY-SA 3.0
2011-11-18T14:55:24.083Z
2011-11-18T16:16:00.020Z
2011-11-18T16:16:00.020Z
Jan Johannsen
<p>I don’t really know whether it is representative of the area (due to my general unfamiliarity with it), but the work of Giorgi Japaridze on <a href="http://www.cis.upenn.edu/~giorgi/cl.html" rel="nofollow">computability logic</a> belongs to the second approach.</p>

CC BY-SA 3.0
2011-11-18T18:17:31.713Z
2011-11-18T18:17:31.713Z
Emil Jeřábek
<p>I think the first approach, the <em>bounded arithmetic</em> approach, is the most popular and well-studied approach. The name <em>bounded arithmetic</em> indicates the use of weak subsystems of Peano arithmetics, where  induction is restricted to formulas with bounded quantifiers.  I already summarized the main idea behind this approach in this <a href="https://cstheory.stackexchange.com/questions/3253/what-books-should-everyone-read/3414#3414">post</a>. An excellent recent reference on bounded arithmetic is the <a href="http://www.cs.toronto.edu/~sacook/homepage/book/" rel="nofollow noreferrer">book</a> by Cook and Nguyen, whose draft is freely available. </p>

<p>The second approach uses linear logic and its subsystem as mentioned by Kaveh, which I don't know much about. </p>

<p>I haven't heard of the third approach although I'm working on bounded arithmetic. But it sounds a bit strange to me since without some form of syntactic or logical restriction, how does then a theory characterize a complexity class?</p>

CC BY-SA 2.5
2011-01-31T17:45:45.870Z
2011-01-31T17:45:45.870Z
2017-04-13T12:32:28.743Z
Dai Le
<p>When reading the paper &quot;<a href="http://arxiv.org/abs/1101.5444" rel="noreferrer">An applicative theory for FPH</a>&quot; you can encounter the following passage:</p>
<blockquote>
<p>Considering theories which characterize classes of computational complexity, there are three different approaches:</p>
<ul>
<li>in one, the functions which can be defined within the theory are “automatically” within a certain complexity class. In such an account, the syntax has to be restricted to guarantee that one stays in the appropriate class. This results, in general, in the problem that certain definitions of functions do not work any longer, even if the function is in the complexity class under consideration.</li>
<li>In a second account, the underlying logic is restricted.</li>
<li>In the third account, one does not restrict the syntax, allowing, in general, to write down “function terms” for arbitrary (partial recursive) functions, nor the logic, but only for those function terms which belong to the complexity class under consideration, one can prove that they have a certain characteristic property, usually, the property that they are “provably total”. While the function terms, according to the underlying syntactical framework, may
have a straightforward computational character, i.e., as <span class="math-container">$\lambda$</span> terms, the logic which is used to prove the characteristic property may well be classical.</li>
</ul>
</blockquote>
<p>My question concerns references which can be as an introduction to the three above-mentioned approaches. In this passage we see just characterizations for approaches, but do these have any generally accepted names?</p>

CC BY-SA 2.5
2011-01-31T14:25:28.350Z
The fundamental question of computational complexity is finding a theory that characterizes efficient computing?
Mohammad Al-Turkistany
CC BY-SA 2.5
2011-01-31T14:34:53.500Z
You can reader about the first approach, which is the main approach I think, in the recent book by Cook and Nguyen: http://www.cs.toronto.edu/~sacook/homepage/book/ . I haven't seen the third approach (from my limited experience), and I need time to understand what the second approach means.
Dai Le
CC BY-SA 2.5
2011-01-31T14:38:37.407Z
@Dai Le: Thank you for the comment. How about the name for this approach? Proof complexity?
Oleksandr Bondarenko
CC BY-SA 2.5
2011-01-31T14:42:46.577Z
@Oleksandr: I think that's the "bounded arithmetic" approach. This approach is very well-studied and elegant. Cook-Nguyen book also has pointers to other sources. I wrote a bit about it here: http://cstheory.stackexchange.com/questions/3253/what-books-should-everyone-read/3414#3414
Dai Le
CC BY-SA 2.5
2011-01-31T15:11:54.977Z
Dai has answered the first approach, the second approach uses non-classical logics like Girard's linear logic and its subsystems to capture complexity classes. It is related to implicit complexity and type theory (e.g. Godel's system T, ...). I don't understand the third one, reading the article may give a clue as it should cite some references for each of these approaches.
Kaveh
CC BY-SA 2.5
2011-01-31T17:10:20.740Z
@Dai make the comment an answer ?
Suresh Venkat
CC BY-SA 2.5
2011-02-01T06:13:07.403Z
is the second approach just called descriptive complexity? Or am I confused?
Artem Kaznatcheev
CC BY-SA 2.5
2011-02-01T09:26:40.853Z
The third is pretty much what we do every day when we put an algorithm given in any pseudocode in complexity classes, is it not?
Raphael
CC BY-SA 2.5
2011-02-02T05:42:10.990Z
@Artem: All approaches mentioned here are proof-theoretic, where the goal is to study what can be proven from a given theory (i.e., reasoning power of a theory). In constrast, descriptive complexity is model-theoretic, where we're a given a logical language, and we want to know what properties can be defined/expressed using this logical language (i.e., definability of a logical language).
Dai Le
<cc.complexity-theory><reference-request><complexity-classes><lo.logic><proof-complexity>
Theories which characterize classes of computational complexity
Oleksandr Bondarenko
# Theories which characterize classes of computational complexity

(Asked by: username_0 on 2011-01-31)

When reading the paper "[An applicative theory for FPH](http://arxiv.org/abs/1101.5444)" you can encounter the following passage:

> Considering theories which characterize classes of computational complexity, there are three different approaches:
>
> * in one, the functions which can be defined within the theory are “automatically” within a certain complexity class. In such an account, the syntax has to be restricted to guarantee that one stays in the appropriate class. This results, in general, in the problem that certain definitions of functions do not work any longer, even if the function is in the complexity class under consideration.
> * In a second account, the underlying logic is restricted.
> * In the third account, one does not restrict the syntax, allowing, in general, to write down “function terms” for arbitrary (partial recursive) functions, nor the logic, but only for those function terms which belong to the complexity class under consideration, one can prove that they have a certain characteristic property, usually, the property that they are “provably total”. While the function terms, according to the underlying syntactical framework, may
>   have a straightforward computational character, i.e., as $\lambda$ terms, the logic which is used to prove the characteristic property may well be classical.

My question concerns references which can be as an introduction to the three above-mentioned approaches. In this passage we see just characterizations for approaches, but do these have any generally accepted names?

**Tags:** cc.complexity-theory, reference-request, complexity-classes, lo.logic, proof-complexity

> **Comments:**
> **username_1**: The fundamental question of computational complexity is finding a theory that characterizes efficient computing?  
> **username_2**: You can reader about the first approach, which is the main approach I think, in the recent book by Cook and Nguyen: http://www.cs.toronto.edu/~sacook/homepage/book/ . I haven't seen the third approach (from my limited experience), and I need time to understand what the second approach means.  
> **username_0**: @username_2: Thank you for the comment. How about the name for this approach? Proof complexity?  
> **username_2**: @Oleksandr: I think that's the "bounded arithmetic" approach. This approach is very well-studied and elegant. Cook-Nguyen book also has pointers to other sources. I wrote a bit about it here: http://cstheory.stackexchange.com/questions/3253/what-books-should-everyone-read/3414#3414  
> **username_3**: Dai has answered the first approach, the second approach uses non-classical logics like Girard's linear logic and its subsystems to capture complexity classes. It is related to implicit complexity and type theory (e.g. Godel's system T, ...). I don't understand the third one, reading the article may give a clue as it should cite some references for each of these approaches.  
> **username_4**: @Dai make the comment an answer ?  
> **username_5**: is the second approach just called descriptive complexity? Or am I confused?  
> **username_6**: The third is pretty much what we do every day when we put an algorithm given in any pseudocode in complexity classes, is it not?  
> **username_2**: @Artem: All approaches mentioned here are proof-theoretic, where the goal is to study what can be proven from a given theory (i.e., reasoning power of a theory). In constrast, descriptive complexity is model-theoretic, where we're a given a logical language, and we want to know what properties can be defined/expressed using this logical language (i.e., definability of a logical language).  

---

## 3 answers

### Answer by username_2 on 2011-01-31. Score: 15 | Accepted answer

I think the first approach, the *bounded arithmetic* approach, is the most popular and well-studied approach. The name *bounded arithmetic* indicates the use of weak subsystems of Peano arithmetics, where induction is restricted to formulas with bounded quantifiers. I already summarized the main idea behind this approach in this [post](https://cstheory.stackexchange.com/questions/3253/what-books-should-everyone-read/3414#3414). An excellent recent reference on bounded arithmetic is the [book](http://www.cs.toronto.edu/~sacook/homepage/book/) by Cook and Nguyen, whose draft is freely available.

The second approach uses linear logic and its subsystem as mentioned by username_3, which I don't know much about.

I haven't heard of the third approach although I'm working on bounded arithmetic. But it sounds a bit strange to me since without some form of syntactic or logical restriction, how does then a theory characterize a complexity class?


---

### Answer by username_7 on 2011-11-18. Score: 7

The third approach mentioned in the linked paper refers to the framework of bounded applicative theories, which are subsystems of Feferman's theory of Explicit Mathematics just as Bounded Arithmetic theories are subsystems of Peano Arithmetic (or higher order extensions of it). These theories contain full lambda calculus (or combinatory logic rather) and therefore have terms denoting all computable functions. They also have a predicate $W$ denoting the set of binary words. The strength of a theory is mainly determined by what axioms about $W$ it contains. The way to characterize a complexity class $C$ by theory $T$ is the following:

* For a function $f$ there is a term $t\_f$ such that $T$ proves $\forall x. W(x) \to W(t\_f(x)) $ if and only if $f$ is in $C$.

They originate from the work of Thomas Strahm, in particular the following papers:

Thomas Strahm. Theories with self-application and computational complexity, Information and Computation 185, 2003, pp. 263-297. <http://dx.doi.org/10.1016/S0890-5401(03)00086-5>

Thomas Strahm. A proof-theoretic characterization of the basic feasible functionals, Theoretical Computer Science 329, 2004, pp. 159-176. <http://dx.doi.org/10.1016/j.tcs.2004.08.009>


---

### Answer by username_8 on 2011-11-18. Score: 3

I don’t really know whether it is representative of the area (due to my general unfamiliarity with it), but the work of Giorgi Japaridze on [computability logic](http://www.cis.upenn.edu/~giorgi/cl.html) belongs to the second approach.


---

