Teorias que caracterizam classes de complexidade computacional

Ao ler o artigo " Uma teoria aplicada à FPH ", você pode encontrar a seguinte passagem:

Considerando as teorias que caracterizam classes de complexidade computacional, existem três abordagens diferentes:

• em um, as funções que podem ser definidas na teoria estão "automaticamente" dentro de uma certa classe de complexidade. Nessa conta, a sintaxe deve ser restrita para garantir que alguém permaneça na classe apropriada. Isso resulta, em geral, no problema de que certas definições de funções não funcionam mais, mesmo se a função estiver na classe de complexidade em consideração.
• Em uma segunda conta, a lógica subjacente é restrita.
• Na terceira conta, não se restringe a sintaxe, permitindo, em geral, anotar “termos de função” para funções arbitrárias (recursivas parciais), nem a lógica, mas apenas para os termos de função que pertencem à classe de complexidade em consideração , pode-se provar que eles têm uma certa propriedade característica, geralmente a propriedade que eles são "provadamente totais". Enquanto os termos da função, de acordo com a estrutura sintática subjacente, podem ter um caráter computacional direto, ou seja, como termos , a lógica usada para provar a propriedade da característica pode muito bem ser clássica.$\lambda$

Minha pergunta diz respeito a referências que podem ser uma introdução às três abordagens acima mencionadas. Nesta passagem, vemos apenas caracterizações para abordagens, mas elas têm nomes geralmente aceitos?

Eu acho que a primeira abordagem, a abordagem aritmética limitada , é a abordagem mais popular e bem estudada. O nome aritmética limitada indica o uso de subsistemas fracos da aritmética Peano, onde a indução é restrita a fórmulas com quantificadores limitados. Eu já resumi a idéia principal por trás dessa abordagem neste post . Uma excelente referência recente sobre aritmética limitada é o livro de Cook e Nguyen, cujo rascunho está disponível gratuitamente.

A segunda abordagem usa a lógica linear e seu subsistema, como mencionado por Kaveh, sobre o qual eu não sei muito.

Não ouvi falar da terceira abordagem, embora esteja trabalhando em aritmética limitada. Mas me parece um pouco estranho, pois, sem alguma forma de restrição sintática ou lógica, como então uma teoria caracteriza uma classe de complexidade?

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

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

Eles se originam do trabalho de Thomas Strahm, em particular os seguintes documentos:

Thomas Strahm. Teorias com auto-aplicação e complexidade computacional, Information and Computation 185, 2003, pp. 263-297. http://dx.doi.org/10.1016/S0890-5401(03)00086-5

Thomas Strahm. Uma caracterização teórica da prova dos funcionais básicos viáveis, Teoria da Computação 329, 2004, pp. 159-176. http://dx.doi.org/10.1016/j.tcs.2004.08.009

Realmente não sei se é representativo da área (devido ao meu desconhecimento geral), mas o trabalho de Giorgi Japaridze sobre lógica da computabilidade pertence à segunda abordagem.