Théories qui caractérisent les classes de complexité informatique

15

En lisant l'article " Une théorie applicative pour la FPH ", vous pouvez rencontrer le passage suivant:

Compte tenu des théories qui caractérisent les classes de complexité informatique, il existe trois approches différentes:

  • dans l'un, les fonctions qui peuvent être définies dans la théorie sont «automatiquement» dans une certaine classe de complexité. Dans un tel compte, la syntaxe doit être restreinte pour garantir que l'on reste dans la classe appropriée. Cela se traduit, en général, par le problème que certaines définitions de fonctions ne fonctionnent plus, même si la fonction est dans la classe de complexité considérée.
  • Dans un deuxième compte, la logique sous-jacente est restreinte.
  • Dans le troisième récit, on ne restreint pas la syntaxe, permettant, en général, d'écrire des «termes de fonction» pour des fonctions arbitraires (récursives partielles), ni la logique, mais uniquement pour les termes de fonction qui appartiennent à la classe de complexité considérée. , on peut prouver qu'ils ont une certaine propriété caractéristique, généralement, la propriété qu'ils sont «prouvablement totaux». Alors que les termes de fonction, selon le cadre syntaxique sous-jacent, peuvent avoir un caractère de calcul simple, c'est-à-dire en tant que termes , la logique qui est utilisée pour prouver la propriété caractéristique peut bien être classique.λ

Ma question concerne les références qui peuvent être une introduction aux trois approches susmentionnées. Dans ce passage, nous ne voyons que des caractérisations d'approches, mais celles-ci ont-elles des noms généralement acceptés?

Oleksandr Bondarenko
la source
La question fondamentale de la complexité de calcul est de trouver une théorie qui caractérise un calcul efficace?
Mohammad Al-Turkistany
4
Vous pouvez lire sur la première approche, qui est l'approche principale, je pense, dans le livre récent de Cook et Nguyen: cs.toronto.edu/~sacook/homepage/book . Je n'ai pas vu la troisième approche (de mon expérience limitée), et j'ai besoin de temps pour comprendre ce que signifie la deuxième approche.
Dai Le
@Dai Le: Merci pour le commentaire. Que diriez-vous du nom de cette approche? Complexité de la preuve?
Oleksandr Bondarenko
2
@Oleksandr: Je pense que c'est l'approche "arithmétique bornée". Cette approche est très bien étudiée et élégante. Le livre de Cook-Nguyen contient également des pointeurs vers d'autres sources. J'en ai écrit un peu ici: cstheory.stackexchange.com/questions/3253/…
Dai Le
2
@Dai faire du commentaire une réponse?
Suresh Venkat

Réponses:

15

Je pense que la première approche, l' approche arithmétique bornée , est l'approche la plus populaire et la mieux étudiée. Le nom arithmétique borné indique l'utilisation de sous-systèmes faibles de l'arithmétique Peano, où l'induction est limitée aux formules avec des quantificateurs bornés. J'ai déjà résumé l'idée principale derrière cette approche dans ce post . Une excellente référence récente sur l'arithmétique bornée est le livre de Cook et Nguyen, dont le projet est disponible gratuitement.

La deuxième approche utilise la logique linéaire et son sous-système comme mentionné par Kaveh, que je ne connais pas beaucoup.

Je n'ai pas entendu parler de la troisième approche bien que je travaille sur l'arithmétique bornée. Mais cela me semble un peu étrange car sans aucune forme de restriction syntaxique ou logique, comment une théorie caractérise-t-elle alors une classe de complexité?

Dai Le
la source
7

WWCT

  • FtFTX.W(X)W(tF(X))FC

Ils proviennent des travaux de Thomas Strahm, en particulier des articles suivants:

Thomas Strahm. Théories avec auto-application et complexité de calcul, Information and Computation 185, 2003, pp. 263-297. http://dx.doi.org/10.1016/S0890-5401(03)00086-5

Thomas Strahm. Une caractérisation de preuve-théorique des fonctions de base réalisables, Théorie Informatique 329, 2004, pp. 159-176. http://dx.doi.org/10.1016/j.tcs.2004.08.009

Jan Johannsen
la source
3

Je ne sais pas vraiment s'il est représentatif de la zone (en raison de ma méconnaissance générale de celui-ci), mais le travail de Giorgi Japaridze sur la logique de calculabilité appartient à la deuxième approche.

Emil Jeřábek soutient Monica
la source