Indecidibilidade e o Problema da Parada

O problema da parada questiona se um dado programa eventualmente para em uma dada entrada, e a prova de Turing de que nenhum algoritmo pode responder a isso para todos os casos é o exemplo fundador de um problema indecidível.

Definition

Um problema de decisão é indecidível quando nenhum algoritmo pode respondê-lo corretamente para cada entrada; o problema da parada, que decide se um programa arbitrário para em uma entrada arbitrária, é o problema indecidível canônico, provado como tal por um argumento diagonal autorreferencial.

Scope

Este tópico abrange o argumento de diagonalização que estabelece a indecidibilidade do problema da parada, a distinção entre problemas decidíveis, reconhecíveis e co-reconhecíveis, o teorema de Rice que mostra que todas as propriedades semânticas não triviais de programas são indecidíveis, e o catálogo de problemas indecidíveis naturais em lógica, matemática e ciência da computação.

Core questions

• Por que nenhum algoritmo único pode decidir se todo programa para?
• Qual é a diferença entre um problema ser decidível e meramente reconhecível?
• Por que essencialmente todas as propriedades interessantes do comportamento do programa são indecidíveis?
• Como a indecidibilidade se espalha do problema da parada para outros problemas?

Key theories

Indecidibilidade do problema da parada

Assumir um algoritmo que decide a parada leva a uma contradição através de um programa que para exatamente quando se prevê que não parará, portanto, tal algoritmo não pode existir.

Teorema de Rice

Toda propriedade não trivial da função computada por um programa — qualquer coisa que se aplica a alguns programas e falha para outros com base no comportamento — é indecidível, generalizando o resultado da parada para todas as propriedades semânticas.

Clinical relevance

Como a parada e, pelo teorema de Rice, todas as propriedades comportamentais não triviais dos programas são indecidíveis, nenhuma ferramenta pode detectar perfeitamente loops infinitos, verificar a correção arbitrária ou analisar completamente cada programa; analisadores estáticos e verificadores devem, portanto, aproximar, aceitar falsos positivos ou restringir seu escopo.

History

Turing estabeleceu a indecidibilidade do problema da parada e do problema de decisão para a lógica em 1936 usando um argumento diagonal inspirado em Cantor e Gödel. Rice provou sua generalização abrangente em 1953, e nas décadas seguintes muitos problemas naturais, incluindo o décimo problema de Hilbert sobre equações diofantinas, foram mostrados como indecidíveis.

Key figures

• Alan Turing
• Henry Gordon Rice
• Emil Post
• Alonzo Church

Seminal works

• turing1937
• sipser2013

Frequently asked questions

Por que não podemos simplesmente executar um programa para ver se ele para?

Executá-lo informa que ele parou apenas se ele realmente parar; se ele for executado para sempre, nenhuma espera finita revelará isso. O problema da parada exige um método que sempre forneça a resposta correta em tempo finito para cada programa e entrada, e Turing provou que tal método não existe.

A indecidibilidade torna a análise de programas inútil?

Não, mas explica por que a análise perfeita é impossível. As ferramentas lidam sendo conservadoras, sinalizando qualquer coisa que não possam provar ser segura, lidando com classes restritas de programas exatamente, ou resolvendo muitos casos práticos, admitindo que podem falhar em casos adversariais ou patológicos.