Recentemente, ouvi uma analogia interessante que afirma que a prova de Turing da indecidibilidade do problema da parada é muito semelhante ao paradoxo do barbeiro de Russell.

Então, fiquei pensando: os matemáticos conseguiram tornar a teoria dos conjuntos consistente ao passar da ingênua formulação de campo de Cantor para um sistema mais complexo de axiomas (teoria dos conjuntos ZFC), fazendo importantes exclusões (restrições) e adições ao longo do caminho.

Portanto, seria possível tentar apresentar uma descrição abstrata da computação geral mais poderosa e expressiva que as máquinas de Turing, e com a qual se poderia obter uma prova existencial ou talvez um algoritmo para resolver o problema de parada para uma máquina de Turing arbitrária?

Você não pode realmente comparar. A teoria dos conjuntos ingênua tinha paradoxos que foram eliminados pela teoria dos conjuntos da ZFC. A teoria precisa ser aprimorada para garantir a consistência, pois uma suposição básica do trabalho científico é que a consistência é alcançável (caso contrário, o raciocínio se torna um negócio arriscado). Suponho que os matemáticos esperavam que fosse possível e trabalhassem para resolver o problema.

Não existe tal situação com a teoria da computação e o problema da parada. Não há paradoxo, não há inconsistência. Acontece que não existe uma máquina de Turing que possa resolver o problema de interrupção da MT. É simplesmente um teorema, não um paradoxo.

Portanto, pode ser que algum avanço em nossa compreensão do universo leve a modelos de computação além do que podemos imaginar agora. O único evento desse tipo, de uma forma muito fraca, que permanece dentro do domínio da TM, foi possivelmente a computação quântica. Além deste exemplo muito fraco que toca a complexidade (quanto tempo leva?) E não a computabilidade (é viável?), Duvido que alguém neste planeta tenha uma pista de que a computabilidade além da MT é esperada.

Além disso, o problema da parada é uma conseqüência direta do fato de as máquinas de Turing serem descritas por um pedaço finito de texto, uma sequência de símbolos. Isso é verdade em todo o nosso conhecimento (tanto quanto sabemos), e é por isso que a fala e os livros são tão importantes. Isso vale para todas as nossas técnicas para descrever provas e cálculos.

Portanto, mesmo se encontrarmos uma maneira de estender a maneira como computamos, digamos com as máquinas T +. Ou isso significaria que encontramos uma maneira de expressar conhecimento além de escrever documentos finitos; nesse caso, a coisa toda fica fora da minha jurisdição (eu afirmo incompetência absoluta) e provavelmente de qualquer outra pessoa. Ou ainda seria expressável em documentos finitos, caso em que teria seu próprio problema de parada para máquinas T +. E você faria a pergunta novamente.

Na verdade, essa situação existe ao contrário. Alguns tipos de máquinas são mais fracos que as máquinas de Turing, como o LBA (Linear Bounded Automata). Eles são bastante poderosos, mas pode ser mostrado exatamente como é feito para a TM que o LBA não pode resolver o problema de parada do LBA. Mas a TM pode resolvê-lo para o LBA.

Finalmente, você pode imaginar modelos computacionais mais poderosos introduzindo o oracle, que são dispositivos que podem dar respostas a problemas específicos e podem ser chamados por uma TM para obter respostas, mas infelizmente não existem fisicamente. Essa TM estendida por oráculo é um exemplo da máquina T + que eu considerei acima. Alguns deles podem resolver o problema de interrupção da MT (abstratamente, não de verdade), mas não podem resolver seu próprio problema de parada, mesmo abstratamente.

Bem, você sempre pode considerar uma máquina de Turing equipada com um oráculo para o problema comum de parada da máquina de Turing. Ou seja, sua nova máquina possui uma fita especial, na qual pode escrever a descrição de uma máquina comum de Turing e sua entrada e perguntar se essa máquina pára nessa entrada. Em uma única etapa, você obtém uma resposta e pode usá-la para realizar cálculos adicionais. (Não importa se está em uma única etapa ou não: seria suficiente se fosse garantido que ela estivesse em um número finito de etapas.)

No entanto, existem dois problemas com essa abordagem.

1. As máquinas de Turing equipadas com esse oráculo não podem decidir seu próprio problema de parada: a prova de Turing da indecidibilidade do problema comum de parada pode ser facilmente modificada para essa nova configuração. De fato, há uma hierarquia infinita, conhecida como "graus de Turing", gerada ao dar ao próximo nível da hierarquia um oráculo para o problema de parada do anterior.

2. Ninguém jamais sugeriu uma maneira pela qual esse oráculo pudesse ser fisicamente implementado. Está tudo muito bem como um dispositivo teórico, mas ninguém tem idéia de como construir um.

Observe também que o ZFC é, em certo sentido, mais fraco que a ingênua teoria dos conjuntos, não mais forte. O ZFC não pode expressar o paradoxo de Russell, enquanto a teoria ingênua dos conjuntos pode. Como tal, uma analogia melhor seria perguntar se o problema da parada é decidível para modelos mais fracos de computação do que as máquinas de Turing. Por exemplo, o problema de parada para autômatos finitos determinísticos (DFAs) é decidível, uma vez que é garantido que os DFAs sejam interrompidos para cada entrada.

Atenção: Uma resposta filosófica / sem rigor

Isso pode ficar um pouco "filosófico", mas acho que se encaixa no espírito da sua pergunta.

Uma máquina não repetível

Uma pedra angular da prova do problema de parada é que uma máquina de Turing se comporta como uma função: para a mesma entrada, ela sempre produz a mesma saída. Se você remover essa propriedade, não precisará lidar com o problema de interrupção "geral", no sentido de que a máquina pode descobrir suas próprias propriedades. Mas você também perde muitas das propriedades teóricas desejáveis ​​dessa máquina.

Removendo propriedades

É um pouco como passar da teoria dos conjuntos para a teoria das categorias: você perde alguns dos "paradoxos" ao perder as limitações. Mas o resultado é muito mais difícil de lidar.

Nesse caso, significa: Você não teria idéia se a máquina apresentasse o resultado "correto". Assim que você sempre pode decidir qual resultado está correto, precisa lidar com algum tipo de "problema de parada" aplicando a máquina a si mesma e construindo uma contradição. Portanto, essa máquina provavelmente não seria muito útil.

O Problema da Parada não foi formulado para expressar as limitações das Máquinas de Turing, mas para expressar uma limitação de todos os sistemas lógicos que podem ser expressos usando um número finito de símbolos. Uma vez que um sistema lógico tenha a capacidade de expressar as soluções para problemas de certa complexidade, ele também terá a capacidade de expressar problemas que não pode resolver. Qualquer extensão de um sistema lógico suficiente para expressar soluções para todos os problemas que ele não conseguia resolver antes também incluirá a capacidade de expressar novos problemas que não pode resolver.

Dada qualquer especificação específica de "Enhanced Turing Machine", seria possível especificar uma "Super-Enhanced Turing Machine" que poderia examinar um programa para o ETM e relatar se ele seria interrompido, mas o SETM só seria capaz de analisar programas para o ETM - não seria capaz de analisar os programas SETM. Não há como definir uma máquina que possa analisar os programas por si só e determinar se eles serão interrompidos porque o ato de adicionar novos recursos criaria novos requisitos para um auto-analisador, e não há como fazer com que os recursos "atinjam" os requisitos. .

Tais máquinas foram previstas e são chamadas de máquinas super-Turing . Várias classes principais de máquinas de super-turing são

• Máquinas com números reais (ou seja, computadores analógicos)
• Máquinas de Turing com tempo infinito
• Máquina de turing não determinística

Nem todas as máquinas de super turing podem resolver o problema de parada (as máquinas de turbulência não determinísticas, em particular, não podem). No entanto, as máquinas conceituais foram criadas, pelo menos em experimentos mentais.