Theorien, die Klassen rechnerischer Komplexität charakterisieren

Beim Lesen der Abhandlung " Eine anwendungsbezogene Theorie für FPH " können Sie folgende Passage finden:

In Anbetracht der Theorien, die Klassen von Rechenkomplexität charakterisieren, gibt es drei verschiedene Ansätze:

• in einem Fall sind die Funktionen, die innerhalb der Theorie definiert werden können, innerhalb einer bestimmten Komplexitätsklasse "automatisch". In einem solchen Konto muss die Syntax eingeschränkt werden, um sicherzustellen, dass man in der entsprechenden Klasse bleibt. Dies führt im Allgemeinen zu dem Problem, dass bestimmte Definitionen von Funktionen nicht mehr funktionieren, selbst wenn sich die Funktion in der betrachteten Komplexitätsklasse befindet.
• In einem zweiten Konto ist die zugrunde liegende Logik eingeschränkt.
• Im dritten Konto wird die Syntax nicht eingeschränkt, so dass im Allgemeinen „Funktionsbegriffe“ für beliebige (teilweise rekursive) Funktionen oder die Logik, sondern nur für diejenigen Funktionsbegriffe, die zu der betrachteten Komplexitätsklasse gehören, niedergeschrieben werden können kann man nachweisen, dass sie eine bestimmte charakteristische Eigenschaft haben, in der Regel die Eigenschaft, dass sie „nachweislich vollständig“ sind. Während die Funktionsterme nach dem zugrunde liegenden syntaktischen Rahmen einen einfachen Berechnungscharakter haben können, dh als Terme, kann die Logik, die zum Nachweis der charakteristischen Eigenschaft verwendet wird, durchaus klassisch sein.$\lambda$

Meine Frage betrifft Referenzen, die als Einführung in die drei oben genannten Ansätze dienen können. In dieser Passage sehen wir nur Charakterisierungen für Ansätze, aber haben diese allgemein akzeptierte Namen?

Ich denke, der erste Ansatz, der beschränkte arithmetische Ansatz, ist der populärste und am besten untersuchte Ansatz. Die namensgebundene Arithmetik weist auf die Verwendung von schwachen Teilsystemen der Peano-Arithmetik hin, bei denen die Induktion auf Formeln mit begrenzten Quantifizierern beschränkt ist. Die Grundidee dieses Ansatzes habe ich bereits in diesem Beitrag zusammengefasst . Eine ausgezeichnete Referenz zur beschränkten Arithmetik in letzter Zeit ist das Buch von Cook und Nguyen, dessen Entwurf frei verfügbar ist.

Der zweite Ansatz verwendet die von Kaveh erwähnte lineare Logik und ihr Subsystem, über die ich nicht viel weiß.

Ich habe noch nichts von dem dritten Ansatz gehört, obwohl ich mich mit beschränkter Arithmetik beschäftige. Aber es klingt für mich etwas seltsam, denn wie charakterisiert eine Theorie ohne irgendeine syntaktische oder logische Einschränkung eine Komplexitätsklasse?

$W$$W$$C$$T$

• $f$$t_f$$T$$\forall x. W(x) \to W(t_f(x))$$f$$C$

Sie stammen aus der Arbeit von Thomas Strahm, insbesondere aus folgenden Arbeiten:

Thomas Strahm. Theorien mit Selbstanwendung und rechnerischer Komplexität, Information and Computation 185, 2003, S. 263-297. http://dx.doi.org/10.1016/S0890-5401(03)00086-5

Thomas Strahm. Eine beweistheoretische Charakterisierung der realisierbaren Grundfunktionen, Theoretical Computer Science 329, 2004, S. 159-176. http://dx.doi.org/10.1016/j.tcs.2004.08.009

Ich weiß nicht genau, ob es für das Gebiet repräsentativ ist (aufgrund meiner allgemeinen Unkenntnis), aber die Arbeit von Giorgi Japaridze zur Berechnungslogik gehört zum zweiten Ansatz.