Estou menos interessado em idiomas em que você pode escrever quase tudo, mas depois é necessário escrever uma prova de que o que você escreveu termina.
Estou mais interessado no espaço de design de linguagens inerentemente confinadas a determinadas classes de complexidade por construção.
Existe algum tipo de hierarquia teórica para linguagens completas de turing?
Respostas:
Existem muitas classes de linguagens de programação em que todos os programas terminam. A forma mais comum de impor rescisão é por meio de tipos. A teoria mais bem desenvolvida dos sistemas de digitação para terminar a computação pode ser a do cubo Lambda de Barendregt, que decompõe a digitação em três eixos ortogonais:
A partir de idiomas de término, como o simplesmente digitadoλ -calculus , pode-se adicionar qualquer combinação desses três eixos e reter a terminação.
Isso tem conexões estreitas com a lógica, através da correspondência de Curry-Howard .
Existem muitas extensões e aprimoramentos, incluindo tipos que capturam classes de complexidade.
fonte
Após o trabalho fundamental de Bellantoni & Cook em Uma nova caracterização teórica da recursão das funções Polytime , houve muito trabalho em caracterizações simples de classes de complexidade por meio de linguagens totais, com fortes conexões com a lógica linear, como Martin Berger observa nos comentários.
Com base neste trabalho, outras classes de complexidade foram caracterizadas: Leivant e Marion deram caracterizações de PSPACE e ELEM (essa última é particularmente interessante).
Também tem havido trabalho no LOGSPACE , novamente com Leivant e Ramyaa.
É um campo bastante emocionante, com uma conferência anual !
fonte