Algoritmo para resolver o "problema de parada" de Turing

23

"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?

Kaveh
fonte
3
MCCA teve um artigo muito interessante em maio: Provando Program Termination
Christoph Walesch
3
"um algoritmo geral [...] para alguns possíveis pares de entrada de programa" - isso quase se contradiz. Eu acho que você quer se restringir a uma subclasse infinita de todos os programas?
Raphael

Respostas:

25

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)).

sepp2k
fonte
1
A classe de funções primitivas-recursivas é uma "linguagem de programação" bem conhecida para a qual o problema de parada é trivialmente decidível.
Raphael
Existem várias linguagens de " programação funcional total " nas quais todos os programas estão terminando.
Anderson Green
3

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.

Yttrill
fonte
4
Eu acho que é você quem completamente e completamente errado. O primeiro parágrafo da sua resposta não se aplica à pergunta porque ela está perguntando sobre algoritmos - e não o que um humano pode ou não pode provar. O restante da resposta responde ao primeiro parágrafo da pergunta, ou seja, se um algoritmo poderia comprovar o encerramento de alguns programas. Todas as respostas anteriores já disseram "sim" a essa.
sepp2k
3
Sua afirmação de que é possível escrever um algoritmo capaz de comprovar o término de todo programa bem escrito em uma linguagem suficientemente simples de Turing é simplesmente completamente falsa. Para todo algoritmo possível que tenta comprovar o término, há problemas em que todo programa que resolve esse problema não pode ser provado que ele é interrompido por esse algoritmo. Portanto, a menos que você esteja dizendo que todo programa que resolve esse problema é mal escrito por definição (o que seria ridículo), isso desmente o seu argumento.
sepp2k
1
@ Sam Se alguém me perguntar se algum código é interrompido, examinarei o código e tentarei descobrir. Mas eu não sou um algoritmo. E sim, é possível escrever um algoritmo que pode verificar se um programa é interrompido para muitos programas. Mas não foi o que Yttrill disse. Yttrill disse que é possível para todos os programas bem escritos. E, como eu disse no meu comentário anterior, isso é simplesmente falso, a menos que você afirme que certos problemas só podem ser resolvidos por programas mal escritos (que novamente seriam ridículos).
sepp2k
1
@ Sam "parece direto para mim que programas intencionalmente escritos para interromper podem ser facilmente analisados ​​quanto a condições de interrupção" - se esse fosse o caso, por que não temos essas ferramentas? Não é como se as pessoas não estivessem tentando. (Um culpado é método de substituição: em tempo de compilação, você não sabe todo o código que será executado.)
Raphael
1
@ Sam "existe um loop infinito" é algo difícil de abordar, mesmo no loop do mundo real. É claro que fui ensinado a encontrar invariantes em loop, mas isso não significa que eu possa encontrar um (facilmente) em muitos casos. Até onde eu sei, adivinhar e provar é o padrão-ouro atualmente. Mais uma vez, se não eram algoritmos razoavelmente gerais, eu esperaria que eles sejam incluídos nos principais compila ou IDEs (que fazer executar algumas, verificações sintáticas triviais). Você pode dar uma referência a um algoritmo razoavelmente forte?
Raphael
3

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.

AXBYXYXYBA

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)

vzn
fonte
ps como um exemplo impressionante de quão poderosos os quasialgoritmos podem ser, o ACM refere que a função ackermanns pode ser provada interrompida por um quasialgorithm, mas é maior que (não computável por) todas as funções recursivas primitivas.
vzn
1
"a palavra" algoritmo "é geralmente reservada para programas que sempre param." - Não sei se isso é verdade. Existem muitos algoritmos que terminam parcialmente (especialmente na verificação) e eu nunca ouvi ninguém dizer "algoritmo".
Raphael
existem usos informais do "algoritmo". "encerrar parcialmente" está ok, mas provavelmente não é padrão. como afirmado, ainda não parece haver prazo estipulado. A wikipedia define um algoritmo como um método eficaz, isto é, decidível com as seguintes características (1) sempre dê alguma resposta ao invés de nunca dar nenhuma resposta; (2) sempre dê a resposta certa e nunca dê uma resposta errada; (3) sempre ser concluído em um número finito de etapas, e não em um número infinito; (4) trabalhar para todas as instâncias de problemas da classe.
fácil
e, posteriormente, no mesmo artigo, ele diz: "Uma elucidação adicional do termo" método eficaz "pode ​​incluir o requisito de que, quando houver um problema de fora da classe para a qual o método é eficaz, o método poderá parar ou repetir para sempre sem interromper , mas não deve retornar um resultado como se fosse a resposta para o problema. " ou seja, quase se contradiz!?! tão claramente, notavelmente, há alguma confusão real sobre a questão principal e a terminologia existente não é rigorosa. Observe a palavra "algoritmo" está perto de mais de um milênio de idade ou menos e mudou substancialmente ....
vzn
É verdade: o significado tradicional é provavelmente "método eficaz", como diz a Wikipedia (não há contradição na frase que você cita; é um pouco claro, no entanto) - as pessoas não conceberam funções / algoritmos que não terminaram (por algumas entradas). Eu acho que isso mudou desde os anos 50; como eu disse, hoje as pessoas chamam claramente um método de terminação parcial de "algoritmo".
Raphael
2

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.


fonte
3
"Como todas as línguas, exceto as mais primitivas, são Turing completas (são necessárias apenas variáveis ​​e condicionais)" Isso não é verdade. Antes de tudo, você precisaria, no mínimo, de recursão ou alguma forma de construção de loop (que deve ser tão poderosa quanto um loop while - um loop de contagem simples não é suficiente). Segundo, acho que não há muitas pessoas que chamariam idiomas como Coq ou Agda (que são totais e, portanto, não estão completos), idiomas primitivos ou de brinquedo.
sepp2k
@ sepp2k: Bem, sim. A aritmética Peano também é bastante útil e não é Turing completa. Uma afirmação simplificada, suponho. Se o OP estiver suficientemente familiarizado com o problema, ela poderá preencher os detalhes técnicos.
3
Existe uma enorme diferença entre ser "suficientemente complexo" e ser completo em Turing. Coq é realmente complexo, e é adequado para uma ampla gama de tarefas práticas.
1
@Kerrek SB Bem, é possível que a linguagem Turing-complete seja usada de maneiras que permaneçam prováveis ​​ao término. Se você puder provar que uma fórmula recursiva sempre se aproxima de sua condição final (como a função fatorial), poderá provar que ela termina mesmo que não seja capaz de lidar com todos os tipos de recursão.
@ArtB: Claro, sempre há alguns programas que podem ser provados para serem finalizados. A primeira pergunta do OP pode sugerir isso, embora não tenha certeza de segui-la completamente. Por exemplo, você não pode ter um "algoritmo genérico" que determine se uma determinada família de programas termina, enquanto, por outro lado, você provavelmente poderia construir uma família restrita de funções, de modo que, assumindo que uma função pertença a essa família, você poderia dizer por algoritmo se ela termina. (Eu não tenho certeza se essa família pode ser não-trivial, embora eu acho que posso, mas não posso dar um exemplo..)
2

TT

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.

UMAeuogTEumecM

Kaveh
fonte
1

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.


fonte
4
Por que você acha que Coq e Agda não são úteis? Você está superestimando o valor da perfeição de Turing.
Eu usei o Coq, mas minha reivindicação permanece, pois a maioria dos softwares comerciais é escrita em Java / C ++ / Ruby / C #, para a qual minhas reivindicações são verdadeiras. O tipo de programa que 90% das pessoas estão interessadas em escrever não se beneficiaria. Basicamente, se você não conhece a Coq / Agda, etc., você não é o mercado alvo para isso.
5
Eu diria que 99% dos programas do mundo real se beneficiariam da implementação em um subconjunto não completo de Turing de um idioma. Você não implementará, digamos, a função Ackermann todos os dias. 100% do CRUD não precisa de uma linguagem "real". O processamento de dados é quase sempre trivial. Veja o projeto Terminator - eles estão servindo até um subconjunto decente de possíveis programas C ++, o que é mais do que suficiente para as coisas do mundo real (incluindo drivers e outro código de baixo nível).
A maioria dos projetos do mundo real deseja reutilizar bibliotecas escritas em linguagens completas de Turing e usar seus IDEs, depuradores e tutoriais. Sim, você pode realizar coisas em idiomas não-Turing, mas não consigo imaginar alguns dizendo "quero fazer X" e minha resposta seja "Use Coq". ps- obrigado por me apresentar ao The Terminator Project .
4
uma proporção inimaginavelmente grande da lógica de negócios já está implementada em um SQL não completo de Turing. E DSLs e eDSLs estão em alta agora. Portanto, em breve a maioria dos programadores de aplicativos de negócios esquecerá todas as linguagens de "uso geral".