15
$\begingroup$

When reading the paper "An applicative theory for FPH" 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?

Improve this question
$\endgroup$
9
  • $\begingroup$ The fundamental question of computational complexity is finding a theory that characterizes efficient computing? $\endgroup$ – Mohammad Al-Turkistany Jan 31 '11 at 14:25
  • 4
    $\begingroup$ You can reader about the first approach, which is the main approach I think, in the recent book by Cook and Nguyen: 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. $\endgroup$ – Dai Le Jan 31 '11 at 14:34
  • $\begingroup$ @Dai Le: Thank you for the comment. How about the name for this approach? Proof complexity? $\endgroup$ – Oleksandr Bondarenko Jan 31 '11 at 14:38
  • 2
    $\begingroup$ @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: cstheory.stackexchange.com/questions/3253/… $\endgroup$ – Dai Le Jan 31 '11 at 14:42
  • 2
    $\begingroup$ @Dai make the comment an answer ? $\endgroup$ – Suresh Venkat Jan 31 '11 at 17:10
15
$\begingroup$

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. An excellent recent reference on bounded arithmetic is the book by Cook and Nguyen, whose draft is freely available.

The second approach uses linear logic and its subsystem as mentioned by Kaveh, 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?

Improve this answer
$\endgroup$
7
$\begingroup$

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

Improve this answer
$\endgroup$
3
$\begingroup$

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 belongs to the second approach.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.