Theories which characterize classes of computational complexity

Question

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?

Answer 1

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?

Answer 2

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