Existe um modelo de computação não completo de Turing, cujo problema de parada é indecidível?

26

Não consigo pensar em nenhum modelo desse tipo, talvez alguma forma de cálculo lambda digitado? algum autômato celular elementar?

Isso quase refutaria o "Princípio da Equivalência Computacional" de Wolfram:

Quase todos os processos que não são obviamente simples podem ser vistos como cálculos de sofisticação equivalente

automata-theory computability turing-machines lambda-calculus universal-computation Diego de Estrada
fonte

Respostas:

18

Você pode criar facilmente modelos artificiais que não são completos para Turing, mas o problema de parada para eles é indecidível. Por exemplo, faça todas as TMs que não parem com nada além de .0 0

Em relação à declaração:

Você não pode refutar uma declaração que não é suficientemente precisa. Quase nenhuma das palavras na declaração está bem definida (forneça a definição para elas, se esse não for o caso).

Kaveh
fonte
mmm, digamos que um modelo é Turing-completo se ele pode simular um UTM.
Diego de Estrada
1
Penso que o princípio de equivalência de Wolfram está mais próximo da física do que da lógica. Os lógicos parecem gostar de atacá-lo por várias razões: não é preciso, não está provado, podemos organizar as coisas para que sejam falsas etc. Mas, na verdade, Wolfram está apontando, a seu modo, um fato muito interessante sobre computação , como surge "na natureza".
Andrej Bauer 28/03
1
Eu não sei sobre a colheita da cereja, o livro parece bastante abrangente para mim, especialmente todas essas notas. Existe uma razão a priori para não permitir alterações nas definições padrão? Você está medindo com o critério errado aqui. Wolfram não está fazendo matemática, pelo menos não no sentido tradicional da palavra.
Andrej Bauer 28/03
4
@ Andrej, meu principal problema é que a declaração é tão vaga que não vejo como ela pode fazer previsões verificáveis ​​/ refutáveis. E sim, se alguém está mudando as definições padrão apenas para poder interpretar o que não seria um suporte para uma reivindicação como um suporte para a reivindicação, acho que é problemático.
precisa
4
A afirmação é vaga, mas e daí? Não é lógica ou matemática. É uma observação, apoiada por um livro grosso e cheio de exemplos, que na natureza os "sistemas computacionais" tendem a ser trivialmente simples ou extremamente sofisticados e "equivalentes" um ao outro. Em vez de criticar Wolfram por não falar o jargão da lógica e da matemática, seria mais produtivo ver que ele tem um ponto e depois formular esse ponto em qualquer formalismo que seu coração desejar. Mas é claro que, se seu coração não deseja isso, você não o fará.
Andrej Bauer 28/03
4

Tenho certeza de que o argumento da diagonalização se aplica a qualquer modelo de computação que:

  • pode se representar como uma string e
  • pode simular outra máquina, dada a representação acima

Se tivéssemos um modelo que violasse uma das condições acima, seu poder computacional seria extremamente limitado.

gabgoh
fonte
10
∀x.f(x)≠x
2

Não tenho certeza sobre a conexão exata, mas isso parece relacionado ao teorema de Friedberg-Muchnik (veja aqui ): há um redefinição cujo grau de Turing é menor que o problema da parada. Esse resultado respondeu a uma pergunta influente de Post e levou à introdução do "método de prioridade" na calculabilidade.

Super0
fonte
-2

Provavelmente. Existem muitos problemas matemáticos que provavelmente incluem alguns deles, que são indecidíveis, ou seja, a resposta é "sim", mas nenhuma prova disso existe. Por exemplo, o problema Collatz 3x + 1 vem à mente como candidato. Ou a questão de se pi contém seqüências arbitrariamente longas de 9s consecutivos. Qualquer problema desse tipo poderia ser considerado um "modelo de computação" presumivelmente muito menos poderoso que um UTM, mas ainda seria indecidível se "pára" ou "sempre pára".

Warren D. Smith
fonte
Não acho que essa abordagem possa funcionar. Veja: para qualquer declaração fixa, existe um algoritmo que decide se é "verdadeiro" ou "falso" em um período finito de tempo, mesmo quando é indecidível no ZFC (ref: en.wikipedia.org/wiki/Busy_beaver #Aplicações ). Por outro lado, se você considerar como modelo de computação o problema "dada uma declaração, decida se há uma prova no ZFC", acho que esse modelo é completo em Turing.
Diego de Estrada