Algoritmo para resolver o "problema de parada" de Turing

"Alan Turing provou em 1936 que um algoritmo geral para resolver o problema de parada de todos os pares possíveis de entrada de programa não pode existir"

Posso encontrar um algoritmo geral para resolver o problema de parada de alguns possíveis pares de entrada de programa?

Posso encontrar uma (s) linguagem (s) de programação em que, para todo tipo de programa nessa linguagem, ele possa decidir se o programa termina ou é executado para sempre?

Posso encontrar um algoritmo geral para resolver o problema de parada de alguns possíveis pares de entrada de programa?

Sim claro. Por exemplo, você pode escrever um algoritmo que retorne "Sim, ele termina" para qualquer programa que não contenha loops nem recursão e "Não, ele não termina" para qualquer programa que contenha um while(true)loop que será definitivamente atingido e não contém uma declaração de pausa e "Não sei" para todo o resto.

Posso encontrar uma (s) linguagem (s) de programação em que, para todo tipo de programa nessa linguagem, ele possa decidir se o programa termina ou é executado para sempre?

Não se esse idioma estiver completo em Turing, não.

No entanto, existem linguagens completas que não são de Turing, como, por exemplo , Coq , Agda ou Microsoft Dafny, para as quais o Problema de Parada é decidível (e de fato é decidido pelos respectivos sistemas de tipos, tornando-as linguagens totais (por exemplo, um programa que pode não terminar) compilar)).

Acho que todas as respostas aqui estão completamente erradas. A resposta para a pergunta é: supondo que o programa tenha a intenção de interromper, então é melhor você poder mostrar que ele para. Se você não conseguir mostrar que ele para com facilidade, o programa deve ser considerado muito mal gravado e rejeitado pelo Controle de Qualidade como tal.

Se você pode realmente escrever um algoritmo de máquina adequado depende da linguagem de programação de entrada e de quão ambicioso você é. É uma meta de projeto razoável para uma linguagem de programação facilitar a comprovação do término.

Se a linguagem é C ++, você provavelmente não pode escrever a ferramenta, é improvável que você faça o analisador funcionar, muito menos provar o término. Para uma linguagem melhor estruturada, você deve ser capaz de gerar uma prova, ou pelo menos fazê-lo com certas suposições: no último caso, a ferramenta deve gerar essas suposições. Uma abordagem semelhante seria incluir asserções de terminação no idioma e usá-las em situações complexas em que a ferramenta confiaria nas asserções.

O ponto principal é que ninguém parece entender que a prova de um programa é realmente possível porque (bons) programadores que pretendem escrever esses programas de interrupção sempre o fazem intencionalmente e com uma imagem mental do porquê de terminar e agir corretamente: esse código é deliberadamente escritos para que fique claro que eles param e estão corretos e se um algoritmo razoável não puder provar isso, possivelmente com algumas dicas, o programa deverá ser rejeitado.

O ponto: os programadores não escrevem programas arbitrários; portanto, a tese do teorema da parada não é satisfeita e a conclusão não se aplica.

excelente e (provavelmente involuntariamente profunda) pergunta. de fato, existem programas de detecção de interrupção que podem ter êxito em conjuntos limitados de insumos. é uma área ativa de pesquisa. possui laços muito fortes com as áreas de prova do teorema (automatizado).

no entanto, ciência da computação não parece ter um termo exato para "programas" que "às vezes" são bem-sucedidos. a palavra "algoritmo" é geralmente reservada para programas que sempre param.

o conceito parece ser distintamente diferente dos algoritmos probabilísticos, em que os teóricos da CS insistem em que haja alguma probabilidade conhecida ou computável de sucesso.

há um termo semialgoritmos que é usado algumas vezes, mas aparentemente é sinônimo de recursivamente enumerável ou não-computável.

portanto, para fins aqui, chame-os de quasialgorithms . o conceito é diferente de decidível vs indecidível.

$A$$X$$B$$Y$$X \subset Y$$X$$Y$$B$$A$

no CS, essa "hierarquia de algoritmos quase" parece ser estudada principalmente apenas informalmente até o momento.

aparece na pesquisa de castores ocupada [1] e no problema do PCP [2]. de fato, um ataque de computação baseado em DNA ao PCP pode ser visto como um quase algoritmo. [3] e é visto em outras áreas já notadas, como prova de teoremas [4].

[1] Novo ataque do milênio ao problema do castor ocupado

[2] Abordando o problema de correspondência de Zhao (v2?)

[3] Usando o DNA para resolver o problema da correspondência pós encadernada por Kari et al.

[4] comprovando o término do programa por Cook et al., Comm. do ACM

(portanto, essa é realmente uma pergunta muito profunda que o defn merece estar no TCS.SE imho ... talvez alguém possa solicitá-lo novamente de uma maneira que se encaixe e permaneça)

Enquanto a linguagem de programação em questão for suficientemente complexa (ou seja, se Turing estiver completa), sempre haverá programas na linguagem que nenhum programa pode provar terminar.

Como todas as linguagens, exceto as mais primitivas, são Turing completas (são necessárias apenas variáveis ​​e condicionais), você realmente pode construir apenas linguagens de brinquedo muito pequenas para as quais pode resolver o problema de interrupção.

Editar: À luz dos comentários, deixe-me ser mais explícito: qualquer idioma que você possa criar para o qual possa resolver o problema de parada precisaria necessariamente ser incompleto em Turing. Isso exclui qualquer idioma que contenha um conjunto adequado de ingredientes básicos (por exemplo, "variáveis, condicionais e saltos", ou como @ sepp2k diz, um loop genérico "while").

Aparentemente, existem várias linguagens práticas "simples" como essa (por exemplo, solucionadores de teoremas, como Coq e Agda). Se eles satisfizerem sua noção de "linguagem de programação", você poderá investigar se eles satisfazem algum tipo de integridade ou se o problema de parada é solucionável para eles.

$T$$T$

Isso é bastante trivial. Se adotarmos a união de qualquer subconjunto ce de TMs de parada e qualquer subconjunto ce de TMs sem parada, o resultado será um conjunto de TMs para as quais o problema de parada é decidível (execute as duas máquinas em paralelo, se a primeira aceitar a TM pára, se o segundo aceitar, a máquina não pára). No entanto, isso não levará a idiomas muito interessantes.

$\mathsf{ALogTime}$$c$$M$

Sim, você pode, mas duvido que seja útil. Você provavelmente precisaria fazer uma análise de caso e só conseguiria procurar os casos mais óbvios. Por exemplo, você pode grep um arquivo para o código while(true){}. Se o arquivo tiver esse código, ele nunca terminará ^. Em geral, você poderia dizer que um programa sem loop ou recursão sempre terminará e há vários casos que você poderia fazer para garantir que um programa terminasse ou não, mas mesmo para um programa de tamanho médio, isso seria muito difícil e em muitos casos, não seria capaz de lhe dar uma resposta.

tl; dr: Sim, mas você não poderá utilizá-lo para a maioria dos programas úteis.

^ Sim, tecnicamente, se esse código não estiver no caminho do código ou se houver outros threads, ele ainda pode terminar, mas estou fazendo uma observação geral aqui.