Теории, которые характеризуют классы вычислительной сложности

Читая статью « Аппликативная теория для FPH », вы можете встретить следующий отрывок:

Рассматривая теории, которые характеризуют классы вычислительной сложности, существует три разных подхода:

• в одном функции, которые могут быть определены в рамках теории, «автоматически» находятся в определенном классе сложности. В такой учетной записи синтаксис должен быть ограничен, чтобы гарантировать, что он остается в соответствующем классе. Это приводит, как правило, к проблеме того, что некоторые определения функций больше не работают, даже если функция находится в рассматриваемом классе сложности.
• Во втором счете основная логика ограничена.
• В третьем случае никто не ограничивает синтаксис, позволяя, как правило, записывать «функциональные члены» для произвольных (частично рекурсивных) функций или логики, но только для тех функциональных элементов, которые принадлежат рассматриваемому классу сложности. Можно доказать, что они обладают определенным характерным свойством, обычно тем свойством, что они «доказуемо тотальны». Хотя функциональные термины, в соответствии с базовой синтаксической структурой, могут иметь простой вычислительный характер, т. качестве λ- терминов, логика, которая используется для доказательства характеристического свойства, вполне может быть классической.$\lambda$

Мой вопрос касается ссылок, которые могут послужить введением в три вышеупомянутых подхода. В этом отрывке мы видим только характеристики подходов, но имеют ли они общепринятые названия?

Я думаю, что первый подход, ограниченный арифметический подход, является наиболее популярным и хорошо изученным подходом. Имя ограничено арифметической указывает на использование слабых подсистем Пеано арифметике, где индукция ограничивается формул с ограниченными кванторами. Я уже изложил основную идею этого подхода в этом посте . Превосходной недавней ссылкой на ограниченную арифметику является книга Кука и Нгуена, черновик которой находится в свободном доступе.

Второй подход использует линейную логику и ее подсистему, как упомянуто Каве, о которой я мало что знаю.

Я не слышал о третьем подходе, хотя я работаю над ограниченной арифметикой. Но это звучит немного странно для меня, поскольку без какой-либо формы синтаксического или логического ограничения, как тогда теория характеризует класс сложности?

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

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

Они происходят от работы Томаса Страма, в частности, следующих работ:

Томас Страм. Теории с самоприменением и вычислительной сложностью, Информация и вычисления 185, 2003, с. 263-297. http://dx.doi.org/10.1016/S0890-5401(03)00086-5

Томас Страм. Теоретико-теоретическая характеристика основных выполнимых функционалов, Теоретическая информатика, 329, 2004, с. 159-176. http://dx.doi.org/10.1016/j.tcs.2004.08.009

Я действительно не знаю, является ли это представителем области (из-за моего общего незнакомого с ним), но работа Джорджа Джапаридзе по логике вычислимости относится ко второму подходу.