O Problema da Paragem e a Indecidibilidade

O problema da paragem, que consiste em decidir se um dado programa para (termina) para uma dada entrada, é o exemplo canónico de um problema algoritmicamente indecidível, e as reduções a partir dele provam a indecidibilidade de muitos outros.

Definition

Um problema de decisão é indecidível se nenhuma máquina de Turing o decidir corretamente para todas as entradas; o problema da paragem questiona se uma máquina arbitrária para para uma entrada arbitrária, e é o problema indecidível prototípico a partir do qual outros são demonstrados indecidíveis por redução.

Scope

Este tópico abrange a formulação precisa do problema da paragem, a sua prova de indecidibilidade por diagonalização, a técnica de redução muitos-para-um para transferir a indecidibilidade, o teorema de Rice sobre propriedades não triviais de programas, e problemas clássicos indecidíveis como o Entscheidungsproblem e o problema da palavra para grupos.

Core questions

• Por que não existe um algoritmo que decida se os programas param?
• Como as reduções são usadas para provar que um problema é indecidível a partir de outro?
• O que o teorema de Rice diz sobre a decisão de propriedades de programas?
• Quais problemas matemáticos famosos se revelaram indecidíveis?

Key theories

Insolubilidade do problema da paragem

Um argumento diagonal mostra que assumir um decisor de paragem leva a uma contradição, portanto, nenhum algoritmo pode decidir a paragem para todos os programas e entradas.

Redução e transferência de indecidibilidade

Se um problema indecidível conhecido se reduz a um problema alvo, o alvo também é indecidível, tornando a redução a ferramenta padrão para estabelecer a indecidibilidade.

Teorema de Rice

Toda propriedade não trivial da função computada por um programa é indecidível, portanto, essencialmente nenhuma propriedade comportamental interessante de programas pode ser decidida algoritmicamente.

Clinical relevance

Os resultados de indecidibilidade estabelecem limites rigorosos para o raciocínio automatizado e a análise de programas: eles mostram que ferramentas gerais perfeitas para verificar a terminação ou as propriedades de programas não podem existir, e explicam por que muitos problemas em lógica, álgebra e teoria dos números não têm solução algorítmica.

History

Turing e Church demonstraram em 1936 que o Entscheidungsproblem, a questão de um algoritmo que decide a validade de primeira ordem, é insolúvel, com o problema da paragem no cerne do argumento de Turing. Rice generalizou o fenómeno em 1953, e a indecidibilidade foi posteriormente estabelecida para problemas concretos como o problema da palavra para grupos por Novikov e o décimo problema de Hilbert por Matiyasevich.

Key figures

• Alan Turing
• Alonzo Church
• Henry Gordon Rice
• Pyotr Novikov

Seminal works

• sipser2013
• turing1936
• rogers1987

Frequently asked questions

Por que um computador mais rápido não consegue resolver o problema da paragem?

A indecidibilidade é independente da velocidade ou da memória: o argumento diagonal exclui qualquer algoritmo, independentemente do tempo que lhe seja dado. O problema da paragem é insolúvel em princípio, não meramente impraticável.

Podemos alguma vez saber se um programa para?

Frequentemente sim para programas específicos, por análise ou executando-os. O que é impossível é um único algoritmo que responda corretamente à pergunta para cada programa e entrada. Os verificadores de terminação práticos, portanto, só têm sucesso em classes restritas ou podem falhar em dar uma resposta.